-
PVS
- Referenced in 620 articles
[sw03484]
- integrated with support tools and a theorem prover. It is intended to capture the state...
-
HOL
- Referenced in 508 articles
[sw05492]
- implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems...
-
z3
- Referenced in 509 articles
[sw04887]
- high-performance theorem prover being developed at Microsoft Research.Z3 supports linear real and integer arithmetic...
-
TPTP
- Referenced in 378 articles
[sw04143]
- TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for automated...
-
E Theorem Prover
- Referenced in 192 articles
[sw10187]
- Brainiac Theorem Prover: E is a theorem prover for full first-order logic with equality...
-
HOL Light
- Referenced in 293 articles
[sw06580]
- Mike Gordon’s original HOL system. Theorem provers in this family use a version...
-
NQTHM
- Referenced in 149 articles
[sw07543]
- truly important changes to the theorem prover since 1979 are the integration of a linear ... user to give hints to the theorem prover. The significant changes in the logic itself ... computational logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117-172 (1988)]. However ... changes to the logic and the theorem prover since the publication of the authors’ former...
-
VAMPIRE
- Referenced in 239 articles
[sw02918]
- RV02,Vor05] is an automatic theorem prover for first-order classical logic. It consists ... result to the kernel. When a theorem is proved, the system produces a verifiable proof...
-
Mace4
- Referenced in 205 articles
[sw06905]
- useful complement to first-order theorem provers, with the prover searching for proofs and Mace4...
-
Prover9
- Referenced in 177 articles
[sw04969]
- Mace4: Prover9 is an automated theorem prover for first-order and equational logic, and Mace4...
-
SPASS
- Referenced in 178 articles
[sw04108]
- SPASS is an automated theorem prover for first-order logic with equality. So the input...
-
SETHEO
- Referenced in 119 articles
[sw00707]
- SETHEO: A high-performance theorem prover. The paper deals with a theoretical background and practical ... interesting system SETHEO --- a theorem prover for first order logic. The system is based...
-
REDLOG
- Referenced in 160 articles
[sw04250]
- language and theory. In contrast to theorem provers, the methods applied know about the underlying...
-
ETPS
- Referenced in 156 articles
[sw06302]
- System. The former is an automated theorem-prover for first-order logic and type theory ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp...
-
ELAN
- Referenced in 108 articles
[sw02179]
- support the design of theorem provers, logic programming languages, constraints solvers and decision procedures ... support the design of theorem provers, logic programming languages, constraints solvers and decision procedures...
-
SATCHMO
- Referenced in 96 articles
[sw06619]
- SATCHMO: a theorem prover implemented in Prolog. The SATCHMO Theorem Prover...
-
Why3
- Referenced in 130 articles
[sw04438]
- called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification...
-
Pesca
- Referenced in 130 articles
[sw13664]
- proof editor and as an automatic theorem prover. Proofs constructed in Pesca can both...
-
Sledgehammer
- Referenced in 120 articles
[sw07047]
- that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising...
-
Java PathFinder
- Referenced in 120 articles
[sw07658]
- applying existing model checkers and theorem provers to real applications...