CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

TPTP: Problem Library for Automated Theorem Proving Systems

areas/reasonng/atp/problems/tptp/
*** This copy of the TPTP is not guaranteed to be the most *** *** recent. The most recent release is always available from *** *** one of the Origin sites listed below. *** The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a collection of test problems for Automated Theorem Proving systems (ATPs), using the clausal normal form of 1st order predicate logic. The TPTP aims to supply the ATP community 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. New generalized variants of those problems whose original presentation is hand-tailored towards a particular automated proof. 3. The availability of these problems via FTP in a general-purpose format, together with a utility to convert the problems to existing ATP formats. (Currently the METEOR, MGTP, OTTER, PTTP, SETHEO, and SPRFN formats are supported, and the utility can easily be extended to produce any format required.) 4. A comprehensive list of references and other interesting information on each problem. 5. General guidelines outlining the requirements for ATP system evaluation. 
See Also: 

   ftp://coral.cs.jcu.edu.au/users/GSutcliffe/WWW/TPTP.HTML
   http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html

Origin:   

   coral.cs.jcu.edu.au:/pub/research/tptp-library/   [137.219.17.4]
   flop.informatik.tu-muenchen.de:/pub/tptp-library/ [131.159.8.35]
Version: 1.1.3 (29-AUG-94); 1.1.1 (8-JUL-94) Copying: Copyright (c) 1993, 1994 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. See the readme.txt file for conditions of use. Updated: Mon Nov 28 15:42:29 1994 CD-ROM: Prime Time Freeware for AI, Issue 1-1 Bug Reports: See Contact Author(s): Geoff Sutcliffe Christian Suttner Contact: Geoff Sutcliffe Department of Computer Science James Cook University Townsville, Australia. Fax: +61 77 814029 OR Christian Suttner Institut fuer Informatik TU Muenchen D-80290 Muenchen, Germany Fax: +49 89 526502 Keywords: Authors!Sutcliffe, Authors!Suttner, Automated Reasoning!Problem Libraries, Automated Theorem Proving, METEOR, MGTP, OTTER, PTTP, Reasoning!Automated Reasoning, SETHEO, SPRFN, TPTP, Test Problems, Theorem Proving!Problem Libraries References: Suttner C., Sutcliffe G. (1993), The TPTP Problem Library (TPTP v1.1.1 - TR 8.7.94), Technical Report AR-94-03, Institut fuer Informatik, Technische Universitaet Muenchen, Munich, Germany; Technical Report 93/11, Department of Computer Science, James Cook University, Townsville, Australia.
Last Web update on Mon Feb 13 10:27:26 1995
AI.Repository@cs.cmu.edu