
Prover9
 Referenced in 170 articles
[sw04969]
 Prover9 and Mace4: Prover9 is an automated theorem prover for firstorder and equational logic...

SPASS
 Referenced in 174 articles
[sw04108]
 SPASS is an automated theorem prover for firstorder 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, 117172 (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 theoremprover for firstorder 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...

LEOII
 Referenced in 49 articles
[sw00512]
 based higherorder theorem prover designed for fruitful cooperation with specialist provers for natural fragments ... cooperate with TPTP compliant firstorder automated theorem provers such as E, SPASS, Gandalf ... winner of the THF division (automation of higherorder logic) at CASCJ5. 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 higherorder logic. The particular form of higher...

TPS
 Referenced in 71 articles
[sw00973]
 Proving System. The former is an automated theoremprover for firstorder 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 firstorder 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 objectoriented ... 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, nontheorems 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...

EDarvin
 Referenced in 19 articles
[sw06852]
 Darwin is an automated theorem prover for firstorder 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...