我想了解爲什麼Prolog實現不按照教科書中的執行模型行事 - 例如，Sterling和Shapiro的「The Prolog of Prolog」一書（第6，「Pure Prolog」，第6.1節，「Prolog的執行模型」）。Prolog中的雙重否定和執行模型
我所指的執行模型是這樣的（第93頁斯特林&夏皮羅的）：
輸入：一個目標G和程序P
輸出： G的實例爲P的邏輯結果，或不以其他方式
算法：
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）和一個單一的事實。
n(X) :- X, !, fail.
n(X).
f(a).
如果我試圖證明n(n(f(X)))，它成功（根據兩本教科書，並在SWI序言，序言GNU和邑）。但這不是很奇怪嗎？根據該執行模式，這幾本書揭露，這是我希望發生的（跳過的變量重命名讓事情變得簡單，因爲不會有什麼衝突呢）：
預解：
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」 應該不成功！裁員後失敗。故事結局。 （事實上，輸入!,fail,!,fail作爲查詢將在我有權訪問的所有Prolog系統中失敗）。
所以我可以假定教科書中的執行模型並不完全是Prolog使用的模型？
編輯：將第一個子句更改爲n(X) :- call(X), !, fail在我嘗試的所有Prolog中沒有任何區別。
謝謝你的回答。我以爲 ！只意味着「承諾已經在當前替代的綁定，並不再退縮」......我不明白爲什麼解決方案會變空。 – josh 2012-07-24 10:54:18
例如，此處的剪切不會使解析變空：a（X）： - write（'one'），！，write（'two'）。 ------ b（X）： - a（X），寫（'三'）。這將實際上打印「onetwothree」（「三」被打印因爲「寫」（'三'）「沒有從解決方案中刪除時找到切割。我仍然有點困惑。 – josh 2012-07-24 11:03:08
請注意那個解釋器是暗示的，當談到「選擇」時，它說「任何一個匹配的人都可以選擇」，但是接着談到「如果做出了另一個選擇會怎麼樣」，這意味着解釋者的一個「運行」解釋了一個結果。但這意味着所有可能的選擇都已經完成，所以***所有可能的結果***都已經到達了。「Cut」就是減少找到的結果的數量，它說：「不要搜索更多的結果，我現在所擁有的就足夠了「，你不會把它放到解決方案中，它不是一個邏輯目標，它是一個操作命令2intrptr。 – 2012-07-24 13:16:36