プロローグを使用した定理証明

Question

プロローグを使用して定理証明を書くにはどうすればよいですか？

私はこのようなことは、通常の書き込みをしようとしている：

parallel(X,Y):-perpendicular(X,Z),perpendicular(Y,Z), X\==Y,!. 
perpendicular(X,Y):-perpendicular(X,Z),parallel(Z,Y),!. 

あなたは私を助けることができますか？

Answer 1

この質問には枠がついていないため、私は回答を投稿することを嫌っていました。クリーンなフォーマットを追加するためのTheJollySinに感謝します！ Amanが心に持っていたことを示す書き換えで何かが省略されたのは、「私はループ内にいる」（SIC）だった。

このループの原因となったクエリが入力されているかどうかわからないため、投機が必要です。 2つのルールは、ゴールがパラレル/ 2または直交/ 2述語のいずれかを含むことを示唆しています。

実際には、クエリがポーズされたときにPrologエンジンが実行する処理、特に単一の目標クエリを理解するのは難しくありません。 Prologは、目標を達成するために非常に単純な「あなたの鼻に従う」戦略を使用します。どの述語が呼び出されたかのルールを探します。次に、それらのルールのうちの最初のルールから始まり、それらのルールの中に入るルールが適用可能かどうかを確認します。

Prologプログラマーの初めから一般的には苦労しているトピックが3つあります。 1つは、Prologエンジンが行う検索の再帰的性質です。/2垂直のためだけのルールは、それ自体のためのサブゴールおよびパラレル/用の別のサブゴールの両方を起動しながら、ここで/ 2平行ための唯一のルールは、/ 2垂直のための2つのサブゴールを呼び出す右側を有します2。いずれかの種類のクエリーを満足させると必然的に、分岐頭部との闘いがa Hydra-likeになることが予想されます。

この例で2番目に表示されるトピックは、フリー変数の使用です。 2つの直交性または並列性についての知識を得るためには、何らかの形でクエリまたはルールが変数を「グラウンド」の用語に「バインディング」する必要があります。再び実際の目標を照会することなく、Amanがそれをどのように期待しているかを推測するのは難しいです。おそらく、垂直または平行である特定の線について「事実」が供​​給されていたはずです。行は単に原子（小文字）として表すことができますが、Prolog変数は大文字（2つの規則のように）またはアンダースコア（_）で始まる名前です。

最後に、Prologがネゲートを処理する方法が非常に混乱する可能性があります。これらのルールには、X\==Yが呼び出される場所に触れるだけです。しかし、その短いサブゴールでさえ、慎重な理解が必要です。 Prologは「否定を失敗として」実装するため、X==Y does not succeedの場合にのみX\==Yが成功します。 XとYが統一を試みることなく同じであるかどうかを尋ねるので、この後者の目標も微妙です。したがって、これらが異なる変数であれば、両方とも空きの場合は、X==Yが失敗し（X\==Yが成功します）。一方、X==Yが成功する唯一の方法（したがって、X\==Yが失敗する）は、両方の変数が同じ基本条件にバインドされている場合に発生します。上で議論したように、2つのルールはそのような場合のための方法を提供しませんが、クエリーの目的でこれが何かを処理したかもしれません。

• 再帰
• 自由と束縛変数
• 否定

はおそらく、より具体的な提案は、約行うことができます。

アマンのための宿題は、これらのPrologのトピックについて学ぶことですジオメトリプルーフを行うプロローグ！

追加： PTTP（Prolog Technology Theorem Prover）は1980年代後半にM.E. Stickelによって書かれました。this 2006 web pageはそれを記述してダウンロードにリンクします。

また、Prologが単独の「汎用汎用定理証明システム」でない理由を簡単にまとめています。後でもっと能力の高い定理証明者へのポインタもここに従うことができます。