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

后成功

如何在 PROLOG 中回溯

How to backtrack in PROLOG

prolog

backtracking