• PVS

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

• HOL

• Referenced in 489 articles [sw05492]
• implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems...

• z3

• Referenced in 488 articles [sw04887]
• high-performance theorem prover being developed at Microsoft Research.Z3 supports linear real and integer arithmetic...

• TPTP

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

• E Theorem Prover

• Referenced in 188 articles [sw10187]
• Brainiac Theorem Prover: E is a theorem prover for full first-order logic with equality...

• HOL Light

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

• VAMPIRE

• Referenced in 233 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 200 articles [sw06905]
• useful complement to first-order theorem provers, with the prover searching for proofs and Mace4...

• Prover9

• Referenced in 174 articles [sw04969]
• Mace4: Prover9 is an automated theorem prover for first-order and equational logic, and Mace4...

• SPASS

• Referenced in 177 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 159 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 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 126 articles [sw04438]
• called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification...

• Pesca

• Referenced in 127 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 first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising...