Thousands of Problems for Theorem Provers explained

TPTP (Thousands of Problems for Theorem Provers)^[1] is a freely available collection of problems for automated theorem proving. It is used to evaluate the efficacy of automated reasoning algorithms.^{[2] [3] [4]} Problems are expressed in a simple text-based format for first order logic or higher-order logic.^[5] TPTP is used as the source of some problems in CASC.

Notes and References

1. Web site: The TPTP Problem Library for Automated Theorem Proving.
2. Book: Comparing Unification Algorithms in First-Order Theorem Proving. 2009. Hoder . Kryštof . Voronkov . Andrei . KI 2009: Advances in Artificial Intelligence. Lecture Notes in Computer Science. 5803. 435–443. 10.1007/978-3-642-04617-9_55 . 978-3-642-04616-2. https://www.researchgate.net/publication/221562903. 10.1.1.329.1809 .
3. First-Order Proof Tactics in Higher-Order Logic Theorem Provers . 2003. Hurd . Joe . 11201048 .
4. Using Hundreds of Workstations to Solve First-Order Logic Problems . 1994 . Segre . Alberto Maria. Sturgill . David B. . AAAI-94 Proceedings..
5. Book: THF0 – The Core of the TPTP Language for Higher-Order Logic . 2008 . Benzmüller . Christoph . Rabe . Florian . Sutcliffe . Geoff . Automated Reasoning . Lecture Notes in Computer Science . 5195 . 491–506 . 10.1007/978-3-540-71070-7_41. 978-3-540-71069-1 .