如何阻止prolog无限地检查不可能的解决方案？

Question

假设以下程序:

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).

它适用于添加两个数字,但是当我尝试查询以下类型时:

plus(Z,Z,s(0)).

它继续搜索可能的值Z很长时间后应该很明显没有解决方案(即Z>s(0))

我熟悉cut(!)运算符,我的直觉说解决方案与它有关,我只是不确定如何在这种情况下使用它.

Answer 1

!/0非常一致地不是对于此类问题来说，它通常会导致丢失更一般查询的有效解决方案。

相反，请考虑使用有限域约束，在这种情况下效果非常好：

?- use_module(library(clpfd)).
true.

?- Z + Z #= 0.
Z = 0.

?- Z + Z #= 0, Z #> 0.
false.

编辑：根据要求，没有 CLP(FD) 的可能解决方案：

plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).