Jens Otten

Theorem Provers

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 first-order 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.

Overview:

nanoCoP

nanoCoP is a compact theorem prover for classical first-order logic with equality, which is based on the non-clausal connection calculus and implemented in Prolog. It combines the advantages of natural non-clausal calculi with the efficiency of connection-driven proof search. [ more ]

nanoCoP-M

nanoCoP-M is a compact Prolog program that implements a sound and complete theorem prover for several modal first-order logics. It is an extension of the classic theorem prover nanoCoP, which is based on the non-clausal connection calculus. Using prefixes to encode the restrictions in modal logics and an adapted skolemization ensures a strong performance. [ more ]

nanoCoP-i

nanoCoP-i is a compact Prolog program that implements a sound and complete theorem prover for intuitionistic first-order logic. It is an intuitionistic extension of the classic theorem prover nanoCoP, which is based on the non-clausal connection calculus. Using prefixes to encode the restrictions in intuitionistic logic and an adapted skolemization ensures a strong performance. [ more ]

leanCoP

leanCoP is a compact Prolog theorem prover for classical first-order 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

MleanCoP is a compact Prolog program that implements a sound and complete theorem prover for several modal first-order 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

ileanCoP is a compact Prolog program that implements a sound and complete theorem prover for intuitionistic first-order 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 ]

QMLTP Library

The QMLTP Library (Quantified Modal Logics Theorem Proving Library) provides a platform for testing and benchmarking automated theorem proving systems for first-order 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 first-order modal logics. [ more ]

ILTP Library

The ILTP Library (Intuitionistic Logic Theorem Proving Library) provides a platform for testing and benchmarking automated theorem proving systems for first-order intuitionistic logic. It includes a collection of propositional and first-order benchmark formulae in a standardised syntax, information about existing intuitionistic theorem proving systems, performance details and status information for all included formulae. [ more ]

MleanTAP

MleanTAP is a Prolog program that implements a sound and complete theorem prover for some first-order modal logics. It is based on free-variable 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

ileanTAP is a Prolog program that implements a sound and complete theorem prover for first-order intuitionistic logic. It is based on free-variable 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 non-classical logics. [ more ]

MleanSeP

MleanSeP is a Prolog program that implements a compact theorem prover for some first-order 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

ileanSeP is a Prolog program that implements a compact theorem prover for first-order intuitionistic logic. It is based on a single-succedent 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

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

ncDP is a non-clausal theorem prover for classical propositional logic. It is a generalization of the well-know Davis - Putnam - Logemann - Loveland decision procedure for propositional formulae in clausal form. By working entirely on the original (non-clausal) formula, any translation steps to clausal form are avoided. This yields a compact code and a reasonable performance. [ more ]