The TPTP Problem Library
|by||Geoff Sutcliffe||and||Christian Suttner|
The TPTP (Thousands of Problems for Theorem Provers) 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 capabilities of the ATP systems 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.|
You could also work your way through the slides of the TPTP World Tutorial.
The TPTP Needs Money ||If your work benefits from use of the TPTP and related projects, consider making an annual cash donation of 100 units of a reasonable currency, to support the TPTP. A donation can be made as an unrestricted gift (tax deductable) to the University of Miami, explicitly to support the TPTP and related projects. Read about the benefits and process of making a donation. A premium support contract is also available.|
|The current release of the TPTP Library is TPTP-v8.0.0 (Fri Apr 22 16:31:02 EDT 2022)|
| Download package, 808MB, expands to 9.1GB.
(Contains the problems, axiom sets, documents, and utilities.)|
|Online access to:|
|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 hyperlinked BNF for the TPTP language.|
If you would like to cite the TPTP, please use:
|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 TMTP (Thousands of Models for Theorem Provers) Model Library is a library of models of axiomatizations for automated theorem proving (ATP) systems. In particular, it contains models for TPTP axiomatizations.|
| The TPTP is used to supply problems for the CADE ATP System
|| We are working on new features for the TPTP, as explained
in the following proposals.
Comments from potential users will be appreciated.
|| 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).
|| 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:
|| Case studies that require induction.
|| Benchmark verification tasks in software verification, as used
|| This website features a series of notebooks presenting some of
Larry Wos’s most recent and hitherto unpublished research in
automated reasoning (also in 1st order logic).
|| The major goal of SMT-LIB is to establish a library of benchmarks
for Satisfiability Modulo Theories, that is, satisfiability of
formulas with respect to background theories for which specialized
decision procedures exist.
|| The Quantified Modal Logics Theorem Proving (QMLTP) library
provides a platform for testing and benchmarking automated
theorem proving (ATP) systems for first-order modal logics.
|| The Dozens of Problems for Partial Deduction (DPPD) Library of
Benchmarks aims at being a standard suite of benchmarks for partial
|| 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
|| 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.
|| The Termination Problems Database is a library of test problems
for termination provers.
Currently, it includes termination problems for term rewrite
systems and logic programs.
|| A benchmark library of problems for the constraints community.
The main motivation for CSPLib is to focus research in constraints
away from purely random problems and onto more structured problems.
|| A collection of test data sets for a variety of Operations
Research (OR) problems.
|| The Project Scheduling Problem Library.
|| The graph matching library, developed mainly to test the VF
graph matching algorithm, and to compare it with other known
|| A collection of benchmark problems, solvers, and tools for SAT
|| Experiments and execution traces of SAT solvers, on all benchmarks
that are provided.