Loading article…
E は、等式付き完全一階論理のための高性能な定理証明器です。 [1]これは、等式重ね合わせ計算に基づいており、純粋に等式のパラダイムを使用しています。他の定理証明器に統合されており、いくつかの定理証明コンテストで最上位のシステムの 1 つとなっています。E は、もともとミュンヘン工科大学の自動推論グループに所属し、現在はバーデン＝ヴュルテンベルク州立大学シュトゥットガルト校に所属するStephan Schulz によって開発されました。
システム
このシステムは等式重ね合わせ計算に基づいています。現在の他のほとんどの証明器とは対照的に、実装では実際には純粋に等式的なパラダイムを使用し、適切な等式推論を介して非等式推論をシミュレートします。重要な革新には、共有項書き換え（多くの可能な等式簡略化が単一の操作で実行される）、[2]推論を高速化するためのいくつかの効率的な項インデックスデータ構造、高度な推論リテラル選択戦略、検索動作を改善するための機械学習技術のさまざまな使用などがあります。[2] [3] [4]バージョン2.0以降、Eは多ソートロジックをサポートしています。[5]
EはC言語で実装されており、ほとんどのUNIX系OSやCygwin環境に移植可能です。GNU GPLの下で利用可能です。[6]
競技会
この証明器はCADE ATPシステムコンペティションで一貫して優れた成績を収めており、2000年にCNF/MIXカテゴリーで優勝し、それ以来常にトップシステムの1つとなっています。[7] 2008年には2位になりました。[8] 2009年にはFOF（完全一階述語論理）とUEQ（単位等式論理）カテゴリーで2位、CNF（節論理）で3位（ヴァンパイアの2つのバージョンに次ぐ）を獲得しました。 [9] 2010年にはFOFとCNFで同様の成績を収め、「総合最優秀」システムとして特別賞を受賞しました。[10] 2011年、CASC-23 EはCNF部門で優勝し、UEQとLTBでも2位を獲得しました。[11]
アプリケーション
Eは他のいくつかの定理証明器にも統合されている。Vampire 、SPASS、CVC4、Z3とともに、 IsabelleのSledgehammer戦略の中核をなしている。 [12] [ 13] EはSInE [14]やLEO-II [15]の推論エンジンでもあり、iProverの節化システムとして使用されている。[16]
Eの応用としては、大規模オントロジーの推論[17] 、ソフトウェア検証[18] 、ソフトウェア認証[19]などがある。
参考文献
- ^ Schulz, Stephan (2002). 「E – ブレイニアック定理証明器」. Journal of AI Communications . 15 (2/3): 111–126.
- ^ ab 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」.自動推論. コンピュータサイエンスの講義ノート. 第3097巻. pp. 223–228. doi :10.1007/978-3-540-25984-8_15. ISBN 978-3-540-22345-0。
- ^ Schulz, Stephan (2001)。「等式定理証明のための探索制御知識の学習」。KI 2001: 人工知能の進歩。コンピュータサイエンスの講義ノート。第 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). 「E 等式定理証明器」2009 年3 月 24 日閲覧。
- ^ Sutcliffe, Geoff. 「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). 「CADE ATP System Competition」. マイアミ大学. 2010年6月29日時点のオリジナルよりアーカイブ。2010年7月20日閲覧。
- ^ Sutcliffe, Geoff (2011). 「CADE ATP System Competition」. マイアミ大学. 2011年8月12日時点のオリジナルよりアーカイブ。2011年8月14日閲覧。
- ^ Paulson, Lawrence C. (2008). 「対話型証明の自動化: テクニック、教訓、展望」(PDF)。システム インフラストラクチャの検証のためのツールとテクニック - Michael JC Gordon 教授を記念した記念論文集 FRS : 29–30 。 2009 年12 月 19 日閲覧。
- ^ Meng, Jia; Lawrence C. Paulson (2004). 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). The 4th IJCAR ATP System Competition (PDF) . 2009年6月17日時点のオリジナル(PDF)からアーカイブ。2009年12月18日閲覧。
- ^ Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). 「LEO-II – 古典的高階論理のための協調型自動定理証明器 (システム説明)」. 自動推論(PDF) . コンピュータサイエンスの講義ノート. Vol. 5195. Springer. pp. 162–170. doi :10.1007/978-3-540-71070-7_14. ISBN 978-3-540-71069-1. 2011年6月15日時点のオリジナル（PDF）からアーカイブ。2009年12月20日閲覧。
- ^ Korovin, Konstantin (2008). 「iProver - インスタンス化ベースの一階論理定理証明器」.自動推論. コンピュータサイエンスの講義ノート. 第 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: 常識オントロジーにおける表現力と効率性」(PDF)。AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications。AAAI。
- ^ Ranise, Silvio; David Déharbe (2003). 「軽量定理証明のポインタプログラムのデバッグと検証への適用」.理論計算機科学における電子ノート. 86 (1). 第4回国際第一階定理証明ワークショップ: 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の開発者