The QMLTP Library

Benchmarking Theorem Provers for First-Order Modal Logics

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

Thomas Raths Jens Otten
University of Oslo

Jens Otten / Thomas Raths 11.10.2021