Let's consider the following Prolog program (from "The Art of Prolog"):
natural_number(0).
natural_number(s(X)) :- natural_number(X).
plus(X, 0, X) :- natural_number(X).
plus(X, s(Y), s(Z)) :- plus(X, Y, Z).
and the query:
?- plus(s(s(s(0))), s(0), Z).
Both SICStus and SWI produce the expected Z = s(s(s(s(0))))
answer, but query the user for the next answer (a correct no
/false
answer). However, I cannot understand why there is an open branch in the SLD tree after the only goal is found. I tried debugging both under SICStus and under SWI, but I am not really able to interpret the result yet. I can only say that, as far as I could understand, both backtrack to plus(s(s(s(0))), 0, _Z2)
. Can someone help me understanding this behavior?