TPTP (Thousands of Problems for Theorem Provers) is a freely available collection of problems for
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
. It is used to evaluate the efficacy of automated reasoning algorithms. Problems are expressed in a simple text-based format for first order logic or higher-order logic.
TPTP is used as the source of some problems in
CASC.
References
External links
Web site
Automated theorem proving
{{Mathlogic-stub