The QMLTP Library

Benchmarking Theorem Provers for First-Order Modal Logics

Benchmark Problems
ATP Systems
Benchmark Problems

The most recent version of the QMLTP library contains 600 problems for first-order modal logics (580 uni-modal problems and 20 multi-modal problems). All problems are represented in the standardized syntax of the TPTP library for classical logic extended by two additional unary operators #box and #dia representing the modalities "necessary" and "possible". The problem set includes some documentation, e.g. papers about the QMLTP library, comparison tables, statistics files and a readme file. The tptp2X tool and some format files are included as well. They can be used for converting the problems into a syntax used by some of the existing first-order modal ATP systems.

The following readme files give a brief introduction on how to use the QMLTP library:

The performance results of some first-order ATP systems on these benchmark problems can be found in the ATP systems section. Please contact us if you would like to submit new problems suitable for benchmarking first-order modal ATP systems.

QMLTP Library v1.1

The QMLTP library v1.1 contains 600 modal problems. See the documentation for a detailed description.

QMLTP library v1.1

Problem library: QMLTP-v1.1.tar.gz (gzipped tar, 568 kbytes)
Statistics: QMLTP-v1.1-statistics.txt (3 kbytes)

Jens Otten / Thomas Raths 31.01.2012