我有以下知识库，应该添加两个参数并给出结果：
add(0,X,X).
add(succ(X),Y,succ(R)):- add(X,Y,R).
现在这是我的查询：
?- add(succ(succ(succ(0))), succ(succ(0)), Result).
0 不与第一个参数统一，因此它转到第二个 add/3 子句。现在这是我无法弄清楚的事情。这本书（LPN）告诉我，最外层的成功因素被排除在第一个参数之外，但我不知道为什么？在我看来，它增加了一个 succ 仿函数。有人可以解释一下为什么要剥离它吗？
提前致谢！
卢克
在您的顶级提示符下尝试此操作：
?- succ(succ(0)) = succ(X).
在您输入之前<Enter>，您认为解决方案是什么？
书中谈到的“剥离”发生在第二个子句的头部add(succ(X), ...)和递归调用之间add(X, ...)。
我真的没有看到在这里谈论“剥离”的附加价值。实际发生的情况是，如果 to 的第一个参数add/3是带有函子的术语succ/1（所以任何看起来像succ(<Whatever>), 那么，X将与 this 统一<Whatever>。在查询的情况下：
?- add(succ(succ(succ(0))), succ(succ(0)), Result).
<Whatever>是succ(succ(0))，所以 与X统一succ(succ(0))，这是对 的递归调用的第一个参数add/3。