The TPTP Problem Library
|
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.
The current release of the TPTP Problem Library is TPTP-v9.0.0 (Sat Jun 1 19:35:01 EDT 2024) | |
• TPTP-v9.0.0.tgz |
Download package, 79MB, expands to 9.8GB.
(Contains the problems, axiom sets, documents, and utilities.) |
Online access to: | |
• ReadMe | Basic information. |
• Problems | Individual problems. |
• Axiom sets | Individual axiom sets. |
• Documents | All the TPTP documents |
• History and Archive | History of changes to the TPTP and the archive of previous versions. |
• SystemB4TPTP | Online access to SystemB4TPTP problem preparation. |
• SystemOnTPTP | Online access to SystemOnTPTP problem solving. |
• TPTP2T online | Online access to TPTP2T problem and solution selection. |
| |
Current information, available only online: | |
• Bug list | Bugged problems list (Bugs found in the current version) |
• Technical manual | Details about the TPTP. Read this whenever you have a question about the TPTP. |
• SyntaxBNF | The very latest hyperlinked BNF for the TPTP language. |
| |
If you would like to cite the TPTP problem library, please use: | @Article{Sut17, Author = "Sutcliffe, G.", Year = "2017", Title = "{The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0}", Journal = "Journal of Automated Reasoning", Volume = "59", Number = "4", Pages = "483-502" } |
If you would like to cite the TPTP logic languages, please use: | @Article{Sut22, Author = "Sutcliffe, G.", Year = "2022", Title = "{The Logic Languages of the TPTP World}", Journal = "Logic Journal of the IGPL", DOI = "10.1093/jigpal/jzac068" } |
| |
Other people are doing similar things for other types of ATP problems: | |
• SUMO | In TPTP format |
• The Mizar-TPTP | Semantic Presentation |
• VeriFun | Case studies that require induction. |
• SV-COMP | Benchmark verification tasks in software verification, as used in SV-COMP. |
• Larry Wos' Notebooks | 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). |
• SMT-LIB | 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. |
• QMLTP | 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. |
• ILTP | 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. |
• TPBD | 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. |
• CSPLib | 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. |
• OR-Library | A collection of test data sets for a variety of Operations Research (OR) problems. |
• SATLIB | A collection of benchmark problems, solvers, and tools for SAT related research. |
• QBFLib | QBFLIB is a collection of benchmark problems, solvers, and tools related to Quantified Boolean Formula (QBF) satisfiability. |