我试图理解为什么 Prolog 实现不按照教科书中的执行模型运行——例如，Sterling 和 Shapiro 的“Prolog 的艺术”书中的那个（第 6 章，“Pure Prolog”，第 6.1 节， “Prolog 的执行模型”）。
我所指的执行模型是这样的（Sterling & Shapiro 的第 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 页），Prologchoose goal A以从左到右的顺序选择目标 ( )，并choose renamed clause ...按照它们在程序中出现的顺序搜索子句 ( )。
下面的程序有一个定义not（n在程序中调用）和一个单一的事实。
n(X) :- X, !, fail.
n(X).
f(a).
如果我尝试证明n(n(f(X)))，它会成功（根据两本教科书以及 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”应该不会成功！切割后有一个失败。故事结局。（事实上，!,fail,!,fail在我有权访问的所有 Prolog 系统中，作为查询输入都会失败）。
那么我可以假设教科书中的执行模型并不是Prolog使用的吗？
编辑：将第一个子句更改为对n(X) :- call(X), !, fail我尝试过的所有 Prolog 都没有影响。