The TPTP Problem Library, Release v1.2.0
The
full version
of this announcement is available.
The TPTP (Thousands of Problems for Theorem Provers) Problem Library
is a library of test problems for automated theorem proving (ATP)
systems, using the clause normal form of 1st order logic. The TPTP
supplies the ATP community with:
-
A comprehensive library of the ATP test problems that are
available today, in order to provide an overview and a simple,
unambiguous reference mechanism.
-
A comprehensive list of references and other interesting
information for each problem.
-
New generalized variants of problems whose original presentation is
hand-tailored towards a particular automated proof.
-
Arbitary size instances of generic problems (e.g., the pigeon-holes
problem).
-
A utility to convert the problems to existing ATP formats.
Currently the KIF, leanTAP, 3TAP, METEOR, MGTP, OTTER, PTTP,
SETHEO, and SPRFN formats are supported, and the utility can
easily be extended to produce any format required.
-
General guidelines outlining the requirements for ATP system
evaluation.
The tools are available on the WWW or by anonymous ftp, with either
of the following URLs:
-
WWW
-
-
FTP
-
-
WWW
-
-
FTP
-
If you would like to register as a TPTP user, and be kept informed
of such developments, please email one of us. Our addresses are:
Geoff Sutcliffe : geoff@cs.jcu.edu.au (FAX: +61-77-814029)
Christian Suttner : suttner@informatik.tu-muenchen.de
(FAX: +49-89-526502)