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
  1. "The TPTP Problem Library for Automated Theorem Proving".
  2. Hoder, Kryštof; Voronkov, Andrei (2009). "Comparing Unification Algorithms in First-Order Theorem Proving". CiteSeerX 10.1.1.329.1809. doi:10.1007/978-3-642-04617-9_55. Cite journal requires |journal= (help)
  3. Hurd, Joe (2003). "First-Order Proof Tactics in Higher-Order Logic Theorem Provers". Cite journal requires |journal= (help)
  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". doi:10.1007/978-3-540-71070-7_41. Cite journal requires |journal= (help)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.