|
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.
The QMLTP library v1.1 contains 600 modal problems.
See the documentation
for a detailed description.
QMLTP library v1.1
|