如何在PROLOG中回溯

Question

我有以下PROLOG查询，它是数据库。

r(X,Y), s(Y,Z), not(r(Y,X)), not(s(Y,Y). 

r(a,b). r(a,c). r(b,a). r(a,d). 
s(b,c). s(b,d). s(c,c). s(d,e). 

PROLOG在此示例中如何回溯？我想它会是这样的：

1- Unifies X with 'a' and Y with 'b' 

2- Unifies Y with 'b' and Z with 'c' 

3- This goal means that there mustn't be any other clause in the database where 
    this happens: r(a,b) r(b,a). 
    My doubt lies here. Does prolog advance to the next goals or does it verify 
    the other r(X,Y) database clauses to check for a match and possibly invalidate 
    the solution? 

    I guess that what Prolog does is the following: 
    - Verifies the rest of the r(X,Y) clauses to check for a r(Y,X) match and if 
    there is one, then it backtracks to the 2nd step (s(Y,Z)). 
    This will obviously generate unnecessary tree branches which do not need to be 
    tested since the 1st goal is always the same. 

4. Verifies if S(X,Y), X == Y. Backtracks to step 1 with new values (a & c) and so on. 

我是否正确？如果有人能根据这个问题绘制一棵树，我真的会感到厌烦，所以我可以完全理解它。

Answer 1

我建议你使用示踪器来查看证明树（有些人认为是不好的做法，但如果你遇到困难，它确实有助于理解执行模型）。所以你去（有\+/1替换not/1）：

?- trace(r/1), trace(s/1). 
true. 

[debug] ?- r(X, Y), s(Y, Z), \+ r(Y, X), \+ s(Y, Y). 
T Call: (7) r(_G341, _G342) 
T Exit: (7) r(a, b) 
T Call: (7) s(b, _G345) 
T Exit: (7) s(b, c) 
T Call: (7) r(b, a) 
T Exit: (7) r(b, a) 
T Redo: (7) s(b, _G345) 
T Exit: (7) s(b, d) 
T Call: (7) r(b, a) 
T Exit: (7) r(b, a) 
T Redo: (7) r(_G341, _G342) 
T Exit: (7) r(a, c) 
T Call: (7) s(c, _G345) 
T Exit: (7) s(c, c) 
T Call: (7) r(c, a) 
T Fail: (7) r(c, a) 
T Call: (7) s(c, c) 
T Exit: (7) s(c, c) 
T Redo: (7) r(_G341, _G342) 
T Exit: (7) r(b, a) 
T Call: (7) s(a, _G345) 
T Fail: (7) s(a, _G345) 
T Redo: (7) r(_G341, _G342) 
T Exit: (7) r(a, d) 
T Call: (7) s(d, _G345) 
T Exit: (7) s(d, e) 
T Call: (7) r(d, a) 
T Fail: (7) r(d, a) 
T Call: (7) s(d, d) 
T Fail: (7) s(d, d) 
X = a, 
Y = d, 
Z = e. 

还有就是你证明树。 Redo是Prolog回溯的地方。当呼叫成功时，\+失败，Prolog在Exit后执行Redo。当目标失败时，\+成功后Fail。