suppose the following program:
nat(0).
nat(s(N)) :- nat(N).
/* 0+b=b */
plus(0,B,B) :- nat(B).
/* (a+1)+b = c iff a+(b+1)=c */
plus(s(A),B,C) :- plus(A,s(B),C).
it works great for adding two numbers, but when i attempt a query of the following sort:
plus(Z,Z,s(0)).
it goes on to search possible values for Z long after it should be obvious that there is no solution (i.e. Z>s(0))
i'm familiar with the cut(!) operator and my intuition says the solution has something to do with it, i'm just not sure how to use it in this case.
!/0 is quite consistently not a good solution for such problems. It typically leads to loss of valid solutions for more general queries.
Instead, consider using finite domain constraints, which work perfectly well in this case:
?- use_module(library(clpfd)).
true.
?- Z + Z #= 0.
Z = 0.
?- Z + Z #= 0, Z #> 0.
false.
EDIT: A possible solution without CLP(FD), as requested:
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).