
SPASS
 Referenced in 155 articles
[sw04108]
 SPASS is an automated theorem prover for firstorder logic with equality. So the input...

Prover9
 Referenced in 147 articles
[sw04969]
 Prover9 and Mace4: Prover9 is an automated theorem prover for firstorder 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, 117172 (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 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 117 articles
[sw04438]
 WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions...

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

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

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

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

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

EDarvin
 Referenced in 18 articles
[sw06852]
 Darwin is an automated theorem prover for firstorder clausal logic with equality. It accepts...