• Prover9

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

  • Referenced in 174 articles [sw04108]
  • SPASS is an automated theorem prover for first-order logic with equality. So the input...
  • TPTP

  • Referenced in 368 articles [sw04143]
  • Problems for Theorem Provers) is a library of test problems for automated theorem proving...
  • NQTHM

  • Referenced in 146 articles [sw07543]
  • 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...
  • ETPS

  • Referenced in 152 articles [sw06302]
  • Proving System. The former is an automated theorem-prover for first-order logic and type ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... some extent under Windows. Potential applications of automated theorem proving include hardware and software verification...
  • Why3

  • Referenced in 126 articles [sw04438]
  • WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions...
  • LEO-II

  • Referenced in 49 articles [sw00512]
  • based higher-order theorem prover designed for fruitful cooperation with specialist provers for natural fragments ... cooperate with TPTP compliant first-order automated theorem provers such as E, SPASS, Gandalf ... winner of the THF division (automation of higher-order logic) at CASC-J5. At CASC ... been the first theorem prover that supports THF, FOF and CNF syntax...
  • Satallax

  • Referenced in 48 articles [sw06849]
  • Satallax is an automated theorem prover for higher-order logic. The particular form of higher...
  • TPS

  • Referenced in 71 articles [sw00973]
  • Proving System. The former is an automated theorem-prover for first-order logic and type ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... some extent under Windows. Potential applications of automated theorem proving include hardware and software verification...
  • MPTP 0.2

  • Referenced in 43 articles [sw02589]
  • available to current first-order automated theorem provers (ATPs) (and vice versa) and to boost...
  • Zenon

  • Referenced in 21 articles [sw06753]
  • Zenon: An extensible automated theorem prover producing checkable proofs. We present Zenon, an automated theorem ... Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented ... extended, which makes specific (and possibly local) automation possible in Focal...
  • HR

  • Referenced in 29 articles [sw10392]
  • conjectures and these become theorems if they are proved, non-theorems if disproved. Similar ... itself and (iii) using the Otter theorem prover to prove conjectures. In domains where Otter ... large numbers of theorems for testing automated theorem provers (ATPs), or smaller numbers of prime ... problems, the generation of lemmas for automated theorem proving, and the production of benchmark theorems...
  • EasyCrypt

  • Referenced in 28 articles [sw09738]
  • shelf SMT solvers and automated theorem provers, and then compiled into verifiable proofs...
  • DCTP

  • Referenced in 21 articles [sw06621]
  • Calculus Theorem Prover. DCTP is an automated theorem prover for first order clause logic. Given...
  • KeYmaera

  • Referenced in 37 articles [sw03709]
  • KeYmaera: A hybrid theorem prover for hybrid systems. KeYmaera is a hybrid verification tool ... prover technologies. It is an automated and interactive theorem prover for a natural specification ... program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free...
  • Darwin

  • Referenced in 24 articles [sw04175]
  • Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated...
  • MPTP

  • Referenced in 22 articles [sw02489]
  • mathematics available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system ... untyped first order format suitable for automated theorem provers, and for generating theorem proving problems...
  • TRAMP

  • Referenced in 20 articles [sw21343]
  • system transforms the output of several automated theorem provers for first order logic with equality...
  • E-Darvin

  • Referenced in 19 articles [sw06852]
  • Darwin is an automated theorem prover for first-order clausal logic with equality. It accepts...
  • MathWeb

  • Referenced in 18 articles [sw10293]
  • tasks can be delegated to an automated theorem prover (ATP) by encoding them into...