*Email us if you want to register as a TPTP user or be removed from this alias. The TPTP Problem Library, Release v2.0.0 ---------------------------------------- (This version will be used in CADE-14 ATP System Competition) 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. 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 N-queens problem). + A utility to convert the problems to existing ATP systems' formats. + 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 being published do not always 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 v2.0.0 of the TPTP is now available. TPTP v2.0.0 contains 3277 problems in 27 domains. The major changes in this version are : + FOF (First Order Form) problems have been added. + Three new domains have been added: FLD (Field theory), KRS (Knowledge Representation), and MGT (Management). + Difficulty ratings have been assigned to those problems for which sufficient performance data from state-of-the-art ATP systems is available. The ratings are given in a new % Rating field in the problem headers. + A new utility called tptp1T, for finding problems with certain user specified characteristics, has been added. Other changes (after v1.2.1) are: + FOF problems 110 new abstract problems, in the domains COM GRP LCL MGT MSC PUZ SET SYN. 217 new problems, in the domains COM GRP LCL MGT MSC PUZ SET SYN. 1 new generators. 0 bugfixes done. + CNF problems 120 new abstract problems, in the domains FLD KRS LCL PUZ. 309 new problems, in the domains FLD KRS LCL PUZ. 1 new generators, in the domains PUZ. 3 bugfixes done, in the domains GRP SYN. + The % Version fields have been reviewed. Problems that are "Special" have been explicitly labelled as such. + The % Syntax field of CNF problems has been extended to include the average number of literals per clause and the average term depth. + The tptp2X utility has been extended and improved : - Four new CNF output formats: CLIN-S, DFG, DIMACS, ILF. - Three FOF output formats: TPTP, Otter, OSCAR. - Nine new transformations: clausify (4 FOF to CNF transformations), simplify (simplifies a set of clauses), cnf (clausify then simplify), er (reverses arguments in the clauses of unit equality problems), ran_er (does the er transformation to randomly selected clauses). - The format modules now receive an extra argument containing the file header information. This information may be used only for supplementary documentation of the problem. + The TPTP technical report has been updated. 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-v2.0.0, TPTP-v2.0.0.tar.gz, and TR-v2.0.0.ps.gz. General information about the library is in the ReadMe-v2.0.0 file, the library is packaged in TPTP-v2.0.0.tar.gz, and a technical report describing the TPTP (in postscript form) is in TR-v2.0.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 * ftp> quit Or use the World Wide Web (WWW) with either of the following URLs : http://www.cs.jcu.edu.au/~tptp/ http://wwwjessen.informatik.tu-muenchen.de/~tptp/ 2. Installing the TPTP prompt> gunzip -c TPTP-v2.0.0.tar.gz | tar xvf - prompt> TPTP-v2.0.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-v2.0.0/TPTP2X/tptp2X -f where is one of clin_s, dfg, dimacs, ilf, kif, leantap, tap, meteor, mgtp, oscar, otter, pttp, setheo, sprfn, or tptp. Some of the formats cannot cope with certain types of problems, e.g., dimacs format is for only propositional CNF problems. The tptp format 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. ================================================================================