定理証明器のための数千もの問題

TPTP (Thousands of Problems for Theorem Provers) ^{[ 1 ]}は、自動定理証明のための無料で利用できる問題集です。これは、自動推論アルゴリズムの有効性を評価するために使用されます。^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}問題は、一階述語論理または高階述語論理のシンプルなテキストベースの形式で表現されます。^{[ 5 ]} TPTP は、 CASCの一部の問題のソースとして使用されています。

参考文献

↑ 「自動定理証明のためのTPTP問題ライブラリ」。
↑ 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 (2003 年 9 月) 「高階論理定理証明器における一階証明戦術」。Archer, Myla、De Vito, Ben、Muñoz, César (編)『Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences (PDF) 』。会議出版物。Vol. NASA/CP-2003-212448。NASA 科学技術情報プログラムオフィス。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 – 高階論理のためのTPTP言語の中核". 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] 「自動定理証明のためのTPTP問題ライブラリ」。

[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 (2003 年 9 月) 「高階論理定理証明器における一階証明戦術」。Archer, Myla、De Vito, Ben、Muñoz, César (編)『Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences (PDF) 』。会議出版物。Vol. NASA/CP-2003-212448。NASA 科学技術情報プログラムオフィス。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 – 高階論理のためのTPTP言語の中核". 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 ]

参考文献

外部リンク

関連するトピック

は、自動定理証明

TPTP は、 CASC

CiteSeerX

doi