E（定理証明器）

Eは、等号を含む完全な一階述語論理のための高性能定理証明器です。^[¹^]等式重ね合わせ計算に基づいており、純粋に等式パラダイムを使用しています。他の定理証明器に統合されており、いくつかの定理証明コンテストで上位に入賞しています。E は、元々はミュンヘン工科大学の自動推論グループに所属し、現在はバーデン＝ヴュルテンベルク州立協同大学シュトゥットガルトに所属する Stephan Schulz によって開発されました。

システム

このシステムは等式重ね合わせ計算に基づいています。他のほとんどの現在の証明器とは対照的に、実装では実際に純粋に等式パラダイムを使用し、適切な等式推論を介して非等式推論をシミュレートします。重要な革新には、共有項書き換え（可能な多くの等式簡略化が単一の操作で実行される）、^{[ 2 ]}推論を高速化するためのいくつかの効率的な項インデックスデータ構造、高度な推論リテラル選択戦略、および検索動作を改善するための機械学習技術のさまざまな使用が含まれます。^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}バージョン 2.0 以降、E は多ソート論理をサポートしています。^{[ 5 ]}

EはC言語で実装されており、ほとんどの UNIX系システムとCygwin環境に移植可能です。GNU GPLライセンスで提供されています。^{[ 6 ]}

競技会

この証明器は、 CADE ATP システムコンペティションで一貫して優れた成績を収めており、2000 年に CNF/MIX カテゴリーで優勝し、それ以来常に上位システムに入っています。^{[ 7 ]} 2008 年には 2 位になりました。^{[ 8 ]} 2009 年に FOF (完全一階述語論理) と UEQ (単位等式論理) カテゴリーで 2 位、CNF (節論理)で3 位 ( Vampireの 2 バージョンに次ぐ) を獲得しました。 ^[⁹^] 2010 年に FOF と CNF で同様の成績を収め、「総合的に最優秀」システムとして特別賞を受賞しました。^[¹⁰^] 2011 年の CASC-23 E では、CNF 部門で優勝し、UEQ と LTB で 2 位を獲得しました。^[¹¹^]

アプリケーション

E は他のいくつかの定理証明器に統合されています。Vampire 、SPASS、CVC4、Z3とともに、 IsabelleのSledgehammer戦略の中核を成しています^。[12][13] E^は^SInE^[¹⁴^]および^LEO^-^II [ ¹⁵^]^の推論エンジンでもあり、 iProverの節化システムとしても使用されています。^[¹⁶^]

E の応用例としては、大規模オントロジー上での推論^{[ 17 ]} 、ソフトウェア検証^{[ 18 ]}、ソフトウェア認証^{[ 19 ]などがある。}

参考文献

