TPTP (Thousands of Problems for Theorem Provers)[1] とは自由に利用可能な自動定理証明のための問題集である。これは自動推論アルゴリズムの効率の評価のために使用される。 [2][3][4] 問題は一階述語論理や高階述語論理のためのシンプルなテキストベースの形式で表される。[5] TPTPはCASCの中で問題の収集元として使われている。
脚注^ “ ⇒The TPTP Problem Library for Automated Theorem Proving”. 2023年6月25日閲覧。
^ 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. .mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation.cs-ja1 q,.mw-parser-output .citation.cs-ja2 q{quotes:"「""」""『""』"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free a,.mw-parser-output .citation .cs1-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited a,.mw-parser-output .id-lock-registration a,.mw-parser-output .citation .cs1-lock-limited a,.mw-parser-output .citation .cs1-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription a,.mw-parser-output .citation .cs1-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:#d33}.mw-parser-output .cs1-visible-error{color:#d33}.mw-parser-output .cs1-maint{display:none;color:#3a3;margin-left:0.3em}.mw-parser-output .cs1-format{font-size:95%}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}ISBN 978-3-642-04616-2. https://www.researchgate.net/publication/221562903 
^ Hurd, Joe (2003). First-Order Proof Tactics in Higher-Order Logic Theorem Provers. https://www.semanticscholar.org/paper/First-Order-Proof-Tactics-in-Higher-Order-Logic-In-Hurd/a24fd4cf48276eecb3ca1254da97323aabb6dd7a. 
^ 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. 
^ Benzmuller, 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 

外部リンク

⇒TPTP Web site.