1)
我将从“如何检查”问题开始，因为我认为这将是最有用的。如果您在 xpce 中使用 swi-prolog，请运行 guitracer:
?- consult('pterm'). % my input file
% pterm compiled 0.00 sec, 5 clauses
true.
?- guitracer.
% The graphical front-end will be used for subsequent tracing
true.
?- trace. % debugs step by step
true.
[trace] ?- pterm(f0(f1(null))). % an example query to trace
true.
会出现一个图形界面。按向下箭头逐步统一事物。发生的事情应该很快就能理解。
（使用notrace. 和nodebug. 之后适当地退出跟踪和调试模式）。
2）您似乎误解了谓词的工作原理。谓词是一个逻辑语句，即它总是返回
true 或
false。您可以将它们视为“iseven(X)”类型的经典布尔函数（测试 X 是否为偶数）或“ismemberof(A,B)”（测试 A 是否为 B 的成员）等。当您有像“pred1 :- pred2, pred3”这样的规则。这类似于说“如果 pred2 返回 true，pred1 将返回 true，并且 pred3 返回 true（否则 pred1 返回 false）”。
当使用常量调用谓词时，检查其真值就是检查事实数据库以查看是否可以满足具有这些常量的谓词。但是，当您调用 using variables 时，prolog 会遇到麻烦，试图unify 该变量与它可以链接到的所有允许的东西，看看它是否可以尝试使该谓词为真。如果做不到，它就放弃并说它是假的。
像incr(X,Y) 这样的谓词仍然需要返回真或假，但是，如果按照设计，这只有在 Y 是 X 的递增版本时才成立，其中 X 是预期的要在查询时作为输入给出，那么我们已经欺骗 prolog 制作了一个“函数”，该“函数”将 X 作为输入，并“返回”Y 作为输出，因为 prolog 将尝试找到一个合适的 Y 使谓词为真。
因此，在您的示例中，incr(X,Y) :- pterm(f0(X)), pterm(f1(Y)). 没有任何意义，因为您告诉它incr(X,Y) 将为任何 X、Y 返回 true，只要 prolog 可以使用 X 在事实数据库中查找任何 pterm (f0(X)) 这将导致一个已知事实，并且还使用 Y 来找到一个 pterm(f1(Y)) 项。您没有以任何方式使 Y 依赖于 X。例如，对于 X = null 和 Y = null，此查询将成功。
你的第一个子句应该是这样的。
incr(X,Y) :- X = pterm(f0(Z)), Y = pterm(f1(Z)).
= 在哪里执行统一。 IE。 “为 Z 找到一个值，使得 X 为 pterm(f0(Z))，对于相同的 Z 值，它也适用于 Y = pterm(f1(Z))。”
事实上，这可以更简洁地重写为事实：
incr( pterm(f0(Z)), pterm(f1(Z)) ).
3)
您的第二个子句可以类似地调整。但是，我不确定这在您试图实现的逻辑（即二进制算术）方面是否正确。但我可能误解了您要解决的问题。
我的假设是，如果你有 (0)111，那么后继应该是 1000，而不是 1111。为此，我猜你需要创建一个谓词，递归检查当前处理的数字以下的增量是否导致一个“携带”的数字。
（因为实际的逻辑是你的任务的内容，我不会在这里提供解决方案。但希望这有助于你了解正在发生的事情。随意尝试递归版本并询问另一个基于该代码的问题！）