Automated theorem provers are programs that automate logical reasoning. They can, e.g., be used to provide an answer to the question if a conjecture is a logical consequence of a given set of axioms. More specifically they determine if a given propositional or first-order formula is logically valid with respect to a specific logic.

The following theorem provers are based on theoretical results that are covered in several publications. It also includes a problem library for benchmarking automated theorem provers.

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 ]

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 ]

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 intuitiontistic theorem proving systems, performance details and status information for all included formulae. [ more ]

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 different connectives the implementation can easily be adapted to deal with other non-classical logics. [ more ]

ileanSeP is a Prolog program that implements a very 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 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. Due to the compact code the program can easily be modified for special purposes or applications. [ more ]

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 ]