[Prev][Next][Index][Thread]
TPTP-v1.2.0 release
*Email us if you want to register as a TPTP user or be removed from this alias.
The TPTP Problem Library, Release v1.2.0
----------------------------------------
Geoff Sutcliffe
Dep't of Computer Science, James Cook University, Australia.
geoff@cs.jcu.edu.au
Christian Suttner
Institut fuer Informatik, TU Muenchen, Germany
suttner@informatik.tu-muenchen.de
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 principal motivation for this project is to move the testing and evaluation
of ATP systems from the previously ad hoc situation onto a firm footing. This
became necessary, as results currently being published often do not accurately
reflect the capabilities of the ATP system being considered. A common library
of problems is necessary for meaningful system evaluations, meaningful system
comparisons, repeatability of testing, and the production of statistically
significant results. The TPTP is such a library.
Release v1.2.0 of the TPTP is now available. TPTP v1.2.0 contains 2758 problems
in 25 domains. Here's what's new in v1.2.0 (after v1.1.3) :
+ 267 new problems, in the domains BOO COL GRP MSC PUZ ROB SYN.
+ 49 bugfixes done, in the domains COL LCL PUZ ROB SYN.
+ Generic problems (e.g., the N-queens problem) are now handled by problem
generators, which allow the automatic generation of any desired problem size.
+ The % Syntax field has been reordered in all files.
+ The tptp2X utility has been extended and improved in various ways :
- Installation and use of tptp2X have been simplified.
- tptp2X now updates the % Syntax field after transformations.
- There are three new output formats: 3TAP, KIF, and leanTAP.
- Problem generation has been integrated into tptp2X.
- The syntax for specifying equality axiom removal has changed.
- The syntax for specifying OTTER format output has changed.
- A new syntax conversion option for the SETHEO system has been added.
+ The TPTP technical report has been substantially revised.
The TPTP is regularly updated with new problems, additional information, and
enhanced utilities. 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)
or Christian Suttner - suttner@informatik.tu-muenchen.de (FAX: +49-89-526502)
The TPTP can be obtained by anonymous ftp from either the Department of
Computer Science, James Cook University, Australia, or the Institut fuer
Informatik, TU Muenchen, Germany. Instructions for fetching and unpacking the
TPTP are given below in the Quick Guide. There are three files in the TPTP
distribution: ReadMe-v1.2.0, TPTP-v1.2.0.tar.gz, and TR-v1.2.0.ps.gz. General
information about the library is in the ReadMe-v1.2.0 file, the library is
packaged in TPTP-v1.2.0.tar.gz, and a technical report describing the TPTP (in
postscript form) is in TR-v1.2.0.ps.gz. Please read the ReadMe file, as it
contains up-to-date information about the TPTP. The technical report serves as
a manual explaining the structure and use of the TPTP. It also explains much of
the reasoning behind the development of the TPTP.
TPTP Quick Installation Guide
-----------------------------
This explains how to obtain, install, and syntax-convert the TPTP problems. For
more details, explanations, and further options, see the TPTP technical report.
1. Obtaining the TPTP by FTP
prompt> cd <the directory where you want the TPTP to reside>
prompt> ftp -i ftp.cs.jcu.edu.au # or: ftp -i 137.219.53.16
# or use
ftp -i flop.informatik.tu-muenchen.de # or: ftp -i 131.159.8.35
Name (ftp.cs.jcu.edu.au:<your login-name>): ftp
331 Guest login ok, send your complete e-mail address as password.
Password:<your full login-name>
ftp> cd pub/research/tptp-library # on ftp.cs.jcu.edu.au
cd pub/tptp-library # on flop.informatik.tu-muenchen.de
ftp> binary
ftp> mget *.gz
ftp> quit
Or use the World Wide Web (WWW) with either of the following URLs :
http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
2. Installing the TPTP
prompt> gunzip -c TPTP-v1.2.0.tar.gz | tar xvf -
prompt> TPTP-v1.2.0/TPTP2X/tptp2X_install
<... the script will then ask for required information>
If you don't have any Prolog installed, you need to get one first. BinProlog
is freely available by anonymous ftp from clement.info.umoncton.ca:BinProlog
3. Converting all the TPTP problems to the syntax of other ATP systems
prompt> TPTP-v1.2.0/TPTP2X/tptp2X -f<Syntax>
where <Syntax> is one of kif, leantap, tap, meteor, mgtp, otter, pttp,
setheo, sprfn, or tptp.
The tptp option simply expands include directives, producing files in the
TPTP Prolog-style syntax. tptp2X offers MUCH more than this. See the TPTP
technical report for a detailed description of the utility, including
information on how to produce output in your own syntax.