Loading article…
Prover9 は、William McCuneによって開発された、一階述語論理および等式論理の自動定理証明器です。
説明
Prover9は、ウィリアム・マッキューンが開発したオッター定理証明器の後継です。[1] : 1 Prover9は、比較的読みやすい証明を生成し、強力なヒント戦略を備えていることで知られています。[1] : 11
Prover9 は、有限モデルと反例を検索するMace4と意図的にペアになっています。どちらも同じ入力から同時に実行することができ、[2] Prover9 は証明を見つけようとし、Mace4 は（反証となる）反例を見つけようとします。Prover9、Mace4、および他の多くのツールは、実装を簡素化するために LADR ("Library for Automated Deduction Research") という基礎ライブラリ上に構築されています。結果として得られる証明は、ACL2 を使用して別途検証された証明チェックツールである Ivy によって二重チェックできます。
2006 年 7 月、LADR/Prover9/Mace4 入力言語に大きな変更が加えられました (これも Otter との違いです)。「節」と「式」の主な違いは完全になくなりました。「式」は自由変数を持つことができ、「節」は「式」のサブセットになりました。Prover9/Mace4 は「目標」タイプの式もサポートしており、これは証明のために自動的に否定されます。Prover9 はデフォルトで証明を自動的に生成しようとしますが、Otter の自動モードは明示的に設定する必要があります。
Prover9 は 2009 年まで活発に開発され、毎月または隔月で新しいリリースが行われました。Prover9 はフリー ソフトウェアであり、したがってオープン ソース ソフトウェアであり、 GPLバージョン 2 以降 に基づいてリリースされています。
例
ソクラテス
伝統的な「人間は皆死ぬ」という証明、「ソクラテスは人間である」は、箴言9では次のように表現できます。
式(仮定)。man
( x ) - > mortal ( x )。 % 自由変数 x を持つオープン式
man (ソクラテス)。
リストの終わり。
公式(目標) 。
死すべき者(ソクラテス) 。
リストの終わり。
これは自動的に節形式に変換されます（Prover9 でも受け入れられます）。
式( sos )。-
人間( x ) | 死す べき者( x )。
人間(ソクラテス)。-
死すべき者(ソクラテス)。
リストの終わり。
2の平方根は無理数である
2の平方根が無理数であることの証明は次のように表現できる: [3]
式(仮定)。
1 * x = x 。 % 恒等式
x * y = y * x 。 % 交換法則
x* ( y * z ) = ( x * y ) * z 。 % 結合法則
( x * y = x * z ) -> y = z 。 % 消去法則 (0 は許可されないため、x!=0)。
%
% では、divides(x,y) を定義しましょう。 x は y を割り切ります。
% 例: 2*3=6 なので、divides(2,6) は true です。
%
除算( x 、y ) <-> ( z x * z = yが存在します )。除算( 2 、x * x ) ->除算( 2 、x )。% 2 が x*x を割り切る場合、x も割り切れます。a * a = 2 * ( b * b )。% a/b = sqrt(2) なので、a^2 = 2 * b^2 です。( x ! = 1 ) -> - (除算( x 、a )および除算( x 、b ))。% a/b は最小の項では2 ! = 1です。 % 元の著者はこれを忘れるところでした。リストの終わり。
参考文献
- ^ ab Phillips, JD; Stanovsky, David. 「ループ理論における自動定理証明」(PDF)。チャールズ大学。 2018年3月28日時点のオリジナルよりアーカイブ(PDF) 。 2018年11月15日閲覧。
- ^ Berghammer, Rudolf; Struth, Georg (2010 年 6 月 21 日)。「自動プログラム構築と検証について」( PDF)。Bolduc, Claude、Desharnais, Jules、Ktari, Bechir (編)。プログラム構築の数学、議事録。第 10 回国際会議、 MPC 2010。ケベック市。doi :10.1007/978-3-642-13321-3。ISBN 978-3-642-13320-6. S2CID 6962311. 2018年11月19日時点の オリジナル（PDF）からアーカイブ。2018年11月19日閲覧。
- ^ Wheeler, David A. 「sqrt2.in」。David A. Wheelerの個人ホームページ。 2016年3月14日閲覧。
外部リンク
- Prover9ホームページ
- Prover9 – Mace4 – LADR フォーラム
- 形式手法（2の平方根の例）