The TPTP Problem Library
for Automated Theorem Proving

by Geoff Sutcliffe
geoff@cs.miami.edu
 and Christian Suttner
christian@suttner.info

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:

The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results 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.

If you're new to all this, you might want to start at the TPTP and TSTP Quick Guide.

The current release of the TPTP Library is TPTP-v3.4.1
Download package, 132.1 Mbytes.
(Contains the problems, axiom sets, documents, and utilities.)

Online access to:
Basic information.
Individual problems.
Individual axiom sets.
All the TPTP documents
History of changes to the TPTP and the archive of previous versions.
Online access to the tptp2T utility.

Current information, available only online:
Bugged problems list (Bugs found in the current version)
Details about the TPTP. Read this whenever you have a question about the TPTP.
The very latest updated BNF for the TPTP language.

TPTP subprojects:
Services for solving problems and recommending systems.
The TSTP (Thousands of Solutions from Theorem Provers) Solution Library is a library of solutions to test problems for automated theorem proving (ATP) systems. In particular, it contains solutions to TPTP problems.
The TPTP is used to supply problems for the CADE ATP System Competition.
  • $100 Challenges
Make money with ATP ...
  • TPTP Proposals
We are working on several new features for the TPTP, as explained in the following proposals. Comments from potential users will be appreciated.
  • TPTP Software
Many people have written software for processing TPTP format data. These links point to software I know of (please send your link if you have some software to add to the list).
  • Geoff's Service Tools. A bunch of tools for manipulating the TPTP, including the JJ parser for the TPTP language (named after the Spanish software developers, Justo Fernandez Reche and José Taboada Berenguer). The JJ parser will parse TPTP files and build a useful data structure, and there are lots of "useful" API functions for interrogating and manipulating the data structure. There is no documentation for any of this yet, but the sample drivers illustrate how to use the JJ parser API.
  • Stephan Schulz's E prover
  • Andrei Tchaltsev's Reusable TPTP parser in Java
We are collecting references for papers that cite the TPTP. If you have cited the TPTP in any of your work that is not yet included, we'd like to add your reference. If you would like to cite the TPTP, please use: 
@Article{SS98,
    Author       = "Sutcliffe, G. and Suttner, C.B.",
    Year         = "1998",
    Title        = "{The TPTP Problem Library: CNF Release v1.2.1}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "21",
    Number       = "2",
    Pages        = "177-203",
    Comment      = "REAL,ATPProgress,SystemOnTPTP,TPTPCite"
}

  • TPTP Tea Party
This approximately-annual meeting is used to to discuss the TPTP and related issues.

Other people are doing similar things for other types of ATP problems:
An environment for submitting and archiving benchmarking Answer-Set Programming (ASP) problems and instances, in which ASP systems can be run under equal and reproducible conditions, leading to independent results.
The Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem proving (ATP) systems for first-order and propositional intuitionistic logic.
TPDB is a library of test problems for termination provers. Currently, it includes termination problems for Term rewrite systems and logic programs.
Louise Dennis maintains a collection of induction challenge problems.
Ian Green maintains the Dream corpus of inductive conjectures. This is a corpus of approximately 1000 conjectures and associated definitions.
Holger Hoos and Thomas Stuetzle maintain a collection of benchmark problems, solvers, and tools for SAT related research.
Laurent Simon is gathering experiments and providing execution traces of provers on all benchmarks that are provided.
Toby Walsh, Ian Gent, and Bart Selman are putting together a benchmark library of problems for the constraints community, called CSPLib. The main motivation for CSPLib is to focus research in constraints away from purely random problems and onto more structured problems.
QBFLIB is a collection of benchmark problems, solvers, and tools related to Quantified Boolean Formula (QBF) satisfiability. QBFLIB is meant as a service to the QBF research community and its main goal is to provide an uniform test-bed for the empirical characterization of QBF solvers.

There were 682 unique visitors to the James Cook University site, 1 January 2001 to 21 March 2001. Then the site moved to the University of Miami. Unique visitors to the University of Miami site since 21 March 2001: