
PVS
 Referenced in 603 articles
[sw03484]
 integrated with support tools and a theorem prover. It is intended to capture the state...

HOL
 Referenced in 483 articles
[sw05492]
 implemented. Builtin decision procedures and theorem provers can automatically establish many simple theorems...

z3
 Referenced in 479 articles
[sw04887]
 highperformance theorem prover being developed at Microsoft Research.Z3 supports linear real and integer arithmetic...

TPTP
 Referenced in 372 articles
[sw04143]
 TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for automated...

E Theorem Prover
 Referenced in 186 articles
[sw10187]
 Brainiac Theorem Prover: E is a theorem prover for full firstorder logic with equality...

HOL Light
 Referenced in 286 articles
[sw06580]
 Mike Gordon’s original HOL system. Theorem provers in this family use a version...

NQTHM
 Referenced in 146 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, 117172 (1988)]. However ... changes to the logic and the theorem prover since the publication of the authors’ former...

VAMPIRE
 Referenced in 232 articles
[sw02918]
 RV02,Vor05] is an automatic theorem prover for firstorder classical logic. It consists ... result to the kernel. When a theorem is proved, the system produces a verifiable proof...

Mace4
 Referenced in 198 articles
[sw06905]
 useful complement to firstorder theorem provers, with the prover searching for proofs and Mace4...

Prover9
 Referenced in 172 articles
[sw04969]
 Mace4: Prover9 is an automated theorem prover for firstorder and equational logic, and Mace4...

SPASS
 Referenced in 177 articles
[sw04108]
 SPASS is an automated theorem prover for firstorder logic with equality. So the input...

SETHEO
 Referenced in 119 articles
[sw00707]
 SETHEO: A highperformance 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 157 articles
[sw04250]
 language and theory. In contrast to theorem provers, the methods applied know about the underlying...

ETPS
 Referenced in 153 articles
[sw06302]
 System. The former is an automated theoremprover for firstorder 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 126 articles
[sw04438]
 called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification...

Pesca
 Referenced in 126 articles
[sw13664]
 proof editor and as an automatic theorem prover. Proofs constructed in Pesca can both...

Java PathFinder
 Referenced in 120 articles
[sw07658]
 applying existing model checkers and theorem provers to real applications...

Sledgehammer
 Referenced in 116 articles
[sw07047]
 that harnesses external firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations arising...