Thousands of Problems for Theorem Provers

Short description: Collection of problems for Automated Theorem Proving

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". http://www.tptp.org/.
↑ 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. 5803. pp. 435–443. doi:10.1007/978-3-642-04617-9_55. ISBN 978-3-642-04616-2. https://www.researchgate.net/publication/221562903.
↑ Hurd, Joe (September 2003). "Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences". in Archer, Myla; De Vito, Ben; Muñoz, César. NASA/CP-2003-212448. NASA Scientific and Technical Information Program Office. pp. 56–68. https://ntrs.nasa.gov/api/citations/20030067561/downloads/20030067561.pdf.
↑ Segre, Alberto Maria; Sturgill, David B. (1994). "Using Hundreds of Workstations to Solve First-Order Logic Problems". AAAI-94 Proceedings.. https://www.aaai.org/Papers/AAAI/1994/AAAI94-029.pdf.
↑ 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. 5195. pp. 491–506. doi:10.1007/978-3-540-71070-7_41. ISBN 978-3-540-71069-1.

External links

No URL found. Please specify a URL here or add one to Wikidata.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Thousands of Problems for Theorem Provers. Read more

[1] "The TPTP Problem Library for Automated Theorem Proving". http://www.tptp.org/.

[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. 5803. pp. 435–443. doi:10.1007/978-3-642-04617-9_55. ISBN 978-3-642-04616-2. https://www.researchgate.net/publication/221562903.

[3] Hurd, Joe (September 2003). "Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences". in Archer, Myla; De Vito, Ben; Muñoz, César. NASA/CP-2003-212448. NASA Scientific and Technical Information Program Office. pp. 56–68. https://ntrs.nasa.gov/api/citations/20030067561/downloads/20030067561.pdf.

[4] Segre, Alberto Maria; Sturgill, David B. (1994). "Using Hundreds of Workstations to Solve First-Order Logic Problems". AAAI-94 Proceedings.. https://www.aaai.org/Papers/AAAI/1994/AAAI94-029.pdf.

[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. 5195. pp. 491–506. doi:10.1007/978-3-540-71070-7_41. ISBN 978-3-540-71069-1.

[1]

[2]

[3]

[4]

[5]