Automated Reasoning Systems
Classic FOF → CNF-Saturation Systems
- Otter
- a well known system
- Prover9
- successor to Otter
- E
- purely equational reasoning
- SPASS
- a theorem prover with sorts
- Vampire
- wins CASC
- iProver
- instantiation based
- Twee
- developed by King Nicholas (of Twee)
Typed Logic (with Arithmetic) Systems
-
Beagle - an evolutionary system
- cvc5
- an SMT system that has seen the light
- Princess
- where arithmetic comes first
- SNARK
- classical ATP with procedural attachments
- SPASS+T
- superposition with built-in arithmetic and SMT
- Vampire
- ad hoc integration of arithmetic
- Z3
- many techniques, with support for many theories
Higher-order Systems
- E
- from FOF to THF
- Nitpick
- model finding with Isabelle
- Leo III
- extensional paramodulation and first-order ATP
- Satallax
- tableau calculus and propositional ATP
- Vampire
- Recent extension to higher-order logic
- Zipperposition
- aimed at typed logics
Non-CNF-Saturation Systems
- Equinox
- a hierarchy of logics
- Geo
- based on geometric resolution
- leanCoP
- very compact connection calculus
- Muscadet
- natural deduction system
Finite Model Finders
- FM-Darwin
- in the spirit of Paradox
- Mace4
- partner of Prover9
- Paradox
- based on flattening and instantiation
- Infinox
- finite model denial
Infinite Model Finders
- cvc5
- an SMT system that has seen the light
- FEST
- models with an integer domain
Meta-Systems
- Fampire
- FLOTTER + Vampire
- MaLARea
- Machine learning axiom selection
- *-MaLeS
- an automatic strategy scheduler
- SSCPA
- selective competition parallism
- CSE
- contradiction separation with saturation
(Higher-order) Proof Assistants (partially "A")
The Theorem Prover Museum