↑ Schulz, Stephan (2002). "E – A Brainiac Theorem Prover". Journal of AI Communications . 15 (2/3): 111– 126.
1 2 Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre" . 2009年6月15日のオリジナルからアーカイブ済み。 2009年3月24日取得。
↑ Schulz, Stephan (2004). "システム記述: E 0.81".自動推論. Lecture Notes in Computer Science. Vol. 3097. pp. 223–228 . doi : 10.1007/978-3-540-25984-8_15 . ISBN 978-3-540-22345-0。
↑ Schulz, Stephan (2001). "等式定理証明のための探索制御知識の学習". KI 2001: 人工知能の進歩. Lecture Notes in Computer Science. Vol. 2174. pp. 320–334 . doi : 10.1007/3-540-45422-5_23 . ISBN 978-3-540-42612-7。
↑ 「Eのウェブサイトのニュース」。 2017年7月10日取得。
↑ Schulz, Stephan (2008). "The E Equational Theorem Prover" . 2009年3月24日取得。
↑ Sutcliffe, Geoff. "The CADE ATP System Competition" . 2009年3月2日時点のオリジナルよりアーカイブ。 2009年3月24日取得。
↑ 「2008年のCASCのFOF部門」。2009年6月15日にオリジナルからアーカイブ済み。2009年12月19日に取得。
↑ Sutcliffe, Geoff (2009). "第4回IJCAR自動定理証明システムコンペティション--CASC-J4" . AI Communications . 22 (1): 59– 72. doi : 10.3233/AIC-2009-0441 . 2009年12月16日取得.
↑ Sutcliffe, Geoff (2010). "The CADE ATP System Competition" . マイアミ大学。2010年6月29日のオリジナルからアーカイブ済み。 2010年7月20日取得。
↑ Sutcliffe, Geoff (2011). "The CADE ATP System Competition" . マイアミ大学。2011年8月12日のオリジナルからアーカイブ済み。 2011年8月14日取得。
↑ Paulson, Lawrence C. (2008). "対話型証明のための自動化: 技術、教訓、展望" (PDF) . Tools and Techniques for Verification of System Infrastructure – A Festschrift in Honour of Professor Michael JC Gordon FRS : 29– 30 . 2009年12月19日取得。
↑ Meng, Jia; Lawrence C. Paulson ( 2004). Experiments on Supporting Interactive Proof Using Resolution . Lecture Notes in Computer Science. Vol. 3097. Springer. pp. 372–384 . CiteSeerX 10.1.1.62.5009 . doi : 10.1007/978-3-540-25984-8_28 . ISBN 978-3-540-22345-0。
↑ Sutcliffe, Geoff; et al. (2009).第4回IJCAR ATPシステム競技会(PDF) . 2009年6月17日にオリジナル(PDF)からアーカイブ済み。2009年12月18日に取得。
↑ Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). "LEO-II – 古典的高階論理のための協調型自動定理証明器（システム記述）". Automated Reasoning (PDF) . Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 162–170 . doi : 10.1007/978-3-540-71070-7_14 . ISBN 978-3-540-71069-12011年6月15日にオリジナル（PDF）からアーカイブされました。 2009年12月20日に取得。
↑ Korovin, Konstantin (2008). "iProver—一階述語論理のためのインスタンス化ベースの定理証明器". Automated Reasoning . Lecture Notes in Computer Science. Vol. 5195. pp. 292–298 . doi : 10.1007/978-3-540-71070-7_24 . ISBN 978-3-540-71069-1。
↑ Ramachandran, Deepak; Pace Reagan; Keith Goolsbery (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology" (PDF) . AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications . AAAI.
↑ Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs" . Electronic Notes in Theoretical Computer Science . 86 (1). 4th International Workshop on First-Order Theorem Proving: Elsevier: 109– 119. doi : 10.1016/S1571-0661(04)80656-X .{{cite journal}}: CS1メンテナンス: 場所 (リンク)
↑ Denney, Ewen; Bernd Fischer; Johan Schumann (2006). "ソフトウェア認証における自動定理証明器の経験的評価" . International Journal on Artificial Intelligence Tools . 15 (1): 81– 107. CiteSeerX 10.1.1.163.4861 . doi : 10.1142/s0218213006002576 . 2012年2月24日のオリジナルからアーカイブ済み。 2009年12月19日取得。

外部リンク

Eホームページ
Eの開発者

[brainiac-1] Schulz, Stephan (2002). "E – A Brainiac Theorem Prover". Journal of AI Communications . 15 (2/3): 111– 126.

[casc2008-2] 1 2 Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre" . 2009年6月15日のオリジナルからアーカイブ済み。 2009年3月24日取得。

[3] Schulz, Stephan (2004). "システム記述: E 0.81".自動推論. Lecture Notes in Computer Science. Vol. 3097. pp. 223–228 . doi : 10.1007/978-3-540-25984-8_15 . ISBN 978-3-540-22345-0。

[4] Schulz, Stephan (2001). "等式定理証明のための探索制御知識の学習". KI 2001: 人工知能の進歩. Lecture Notes in Computer Science. Vol. 2174. pp. 320–334 . doi : 10.1007/3-540-45422-5_23 . ISBN 978-3-540-42612-7。

[5] 「Eのウェブサイトのニュース」。 2017年7月10日取得。

[6] Schulz, Stephan (2008). "The E Equational Theorem Prover" . 2009年3月24日取得。

[7] Sutcliffe, Geoff. "The CADE ATP System Competition" . 2009年3月2日時点のオリジナルよりアーカイブ。 2009年3月24日取得。

[8] 「2008年のCASCのFOF部門」。2009年6月15日にオリジナルからアーカイブ済み。2009年12月19日に取得。

[casc2009-9] Sutcliffe, Geoff (2009). "第4回IJCAR自動定理証明システムコンペティション--CASC-J4" . AI Communications . 22 (1): 59– 72. doi : 10.3233/AIC-2009-0441 . 2009年12月16日取得.

[10] Sutcliffe, Geoff (2010). "The CADE ATP System Competition" . マイアミ大学。2010年6月29日のオリジナルからアーカイブ済み。 2010年7月20日取得。

[11] Sutcliffe, Geoff (2011). "The CADE ATP System Competition" . マイアミ大学。2011年8月12日のオリジナルからアーカイブ済み。 2011年8月14日取得。

[12] Paulson, Lawrence C. (2008). "対話型証明のための自動化: 技術、教訓、展望" (PDF) . Tools and Techniques for Verification of System Infrastructure – A Festschrift in Honour of Professor Michael JC Gordon FRS : 29– 30 . 2009年12月19日取得。

[13] Meng, Jia; Lawrence C. Paulson ( 2004). Experiments on Supporting Interactive Proof Using Resolution . Lecture Notes in Computer Science. Vol. 3097. Springer. pp. 372–384 . CiteSeerX 10.1.1.62.5009 . doi : 10.1007/978-3-540-25984-8_28 . ISBN 978-3-540-22345-0。

[14] Sutcliffe, Geoff; et al. (2009).第4回IJCAR ATPシステム競技会(PDF) . 2009年6月17日にオリジナル(PDF)からアーカイブ済み。2009年12月18日に取得。

[15] Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). "LEO-II – 古典的高階論理のための協調型自動定理証明器（システム記述）". Automated Reasoning (PDF) . Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 162–170 . doi : 10.1007/978-3-540-71070-7_14 . ISBN 978-3-540-71069-12011年6月15日にオリジナル（PDF）からアーカイブされました。 2009年12月20日に取得。

