Prologの否定と論理否定

Question

は、我々は次のプログラムがあるとします。

a(tom). 
v(pat). 

と（falseを返す）問い合わせ：

\+ a(X), v(X). 

トレースするとき、私はXがトムにインスタンス化になっていることがわかります述語a（tom）は成功し、したがって+ a（tom）は失敗します。

私は、Prologのnot（+）が単なるテストであり、インスタンス化を引き起こさないというチュートリアルを読んでいます。

1. 誰かが私のために上記の点を明確にしてもらえますか？私はインスタンス化を見ることができます。

2. 私は、否定（失敗としての否定）と論理否定の間に違いがあることを理解します。どの記事が同じように振る舞い、どのような振る舞いが違うのかを説明する良い記事を参照できますか？

Answer 1

WRTポイント2、Wikipedia articleが良い開始点のようです。

NAFの理解が困難な場合があります。これは、（論理的）否定は、述語計算（例えば、Russel's paradoxを参照）とPrologの強力な変数が実際の反例を維持するためには、を無効にした場合に失敗するという単純なコンテストでも定義するのが本質的に難しいためです。証拠。私は最初の時間を覚えて

%% forall(+Condition, +Action) 
% 
% True if Action if true for all variable bindings for which Condition 
% if true. 

forall(Cond, Action) :- 
    \+ (Cond, \+ Action). 

：あなたはforall/2の実際のライブラリーの定義を理解することができればそれは失敗駆動ループを実行するための好ましい方法です（、ドキュメントを読んで、それを合成し、面白いしてください）を参照してください。 JRFisherで私のリンク集、良いsiteを「洞窟探検」しながら、それを見た、それは...魔法のようにチュートリアルについて

編集を見て、私は、発見しました。それは面白いものがいっぱいです。説明にはちょっと残念ですが、生徒に頻繁に執拗に答える必要があります。失敗による否定に向けたparagraph 2.5を参照してください。私はセクション3も楽しめると思います。プロローグの仕組み

Answer 2

大きな質問です。

短い答え：あなたは "ひっかく"に遭遇しました。

問題、すなわち、地面 リテラル、いかなる変数を含まないリテラルに適用した場合にオペレータ\ +の実装のみ を動作することです。変数のバインディングを生成することはできませんが、サブゴールが成功するか失敗するかをテストするのは だけです。妥当性を保証するには、否定を含むプログラムへの問い合わせに対する回答を にするには、否定 オペレータは地上リテラルだけに適用する必要があります。 がnongroundリテラルに適用されている場合、プログラムは詐欺と言われます。 link

クエリ

v(X), \+ a(X).

を反転した場合あなたは正しい答えを得るでしょう。実装やメタインタプリタの中には、あいまいな目標を検出し、すべての変数が解決されるまで遅延させるものがあります。

あなたのポイントについて1）、あなたはNAFツリー内のインスタンス化を参照してください。そこに起こることは、外側にある変数（この場合はv（X））に影響を与えるべきではありません。プロローグは、しばしば、非効率を避けるために素朴な方法で行動します。理論的には、変数をインスタンス化する代わりにエラーを返してください。

2）これはトピックに関する私の好きな記事です：Nonmonotonic Logic Programmingです。