The QMLTP Library

Benchmarking Theorem Provers for First-Order Modal Logics


Welcome
Benchmark Problems
ATP Systems
Contact
 
ATP Systems

Below you find a list of automated theorem proving systems for first-order modal logic. For each system detailed information is provided including a format file. This file is used in conjunction with the tptp2X tool for converting problems from the QMLTP/TPTP syntax into the input syntax of one of the existing ATP systems. All format files are also included in the problem collection file of the QMLTP library.

The following file contains overall statistics and a performance comparison of ATP systems for modal logic on all problems in the QMLTP library: QMLTP-v1.1-comparison.txt (31 kbytes).

The list below contains information about the following intuitionistic ATP systems: GQML-Prover, Leo-II, Satallax, f2p+MSPASS, MleanTAP, MleanSeP, and MleanCoP.

We appreciate any information about modal ATP systems you would like to see included in this list. If you have tested your system on the benchmark problems in the QMLTP library we would like to hear about it. Please contact us so that we can update the information in this list.


GQML-Prover

Name/version: GQML-Prover version 1.2
Author(s): V. Thion, S. Cerrito, M. C. Mayer (Université de Paris-Sud and Università di Roma)
Homepage/download: http://cialdea.dia.uniroma3.it/GQML/
Description: Analytic tableau prover with free variables for many first-order modal logics. Implemented in OCaml.
Examples: GQMLProver_example.txt (1 kbyte)
References: V. Thion, S. Cerrito, M. Cialdea Mayer. A General Theorem Prover for Quantified Modal Logics. In U. Egly, C. G. Fermüller, Eds., TABLEAUX-2002, LNCS 2381, pp. 266-280. Springer, 2002.
Performance results: GQMLProver1.2_QMLTP-v1.1.txt (60 kbyte)
Format file: format.gqmlprover (6 kbytes)

Leo-II

Name/version: Leo-II version 1.2.6
Author(s): Christoph Benzmüller, Frank Theiss (Articulate Software and Universität des Saarlandes)
Homepage/download: http://www.ags.uni-sb.de/~leo/
Description: Resolution prover using an extensional higher-order resolution calculus. Modal formulae are embedded into simple type theory. Implemented in OCaml.
Examples: Leo-ii_example.txt (4 kbyte)
References: C. Benzmüller, L. Paulson, F. Theiss, A. Fietzke. LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. IJCAR 2008, LNAI 5195, pp. 162-170. Springer, 2008.
Performance results: Leo-ii1.2_QMLTP-v1.1.txt (73 kbyte)
Format file: format.thf (9 kbytes)

Satallax

Name/version: Satallax version 2.2
Author(s): Chad E. Brown (Universität des Saarlandes)
Homepage/download: http://www.ps.uni-saarland.de/~cebrown/satallax/
Description: Tableau prover using a complete ground tableau calculus for higher-order logic. Modal formulae are embedded into simple type theory. Implemented in Common Lisp.
Examples: Satallax_example.txt (36 kbytes)
References: J. Backes, C. E. Brown. Analytic Tableaux for Higher-Order Logic with Choice. IJCAR 2010, LNCS 6173, pp. 76-90. Springer, 2010.
Performance results: Satallax2.2_QMLTP-v1.1.txt (75 kbyte)
Format file: format.thf (9 kbytes)

f2p+MSPASS

Name/version: f2p+MSPASS version 3.0
Author(s): J. Otten (University of Potsdam), U. Hustadt (University of Liverpool), R. A. Schmidt (University of Manchester), C. Weidenbach et al. (MPI Saarbruecken)
Homepage/download: http://www.spass-prover.org/
Description: An instance-based method generating ground formulas that are proved by the ATP system MSPASS 3.0 in propositional modal logic. Implemented in Prolog and C.
Examples: F2p+MSPASS_example.txt (2 kbyte)
References: U. Hustadt, R. A. Schmidt. MSPASS: Modal Reasoning by Translation and First-Order Resolution. R. Dyckhoff., Ed., TABLEAUX-2000, LNAI 1847, pp. 6781. Springer, 2000.
Performance results: F2p+MSPASS3.0_QMLTP-v1.1.txt (53 kbyte)
Format file: format.mleancop (6 kbytes)

MleanTAP

Name/version: MleanTAP version 1.3
Author(s): J. Otten (University of Potsdam)
Homepage/download: http://www.leancop.de/mleantap
Description: Tableau prover for the first-order modal logics D and S4. Uses a prefixed analytic tableau calculus and prefix unification. Implemented in Prolog.
Examples: MleanTAP_example.txt (2 kbyte)
Performance results: MleanTAP1.3_QMLTP-v1.1.txt (61 kbyte)
Format file: format.mleancop (5 kbytes)

MleanSeP

Name/version: MleanSeP version 1.2
Author(s): J. Otten (University of Potsdam)
Homepage/download: http://www.leancop.de/mleansep
Description: Sequent prover for the first-order modal logics D, D4, K, K4, S4, and T. Uses a sequent calculus with free variables and Skolemization. Implemented in Prolog.
Examples: MleanSeP_example.txt (2 kbyte)
Performance results: MleanSeP1.2_QMLTP-v1.1.txt (44 kbyte)
Format file: format.mleancop (5 kbytes)

MleanCoP

Name/version: MleanCoP version 1.2
Author(s): J. Otten (University of Potsdam)
Homepage/download: http://www.leancop.de/mleancop
Description: Automated Prover based on the clausal connection calculus for the first-order modal logics D, S4, S5, and T. Extends the classical leanCoP prover by adding prefixes to the literals and a prefix unification algorithm. Implemented in Prolog.
Examples: MleanCoP_example.txt (2 kbyte)
Performance results: MleanCoP1.2_QMLTP-v1.1.txt (61 kbyte)
Format file: format.mleancop (5 kbytes)


Jens Otten / Thomas Raths - University of Potsdam 31.01.2012