______________________________________________________________________________ | | | This is a BETA-RELEASE of the TPTP Problem Library | | FOR CONTRIBUTING RESEARCHERS ONLY | | | | This beta-release is to provide the opportunity to make the types of changes | | to the library which should be avoided after official release. Your | | collaboration in using this beta-release is highly desired, and will be duly | | acknowledged in the final release, according to its contribution. | | | | Special Conditions of Use for Beta-Release | | ------------------------------------------ | | This beta-release of the TPTP is not final, and the format of presentation | | is subject to change. For the good of yourself and the wider ATP community, | | you must abide by the following conditions : | | 1. You must accept that it is a Beta-release, and may be flawed. (You should | | check back with one of us before referencing the Beta-release in any | | publication, to avoid mistakes arising from changes we are making.) | | 2. You may not distribute the Beta-release any further. If there is anyone | | whom you think should have a copy, please let us know. | | 3. You will aim to provide feedback on the Beta-release until 31/3/93. Any | | problem reports or suggestions must be mailed to | | geoff@cs.jcu.edu.au or | | suttner@informatik.tu-muenchen.de . | | | | Conversely : | | 1. We have already tried to remove flaws from the TPTP as far as possible. | | 2. We will not distribute the Beta-release to anyone who has not agreed to | | these conditions. | | 3. We will react to your problem reports and suggestions. | | 4. We will make an official release of the TPTP after we incorporated the | | feedback (April 1993). The official release will be accompanied by a | | technical report. | | | | Note: The rest of this file is the proposed README file for the official | | release. | |______________________________________________________________________________| File: README as of 3.2.93, regarding TPTP V0 (Beta-release) This files contains important information, and should be read completely and carefully. For correspondance use: geoff@cs.jcu.edu.au (FAX: +61-77-814029) suttner@informatik.tu-muenchen.de (FAX: +49-89-526502) Description ----------- The TPTP (Thousands of Problems for Theorem Provers) problem set aims to supply the community, which is interested in automated theorem proving (ATP) for 1st order predicate logic, with the following : 1. A comprehensive list of the ATP test problems that are available today, in order to provide a simple and unambiguous reference mechanism. 2. Availability of all problems via FTP in a general-purpose format. 3. A comprehensive list of references regarding those problems. The TPTP is the work of Geoff Sutcliffe, Christian Suttner, and Theodor Yemenis. The TPTP was originally compiled at The University of Western Australia, and is now being maintained at the Dept. of Computer Science, James Cook University, Australia. The TPTP is also supported and distributed by the Institut fuer Informatik, TU Muenchen, Germany. Releases -------- Each release of the TPTP is identified by a version number, an edition number, and a patch level, in the form: TPTP v.[.]. The version number refers to major new releases of the TPTP, denoting significant content changes. The edition number is incremented each time new problems are added to the current version. The patch level is incremented each time errors found in the current edition are corrected. Files ----- README - This file. TPTPv0.tar.Z - The TPTP problem library, which expands to : Problems - The problem files directory with subdirectories for each domain. The subdirectories contain problem files with the clauses specific to each problem. Axioms - The axiom set directory, containing axiom set files (that are merged with the problem files). TPTP2X - A directory of Prolog source files, containing a program that reads TPTP problem files and converts them to other formats. Documents - A directory containing documents that relate to the TPTP : README - This file. Domains - The structure and size of the TPTP problem domains. Abbrevs - A list of the abbreviations used in the semantic names. ProblemList - A list of the problems, giving their canonical name, se- mantic name, number of versions, and 1-line description. AxiomList - A list of the axiom sets, giving their canonical name, semantic name, domain, and axiom selection. Index - An index from TPTP problem names to former/other names. ReverseIndex - An index from former problem names to their TPTP names. Conditions of use ----------------- Through the use of this publicly available library of ATP problems, and the specification of how these problems should be presented to ATPs, it is our intention to place the testing, evaluation, and comparison of ATPs on a firm footing. For this reason, you should abide by the following conditions when refering to the TPTP problems : 1. No clauses/literals may be added/removed without explicit notice. 2. The clauses/literals may not be rearranged without explicit notice. If the clause and literal reversing done by the tptp2X utility is used, the reversals must be explicitly noted. 3. The header information in each problem may not be used by an ATP without explicit notice. Any information other than that in the "input_clause"s, that is given to an ATP, must be explicitly noted. 4. The TPTP version, edition, and patch level must be explicitly noted. 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 clauses. 4. You have further suggestions for improvement regarding 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. If you do use the TPTP, please acknowledge this in anything that you publish or distribute (we would like to maintain the TPTP as the common source from which people work, such as to maintain consistency within the ATP community). Acknowledgements. We are indebted to: ---------------- Geoff Alexander, for helping with the SPRFN problems. ANL, esp. Bill McCune, for lots of problems and help. Dan Benanav, for his Hilbert geometry problems. Woody Bledsoe, for providing and helping with the LIM+ problems. Thomas Ludwig, for finding errors in some TPTP problems. Xumin Nie, for explaining the meanings of some problems. David Plaisted, for the problems from the SPRFN distribution. Joachim Posegga, for sending his problems in. Art Quaife, for lots of set theory problems. Mark Stickel, for problems, advice, and comments. Bob Veroff, for a range of problems and comments. TC Wang, for his problems in analysis and number theory.