The QMLTP Library

Benchmarking Theorem Provers for First-Order Modal Logics


Welcome
Benchmark Problems
ATP Systems
Contact
 
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.


Documentation

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)

Contact

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.

Thomas Raths
   traths
@
cs.uni-potsdam
.
de   
Jens Otten
   jeotten
@
cs.uni-potsdam
.
de   

University of Potsdam
Department of Computer Science
August-Bebel-Straße 89, 14482 Potsdam, Germany


Jens Otten / Thomas Raths - University of Potsdam 11.10.2011