Loading article…
| 原作者 | ウィリアム・マッキューン |
|---|---|
| 書かれた | Ｃ |
| タイプ | 自動定理証明 |
| Webサイト | www.mcs.anl.gov/research/projects/AR/otter/ |
Otter は、イリノイ州のアルゴンヌ国立研究所のWilliam McCuneによって開発された自動定理証明器です。Otter は、広く配布された最初の高性能な一階述語論理定理証明器であり、いくつかの重要な実装手法の先駆けとなりました。OtterはOrganized Techniques for Theorem-proving and Effective Researchの頭字語です。
説明
Otter は、重ね合わせ計算と同様の項順序によって制約される、解像度とパラモジュレーションに基づいています。この証明器は、正と負のハイパー解像度とサポート セット戦略もサポートしています。証明検索は、与えられた節アルゴリズムのバージョンを使用した飽和に基づいており、いくつかのヒューリスティックによって制御されます。検索パラメータを自動的に決定するメタヒューリスティックもあります。[1] Otter は、大規模な節セットでの推論パートナーの検索を高速化するために、効率的な項インデックス作成技術 の使用も開拓しました。[2]
Otter は長年にわたって非常に安定していますが、現在は積極的に開発されていません。2008 年 11 月現在、最後の変更ログ エントリは 2004 年 9 月 14 日付です。Otter の後継はProver9です。
このソフトウェアはパブリック ドメインです。シカゴ大学は、このソフトウェアの著作権を主張することを拒否しており、一般の人々が使用、変更、再配布 (変更の有無にかかわらず) することができます。ただし、「米国政府もそのいかなる機関も [...] このソフトウェアの使用が私有権を侵害しないことを表明しません。」[3]
WosとPieperによれば、OTTERは約28,000行のCプログラミング言語で書かれている。[4] : 89–91
参照
注記
- ^ McCune, William; Larry Wos (1997). 「Otter: CADE-13 競技会の化身」. Journal of Automated Reasoning . 18 (2): 211–220. doi :10.1023/A:1005843632307.
- ^ McCune, William (1992). 「用語検索のための識別木インデックスとパスインデックスの実験」。Journal of Automated Reasoning。9 ( 2): 147–167。doi :10.1007/BF00245458。
- ^ tarball内のファイル名
- ^ Wos, Larry; Pieper, Gail W. (1999)。「3.11 OTTERとそれ以前の自動定理証明プログラム」。コンピューティングの世界における魅力的な国: 自動推論ガイド。World Scientific。ISBN 978-9810239107。
参考文献
- カルマン、ジョン・アーノルド（2001年2月）。OTTERによる自動推論。Rinton Press。ISBN 978-1589490048。
外部リンク
- オッターホームページ
- 「OTTER 3.3 リファレンスマニュアル」(PDF)。2018 年 11 月 13 日にオリジナルからアーカイブ。2018 年 11 月 13 日に取得。
{{cite web}}: CS1 maint: bot: 元の URL ステータス不明 (リンク)