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

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

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

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

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

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

NQTHM
 Referenced in 151 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 267 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 228 articles
[sw06905]
 useful complement to firstorder theorem provers, with the prover searching for proofs and Mace4...

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

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

SETHEO
 Referenced in 122 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 166 articles
[sw04250]
 language and theory. In contrast to theorem provers, the methods applied know about the underlying...

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

ETPS
 Referenced in 161 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...

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

SATCHMO
 Referenced in 97 articles
[sw06619]
 SATCHMO: a theorem prover implemented in Prolog. The SATCHMO Theorem Prover...

Why3
 Referenced in 136 articles
[sw04438]
 called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification...

CVC4
 Referenced in 126 articles
[sw09485]
 efficient opensource automatic theorem prover for satisfiability modulo theories (SMT) problems...