5

Prologs を使用して定理証明を作成するにはどうすればよいですか?

私はそれを普通に書こうとしました：

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

手伝って頂けますか？

4

1 に答える 1

4

この質問の枠組みが不十分なため、回答を投稿することを躊躇しました。クリーンなフォーマットを追加してくれたtheJollySinに感謝します！アマンが念頭に置いていたことを示す、書き直しで省略されたものは、「I inter inLoop」（原文のまま）でした。

このループの原因となったクエリが入力されたのかわからないため、推測が必要です。2つのルールは、目標が並列/2または垂直/2述語のいずれかを含むことを示唆しています。

練習すれば、クエリ、特に単一の目標クエリが提示されたときにPrologエンジンが何をするかを理解するのは難しくありません。Prologは、目標を達成しようとする際に、非常に単純な「鼻をたどる」戦略を使用します。呼び出される述語のルールを探します。次に、これらのルールのいずれかを、最初からリストの最後まで適用できるかどうかを確認します。

初心者のPrologプログラマーが通常苦労する3つのトピックがあります。1つは、Prologエンジンが行う検索の再帰的な性質です。ここで、parallel / 2の唯一のルールには、vertical / 2の2つのサブゴールを呼び出す右側があり、parently / 2の唯一のルールは、それ自体のサブゴールとparallel/2の別のサブゴールの両方を呼び出します。どちらかの種類のクエリを満たそうとすると、必然的に、分岐したヘッドとのHydraのような闘争につながることを期待する必要があります。

この例で見られる2番目のトピックは、自由変数の使用です。2つの特定の線（ジオメトリ）の垂直性または平行性についての知識を得る場合、クエリまたはルールは、変数の「グラウンド」用語への「バインド」を提供する必要があります。ここでも、実際の目標が照会されない限り、アマンがそれがどのように機能することを期待していたかを推測するのは困難です。おそらく、垂直または平行な特定の線について提供された「事実」があったはずです。行は単にアトム（おそらく小文字）として表すことができますが、Prolog変数は大文字（2つの与えられた規則のように）またはアンダースコア（_）文字で始まる名前です。

最後に、非常に混乱する可能性のある3番目のトピックは、Prologが否定を処理する方法です。これらのルールには、X\==Y呼び出される場所がほんの少ししかありません。しかし、その短いサブゴールでさえ、注意深い理解が必要です。Prologは「失敗としての否定」を実装しているので、成功しないX\==Y場合にのみ成功します。この後者の目標も微妙です。なぜなら、統一を試みなくても、とが同じであるかどうかを尋ねるからです。したがって、これらが異なる変数である場合、両方とも無料で、失敗します（そして成功します）。一方、成功するための唯一の方法（したがってX==YXYX==YX\==YX==YX\==Y失敗する）は、両方の変数が同じ基底項にバインドされている場合です。上で説明したように、前述の2つのルールは、それが当てはまる方法を提供していませんが、クエリの目標で何かがこれを処理した可能性があります。

アマンの宿題は、これらのプロローグのトピックについて学ぶことです。

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

おそらく、Prologが幾何学証明を行うことについてより具体的な提案をすることができます！

追加： PTTP（Prolog Technology Theorem Prover）は、1980年代後半にME Stickelによって作成されました。この2006年のWebページでは、PTTPとダウンロードへのリンクについて説明しています。

また、Prologだけが「完全な汎用定理証明システム」ではない理由を簡潔に要約します。後で、より有能な定理証明者へのポインタをそこにたどることもできます。

于 2012-04-18T15:37:20.410 に答える