|
|
|
|
Welcome to the QMLTP Library
|
The Quantified Modal Logics Theorem Proving (QMLTP) library provides
a platform for testing and benchmarking automated theorem proving (ATP)
systems for first-order modal logics.
It includes a problem collection
for first-order modal ATP systems
and tools for converting the problems into the input syntax of
some existing modal ATP systems. It also includes
information about currently available
ATP systems for first-order modal logic and their performance
results on the problems in the QMLTP library.
Please contact
us for further information or if you want to submit new
benchmark problems or performance results.
Features of the QMLTP Library:
-
600 modal first-order benchmark problems in a
standardized extended TPTP syntax.
-
Information about the modal status (i.e. Theorem, Non-Theorem
or Unsolved) and about the modal rating (i.e. the relative difficulty
of the problems with respect to current state-of-the-art ATP
systems) of all 580 uni-modal benchmark problems
for modal logics K, D, T, S4 and S5, with
varying, cumulative and constant domains,
and of 20 multi-modal problems with cumulative domains.
-
Tools for translating the benchmark problems into a syntax
of some existing modal ATP systems.
-
Information about currently available ATP systems for
first-order modal logic and their performance on all
problems in the QMLTP library.
The QMLTP library is suitable for developing, testing and evaluating
novel calculi, search strategies and ATP implementations for
first-order modal logic.
The following paper gives a short description of the QMLTP
library v1.0:
-
Thomas Raths, Jens Otten.
The QMLTP Library: Benchmarking Theorem Provers for
Modal Logics.
Technical Report, University of Potsdam, 2011.
·
qmltp-v10_tr.pdf
(120 kbytes)
·
qmltp-v10_tr.dvi
(28 kbytes)
Please contact us if you have benchmark problems or an ATP system
you would like to submit.
If you need more information please do not hesitate to contact us.
|