mic_none

Thousands of Problems for Theorem Provers Source: en.wikipedia.org/wiki/Thousands_of_Problems_for_Theorem_Provers

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

[edit]
  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.
[edit]


Stub icon

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