Automated theorem provers are programs that automate logical
reasoning. They can, e.g., be used to provide an answer to the
question whether a conjecture is a logical consequence of a given
set of axioms.
More specifically, they determine whether a given propositional
or firstorder formula is logically valid with respect to a specific
logic.
The following list contains theorem provers that are based on
theoretical results that are covered in several
publications. It also includes two
problem libraries for benchmarking automated theorem provers.
leanCoP
is a compact Prolog theorem prover for classical firstorder
logic which is based on the connection calculus. It is sound,
complete, and demonstrates a strong performance.
Due to the compact code the program can easily be modified for
special purposes or applications.
[ more ]
MleanCoP
is a compact Prolog program that implements a sound and
complete theorem prover for several modal firstorder logics.
It is an extension of the classic theorem prover
leanCoP, which is based on the clausal connection calculus.
Using prefixes to encode the restrictions in modal logics
and an adapted skolemization ensures leading performance.
[ more ]
ileanCoP
is a compact Prolog program that implements a sound and
complete theorem prover for intuitionistic firstorder logic.
It is an intuitionistic extension of the classic theorem prover
leanCoP, which is based on the clausal connection calculus.
Using prefixes to encode the restrictions in intuitionistic logic
and an adapted skolemization ensures leading performance.
[ more ]
The QMLTP Library
(Quantified Modal Logics Theorem Proving Library) provides a
platform for testing and benchmarking automated theorem proving
systems for firstorder modal logics. It includes a collection of
benchmark formulae in a standardised syntax, status and rating
information for all included formulae and information about
existing theorem proving systems for firstorder modal logics.
[ more ]
The ILTP Library
(Intuitionistic Logic Theorem Proving Library) provides a platform
for testing and benchmarking automated theorem proving systems for
firstorder intuitionistic logic. It includes a collection of
propositional and firstorder benchmark formulae in a standardised
syntax, information about existing intuitionistic theorem
proving systems, performance details and status information for
all included formulae.
[ more ]
MleanTAP
is a Prolog program that implements a sound and complete
theorem prover for some firstorder modal logics. It is based on
freevariable semantic tableaux extended by an additional prefix
unification to ensure the particular restrictions in modal logics.
As a consequence of this technique, the prover can even deal with,
e.g., varying domains in an efficient way.
[ more ]
ileanTAP
is a Prolog program that implements a sound and complete
theorem prover for firstorder intuitionistic logic. It is based on
freevariable semantic tableaux extended by an additional prefix
unification to ensure the particular restrictions in intuitionistic
logic. Due to the modular treatment of the connectives
the implementation can be adapted to other nonclassical logics.
[ more ]
MleanSeP
is a Prolog program that implements a compact
theorem prover for some firstorder modal logics.
It is based on the standard modal sequent
calculi for modal logics. Using an analytic proof
search, free variables and a dynamic skolemization ensures
good performance.
Inference rules are defined in a modular way, which makes
modifications to the calculus easily possible.
[ more ]
ileanSeP
is a Prolog program that implements a compact theorem
prover for firstorder intuitionistic logic. It is based on a
singlesuccedent intuitionistic sequent calculus.
Using an analytic proof search, free variables and skolemization
ensures a decent performance. Inference rules are defined in a
modular way, which makes modifications to the calculus easily
possible.
[ more ]
linTAP
is a tableau prover for the multiplicative and exponential
fragment of Girards linear logic. It proves the classical validity
of a given formula by constructing an analytic tableau and ensures
the linear validity using prefix unification.
[ more ]
ncDP
is a nonclausal theorem prover for classical propositional logic.
It is a generalization of the wellknow
Davis  Putnam  Logemann  Loveland
decision procedure for propositional formulae in clausal form.
By working entirely on the original (nonclausal) formula,
any translation steps to clausal form are avoided. This yields
a compact code and a reasonable performance.
[ more ]
