如何在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。