问题描述
假设我们想要可视化这个 Prolog 执行。没有来自 fidschi 群岛的目标，也没有其他异国情调的假设，只有古老的 SLDNF 使用默认选择规则：
p(a).
p(b).
?- \+ p(c).
Yes
但我们只有一个 Prolog 可视化器可以显示推导 没有作为失败的否定，如 here。我们如何提升 Prolog 可视化工具也将否定显示为失败？
解决方法
否定作为失败的好处，为否定作为失败编写元解释器比为 cut (!) 编写元解释器要容易得多。所以基本上 SLDNF 的 vanilla 解释器可以通过插入一个额外的规则从 SLD 的 vanilla 解释器派生出来：
solve(true) :- !.
solve((A,B)) :- !,solve(A),solve(B).
solve((\+ A)) :- !,\+ solve(A). /* new */
solve(H) :- functor(H,F,A),sys_rule(F/A,H,B),solve(B).
我们现在可以继续从 here 扩展solve/3，但同样徒劳无功。但是我们做了更多的事情，我们还在搜索树中写出失败的分支，类似于 Prolog 可视化工具通过删除子句所做的。所以修改后的solve/3如下：
% solve(+Goal,+Assoc,+Integer,-Assoc)
solve(true,L,_,L) :- !.
solve((A,P,R) :- !,solve(A,H),solve(B,R).
solve((\+ A),L) :- !,\+ solve(A,_). /* new */
solve(H,R) :- functor(H,J,callable_property(J,sys_variable_names(N)),number_codes(P,U),atom_codes(V,[0'_|U]),shift(N,V,W),append(L,W,M),(H = J -> true; offset(P),write(fail),nl,fail),/* new */
reverse(M,Z),triage(M,Z,I,K),offset(P),write_term(I,[variable_names(Z)]),O is P+1,K,O,R).
这是一个示例运行：
?- ?- \+ p(c).
fail
fail
Yes
另见：
人工智能算法、数据结构和习语
CH6：三个元解释器
Georg F. Luger - Addison-Wesley 2009
https://www.cs.unm.edu/~luger/