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.1.2 (Mon Oct 17 14:51:04 EDT 2022)|
| Download package, 912MB, expands to 10.3GB.
(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.|
|Extra details and examples of TXF and THF extended features.|
|The very latest hyperlinked BNF for the TPTP language.|
If you would like to cite the TPTP, please use: