ATP Systems
Classic CNF-Saturation Systems
Non-CNF-Saturation Systems
- Darwin
- implements model evolution
- Equinox
- a hierarchy of logics
- Geo
- based on geometric resolution
- iProver
- instantiation based
- 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
Systems with Arithmetic Capabilities
- Otter
- a well known system
- MetiTarski
- resolution and real closed fields
- SNARK
- classical ATP with procedural attachments
- SPASS+T
- superposition with built-in arithmetic and SMT
- SPASS-XDB
- superposition with external computer algebra
- Z3 - many techniques, with support for many theories
Higher-order Systems
- Isabelle
- strategy scheduling the tactics
- Refute and Nitpick
- model finding with refute and nitpick
- LEO II
- extensional higher-order resolution and first-order ATP
- Satallax
- tableau calculus and propositional ATP
- TPS
- strategey scheduling the old TPS
Meta-Systems
- Fampire
- FLOTTER + Vampire
- GrAnDe
- eground + ZChaff
- MaLARea
- Machine learning axiom selection
- SSCPA
- selective competition parallism
- SRASS
- semantic selection of axioms
- SInE
- SUMO inference engine
(Higher-order) Proof Assistants (partially "A")