[16] Korovin, Konstantin (2008). "iProver—一階述語論理のためのインスタンス化ベースの定理証明器". Automated Reasoning . Lecture Notes in Computer Science. Vol. 5195. pp. 292–298 . doi : 10.1007/978-3-540-71070-7_24 . ISBN 978-3-540-71069-1。

[17] Ramachandran, Deepak; Pace Reagan; Keith Goolsbery (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology" (PDF) . AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications . AAAI.

[18] Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs" . Electronic Notes in Theoretical Computer Science . 86 (1). 4th International Workshop on First-Order Theorem Proving: Elsevier: 109– 119. doi : 10.1016/S1571-0661(04)80656-X .{{cite journal}}: CS1メンテナンス: 場所 (リンク)

[19] Denney, Ewen; Bernd Fischer; Johan Schumann (2006). "ソフトウェア認証における自動定理証明器の経験的評価" . International Journal on Artificial Intelligence Tools . 15 (1): 81– 107. CiteSeerX 10.1.1.163.4861 . doi : 10.1142/s0218213006002576 . 2012年2月24日のオリジナルからアーカイブ済み。 2009年12月19日取得。

[

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[

[

[

。[12][13]

は

LEO

15

[

[ 17 ]

[ 18 ]

[ 19 ]などがある。

システム

競技会

アプリケーション

参考文献

外部リンク

関連するトピック

一階述語論理

定理証明器

重ね合わせ計算

さ