Results 1 to 20 of 611
Sort by:

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