*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 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:): ftp 331 Guest login ok, send your complete e-mail address as password. Password: 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 where 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.