• 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...