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:
- Provers for classical logic: nanoCoP, leanCoP, ncDP.
- Provers for intuitionistic logic: nanoCoP-i, ileanCoP, ileanTAP, ileanSeP.
- Provers for modal logic: nanoCoP-M, MleanCoP, MleanTAP, MleanSeP.
- Provers for linear logic: linTAP.
- Benchmark libraries: ILTP, QMLTP.
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 ]
Recent Activities
- ARQNL 2024. The 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics in Nancy/France.
- AReCCa 2023. The International Workshop on Automated Reasoning with Connection Calculi in Prague/Czech Republic.
- ARQNL 2022. The 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics in Haifa/Israel.
- The nanoCoP 2.0 Connection Provers for
Classical, Intuitionistic and Modal Logics.
Paper at TABLEAUX in Birmingham/UK
[see nanoCoP, nanoCoP-i, nanoCoP-M] -
Build Your Own First-Order Prover and
How to Build an Automated Theorem Prover.
Invited tutorials at CADE in Natal/Brazil and TABLEAUX in London/UK - The Geological Assistant (supporting reasoning in the
geology domain).
A SIRIUS project at the University of Oslo