| Bitwuzla |
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … |
| Boolector |
[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … |
| cvc4 |
[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … |
| cvc5 |
cvc5 is an automatic theorem prover for SMT problems.
|
| E |
E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with … |
| STP |
STP is a constraint solver for quantifier-free bitvectors.
APIs and Bindings This tool is available … |
| Vampire |
Vampire is a theorem prover.
|
| Z3 |
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings This … |
| Zipperposition |
Zipperposition is an automated theorem prover for first-order logic with equality and theories.
|