一种解决方案：抽象解释
预赛
在这个答案中，我使用解释器来证明这一点。但是，它不是Prolog解释器，因为它不会以与Prolog解释程序完全相同的方式来解释程序。
相反，它以更抽象的方式解释程序。这样的解释器因此被称为抽象解释器。
程序表示
至关重要的是，我直接使用源程序，只使用我们通过纯代数推理知道可以安全应用的修改。对于这样的推理非常有帮助，即您的源程序在构造上是完全纯的，因为它只使用纯谓词。
为了简化对程序的推理，我现在将所有统一明确化。很容易看出，这并没有改变程序的含义，并且可以很容易地实现自动化。我得到：
f（_，X，Y）：-
X = 1,
Y = s(1)。
f（Arg，X，Y）：-
精氨酸 = 1，
X = s(X0),
Y = s(s(Y0)),
f(Arg, X0, Y0)。
f（X，Y，T）：-
X = s(X0),
Y = s(Y0),
f(X, Y0, Z),
f(X0, Z, T)。
我把它作为一个简单的练习来证明这在声明上等同于原始程序。
抽象
我使用的抽象如下：我没有对具体的术语1、s(1)等进行推理，而是对我可以证明T成立的 每个术语 Ts(s(1))使用原子 。dd()
让我向您展示我对统一的以下解释的意思：
解释（d = N）：- d（N）。
这说：
如果 d(N) 成立，则 N 将被视为与原子 相同d，正如我们所说，原子应表示任何d/1成立的术语。
请注意，这与具体术语和含义之间的实际统一有很大不同！例如，我们得到：dN
?-解释(X = s(s(1)))。
X = d。
很奇怪，但我希望你能习惯它。
扩展抽象
当然，解释一个单一的统一并不足以解释这个程序，因为它还包含额外的语言元素。
因此，我将抽象解释扩展到：
解释连词很容易，但是呢f/3？
增量推导
如果在抽象解释过程中遇到目标f(X, Y, Z)，那么我们知道以下内容：原则上，论点当然可以与目标成功的任何术语统一。因此，我们跟踪那些我们知道查询原则上可以成功的参数。
因此，我们为谓词配备了一个附加参数：作为f/3程序逻辑结果的目标列表。
此外，我们实现了以下非常重要的规定：如果我们遇到无法用抽象术语安全解释的统一，那么我们会抛出错误而不是静默失败。例如，如果统一在被视为抽象解释时失败，尽管它会成功，这可能会发生作为一个具体的统一，或者如果我们不能完全确定这些论点是否属于预期的领域。该规定的主要目的是避免由于抽象解释器的疏忽而无意中消除了实际解决方案。这是解释器中最关键的方面，任何证明论机制都会面临密切相关的问题（我们如何确保没有遗漏任何证明？）。
这里是：
解释（Var = N，_）：-
must_be(var, Var),
must_be（地面，N），
d(N),
变量 = d。
解释（（A，B），Ds）： -
解释（A，Ds），
解释（B，Ds）。
解释（f（A，B，C），Ds）：-
成员（f（A，B，C），Ds）。
Quis custodiet ipsos custodes？
我们如何判断这是否真的正确？这是最难的部分！事实上，事实证明上述方法不足以确定捕获所有情况，因为如果不成立，它可能会失败。d(N)抽象解释器在无法处理的情况下静默失败显然是不可接受的。所以我们至少还需要一个子句：
解释（Var = N，_）：-
must_be(var, Var),
must_be（地面，N），
\+ d(N),
域错误（d，N）。
事实上，当我们推理基本术语时，抽象解释器变得更不容易出错，因此我将使用原子 any来表示派生答案中的“任何术语”。
在这个域上，统一的解释变成：
解释（Var = N，_）：-
must_be（地面，N），
( var(Var) ->
( d(N) -> Var = d
; N = s(d) -> Var = d
; N = s(s(d)) -> Var = d
; domain_error(d, N)
)
; Var == 任何 -> 真
; 域错误（任何，变量）
）。
此外，我已经在这个抽象域上实现了进一步的统一案例。我把它作为一个练习来思考这是否正确地模拟了预期的语义，并实现了更多的案例。
事实证明，这个定义足以回答发布的问题。然而，它显然还有很多不足之处：它比我们想要的更复杂，而且越来越难以判断我们是否涵盖了所有案例。请注意，任何证明理论的方法都将面临密切相关的问题：它变得越复杂和强大，就越难判断它是否仍然正确。
所有推导：定点见！
现在仍然需要从原始程序中推断出所有内容。
这是一个简单的定点计算：
衍生品（Ds）：-
函子（头，f，3），
findall(Head-Body, Clause(Head, Body), Clauses),
derivables_fixpoint（子句，[]，Ds）。
derivables_fixpoint（子句，Ds0，Ds）：-
findall（D，clauses_derivable（子句，Ds0，D），Ds1，Ds0），
term_variables(Ds1, Vs),
地图列表（=（任何），Vs），
排序（Ds1，Ds2），
（相同长度（Ds2，Ds0）-> Ds = Ds0
; derivables_fixpoint（子句，Ds2，Ds）
）。
Clauses_derivable(Clauses, Ds0, Head) :-
成员（头体，子句），
解释（正文，Ds0）。
由于我们正在推导基本术语，因此sort/2删除了重复项。
示例查询：
?- 导数（Ds）。
错误：参数没有充分实例化
有点虎头蛇尾，抽象解释器无法处理这个程序！
拯救的交换性
在证明论的方法中，我们寻找证明。在基于解释器的方法中，我们可以改进解释器或应用代数定律以保留基本属性的方式转换源程序。
在这种情况下，我将做后者，而将前者留作练习。我们不是在寻找证明，而是在寻找编写程序的等效方法，以便我们的解释器能够推导出所需的属性。例如，我现在使用合取交换律来获得：
f（_，X，Y）：-
X = 1,
Y = s(1)。
f（Arg，X，Y）：-
精氨酸 = 1，
f(Arg, X0, Y0),
X = s(X0),
Y = s(s(Y0))。
f（X，Y，T）：-
f(X, Y0, Z),
f(X0, Z, T),
X = s(X0),
Y = s(Y0)。
同样，我把它作为一个练习来仔细检查这个程序在声明上是否等同于你的原始程序。
iamque opus exegi，因为：
?- 导数（Ds）。
Ds = [f(any, d, d)]。
这表明在 的每个解中f/3，最后两个参数始终是d/1成立的项！特别是，它也适用于您发布的示例参数，即使没有希望实际计算具体条款！
结论
通过抽象解释，我们表明：
- 对于所有成立的
X地方f(_, _, X)，d(X) 也成立
- 除此之外，对于所有成立的
Y地方f(_, Y, _)，d(Y) 也成立。
该问题仅询问第一个属性的特殊情况。我们已经展示了更多！
总之：
如果 f(_, Y, X)持有，则 d(X)持有并 d(Y)持有。
Prolog 使推理 Prolog 程序变得相对容易和方便。这通常使我们能够导出 Prolog 程序的有趣属性，例如终止属性和类型信息。
请参阅有关程序的推理以获取参考和更多解释。
+1 一个很好的问题和参考。