• SPASS

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

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

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

  • Referenced in 137 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 145 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 117 articles [sw04438]
  • WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions...
  • LEO-II

  • Referenced in 42 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...
  • TPS

  • Referenced in 67 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 42 articles [sw02589]
  • available to current first-order automated theorem provers (ATPs) (and vice versa) and to boost...
  • Satallax

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

  • Referenced in 27 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...
  • Zenon

  • Referenced in 19 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...
  • DCTP

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

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

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

  • Referenced in 32 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...
  • MPTP

  • Referenced in 21 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 19 articles [sw21343]
  • system transforms the output of several automated theorem provers for first order logic with equality...
  • MathWeb

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

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