prolog - プロローグの否定

Question

さて、私はなぜそれが機能するのか疑問に思っています、そこではプロローグは変数を失います。

?- \+ \+ member(X,[a]),X=b.
X=b.

ここで、X=aです。自動的に消えました。

Answer 1

\+/1論理的な意味での「ない」ではなく、「失敗としての否定」によって実装されます。つまり、失敗しても\+ Goal成功するということです。Goal

\+/1次のように実装されていると考えてください。

\+(Goal) :- Goal -> fail ; true.

ご覧のとおり、どちらの場合も変数Goalが束縛されることはありません。「if」ブランチでは、バックトラックによってバインドが元に戻され、「else」ブランチでは、バインドされた変数はありません。

あなたの例では、member(X,[a]にバインドXすることで成功しますa。これは\+ member(X,[a])失敗し、\+\+ member(X,[a])この失敗のために成功します。中間故障のため、Xに拘束されませんa。

Answer 2

(\+)/1プロローグの演算子は、証明できないことを表すと想定(not)/1されていますが、古い演算子に対応しています。したがって、基本的にここで行っていることは次のとおりです。

not not member(X, [a]), X = b.

編集

Xが を含むリストである場合a、 の二重否定は、否定がない場合member(X, [a])と同じ結果になりmember(X, [a])ます。、リストX = bにバインドするだけです。bX

また、すべての Prolog 述語とその意味のリストがある、ブックマークしたリンクもここにあります。

お役に立てれば