TPTP-v3.4.2 ReadMe ------------------ Fri May 30 12:37:15 EDT 2008. (Please read the TPTP technical report for full details about the TPTP.) Description ----------- 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. The TPTP is the work of Geoff Sutcliffe and Christian Suttner. The TPTP is maintained and distributed from the Department of Computer Science, University of Miami, USA. The TPTP is also supported by the Institut fuer Informatik, TU Muenchen, Germany. The TPTP is regularly updated. If you would like to become a registered TPTP user and be kept informed of developments, please email Geoff Sutcliffe at geoff@cs.miami.edu. Simple instructions for obtaining and installing the TPTP are given in the Quick Installation Guide at the end of this ReadMe file. Files ----- The TPTP files are kept in various directories, as described below. The directory structure should not be changed, as the TPTP software is coded to work in the structure as distributed. ReadMe-v3.4.2 - This file. TPTP-v3.4.2.tar.gz - The TPTP problem library, which expands to : + Axioms - The axiom files directory. Axiom files are merged into problem files. + Problems - The problem files directory with subdirectories for each domain. The subdirectories contain problem files with the formulae specific to each problem. + Generators - The generator files directory. Generator files are used to generate instances of generic problems, according to user supplied size parameters. + Documents - A directory containing documents that relate to the TPTP. The files contain comprehensive online information about the TPTP, and provide quick access to data that is useful for using the TPTP, using standard system tools (e.g., grep, awk). + TPTP2X - The directory containing the tptp2X utility. The tptp2X utility: * Converts from the TPTP format to formats used by existing ATP systems. * Applies transformations to the clauses of TPTP problems. * Controls the generation of TPTP problem files from TPTP generator files. + Scripts - A directory containing shell scripts that may be used with the TPTP. BuggedProblems-v3.4.2 - A list of bugs in the current TPTP (bugs found after release). Conditions of use ----------------- By providing this library of ATP problems, and a specification of how these problems should be presented to ATP systems, it is our intention to place the testing, evaluation, and comparison of ATP systems onto a firm footing. For this reason, you should abide by the following conditions when using TPTP problems and presenting your results. 1. The TPTP release number must be stated. 2. Each problem must be referenced by its unambiguous syntactic name. 3. No formulae may be changed, added, or removed without explicit notice (this holds also for removing equality axioms when built-in equality is provided by the prover). 4. The formulae may not be reordered without explicit notice. If reordering is done using the tptp2X utility, the reordering must be explicitly noted. 5. The header information in each problem may not be used by the ATP system without explicit notice. Any information that is given to the ATP system, other than that in the "input_formula"s and "input_clause"s, must be explicitly noted. 6. All system switches and default settings must be recorded. Please email one of us if : --------------------------- 1. You find any mistakes in the TPTP. 2. You are able to provide further information for a TPTP problem. 3. You want to contribute a problem to the TPTP. Please use the problem template that comes with the distribution, and fill in header information as far as possible. Any unambiguous representation will do for the formulae. 4. You have any suggestions for improving the TPTP library. General Disclaimer ------------------ Every effort has been made to ensure that the TPTP problems have been correctly presented, and that appropriate acknowledgments have been made. However, we do not guarantee that we have succeeded, and accept no responsibility for any errors or omissions. We will gratefully receive comments and corrections. Copyright --------- The TPTP is copyrighted (c) 1993-2008, by Geoff Sutcliffe & Christian Suttner. Use and verbatim redistribution of the TPTP are permitted. Distribution of any modified version or modified part of the TPTP requires permission. ================================================================================ 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 Use the World Wide Web (WWW) with the following URL : http://www.tptp.org 2. Installing the TPTP prompt> tar xzf TPTP-v3.4.2.tar.gz prompt> cd TPTP-v3.4.2 prompt> ./Scripts/tptp1T_install <... the script will then ask for required information> prompt> ./Scripts/tptp2T_install <... the script will then ask for required information> prompt> ./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. Both utilities can be installed in a default configuration by appending a -default flag to the install command. 3. Converting all the TPTP problems to the syntax of other ATP systems prompt> ./TPTP2X/tptp2X -f<Format> where the available <Format>s can be seen as the extensions of the TPTP2X/format.* files. 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. ================================================================================