Thousands of Problems for Theorem Provers

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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.

References

^ "The TPTP Problem Library for Automated Theorem Proving".
^ Hoder, Kryštof; Voronkov, Andrei (2009). "Comparing Unification Algorithms in First-Order Theorem Proving". KI 2009: Advances in Artificial Intelligence. Lecture Notes in Computer Science. Vol. 5803. pp. 435–443. CiteSeerX 10.1.1.329.1809. doi:10.1007/978-3-642-04617-9_55. ISBN 978-3-642-04616-2.
^ Hurd, Joe (September 2003). "First-Order Proof Tactics in Higher-Order Logic Theorem Provers". In Archer, Myla; De Vito, Ben; Muñoz, César (eds.). Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences (PDF). Conference Publications. Vol. NASA/CP-2003-212448. NASA Scientific and Technical Information Program Office. pp. 56–68. S2CID 11201048.
^ Segre, Alberto Maria; Sturgill, David B. (1994). "Using Hundreds of Workstations to Solve First-Order Logic Problems" (PDF). AAAI-94 Proceedings.
^ Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff (2008). "THF0 – The Core of the TPTP Language for Higher-Order Logic". Automated Reasoning. Lecture Notes in Computer Science. Vol. 5195. pp. 491–506. doi:10.1007/978-3-540-71070-7_41. ISBN 978-3-540-71069-1.

External links

Official website

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

[1] "The TPTP Problem Library for Automated Theorem Proving".

[2] Hoder, Kryštof; Voronkov, Andrei (2009). "Comparing Unification Algorithms in First-Order Theorem Proving". KI 2009: Advances in Artificial Intelligence. Lecture Notes in Computer Science. Vol. 5803. pp. 435–443. CiteSeerX 10.1.1.329.1809. doi:10.1007/978-3-642-04617-9_55. ISBN 978-3-642-04616-2.

[3] Hurd, Joe (September 2003). "First-Order Proof Tactics in Higher-Order Logic Theorem Provers". In Archer, Myla; De Vito, Ben; Muñoz, César (eds.). Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences (PDF). Conference Publications. Vol. NASA/CP-2003-212448. NASA Scientific and Technical Information Program Office. pp. 56–68. S2CID 11201048.

[4] Segre, Alberto Maria; Sturgill, David B. (1994). "Using Hundreds of Workstations to Solve First-Order Logic Problems" (PDF). AAAI-94 Proceedings.

[5] Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff (2008). "THF0 – The Core of the TPTP Language for Higher-Order Logic". Automated Reasoning. Lecture Notes in Computer Science. Vol. 5195. pp. 491–506. doi:10.1007/978-3-540-71070-7_41. ISBN 978-3-540-71069-1.

[1]

[2]

[3]

[4]

[5]