|
|
|
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.
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|