私は、Prologの実装が教科書の実行モデルに従って動作しない理由を理解しようとしています。たとえば、SterlingandShapiroの「TheArtofProlog」（第6章「PureProlog」、セクション6.1、 「プロローグの実行モデル」）。
私が参照している実行モデルは次のとおりです（Sterling＆Shapiroの93ページ）。
入力：目標GとプログラムP
出力： Pの論理的帰結である、またはそれ以外の場合はないGのインスタンス
アルゴリズム：
Initialize resolvent to the goal G
while resolvent not empty:
choose goal A from resolvent
choose renamed clause A' <- B_1, ..., B_n from P
such that A, A' unify with mgu θ
(if no such goal and clause exist, exit the "while" loop)
replace A by B_1, ..., B_n in resolvent
apply θ to resolvent and to G
If resolvent empty, then output G, else output NO
さらに（同じ本の120ページ）、Prologはchoose goal A左から右の順序で目標（）を選択choose renamed clause ...し、プログラムに表示される順序で句（）を検索します。
not以下のプログラムには、 （プログラムで呼び出される）の定義nと1つの事実があります。
n(X) :- X, !, fail.
n(X).
f(a).
私が証明しようとするn(n(f(X)))と、それは成功します（2つの教科書とSWI Prolog、GNU Prolog、Yapによると）。しかし、これは少し奇妙ではありませんか？いくつかの本が公開しているその実行モデルによると、これは私が起こると予想されることです（とにかく競合がないので、物事を単純に保つために変数の名前変更をスキップします）：
レゾルベント：
n(n(f(Z)))統合
Xは最初の節で。と一致しn(f(Z))、ゴールをその節の末尾に置き換えます。レゾルベント：
n(f(Z)), !, fail。統一
Xは、最初の節で再び一致f(Z)し、レゾルベントの最初の目標を節の末尾に置き換えますレゾルベント：
f(Z), !, fail, !, fail。統一マッチ
f(Z)->成功！これで、これはレゾルベントから削除されます。レゾルベント：
!, fail, !, fail。
そして「 」は成功しない!, fail, !, failはずです！カット後、失敗があります。物語の終わり。（そして実際、クエリとして入力すると、私がアクセスできるすべてのPrologシステムで失敗します）。!,fail,!,fail
それで、教科書の実行モデルは、Prologが正確に使用しているものではないと推測できますか？
編集：最初の句を変更して、n(X) :- call(X), !, fail試したすべてのプロローグに違いがないようにします。