我正在组建一个简单的元解释器，它输出证明的步骤。我在将证明步骤作为输出参数时遇到问题。我的谓词explain1以我想要的详细形式返回证明，但不作为输出参数。我的谓词explain2将证明作为输出参数返回，但不是我想要的详细程度。可以修改explain2，以便产生与explain1一样多的信息吗？我不需要它输出文字“解释......”和“解释......”，只是实际的解释和解释。
程序底部的玩具数据（“如果健康，富裕，那么快乐”）只是一个例子，其目的是建立一个包含更多其他事实的数据库。我想尝试制作一个接受效果的谓词，例如： happy(john)，并返回它的解释。所以E的explain论证应该由用户输入;因此另一个查询可能是explain(_, smokes(mary), _)等等。我无法从解释中的C和E变量直接得到我想要的东西，因为我希望程序在证明过程中输出步骤，其中C和E变化，例如“富裕，健康，快乐;赢得如此丰富;真正如此丰富;真正如此幸福”等等。即返回导致效果的所有因果关系。
Markus Triska的优秀site有一些关于此的详细信息，但我无法使代码适应我的问题。
任何帮助将不胜感激！
谢谢/ JCR
我的节目：
main1:-explain1(_, happy(john), _), fail.
main2:-explain2(_, happy(john), _, T), writeln(T), fail.
explain1(C, E, P):-
C = ['True'],
p(C, E, P),
write('Explaining '), write(E),
write('. An explanation is: '), write(C),
write(' with probability '), write(P), nl.
explain1(C, E, P):-
p(C, E, P),
not(C = ['True']),
write('Explaining '), write(E),
write('. An explanation is: '), write(C),
write(' with probability '), write(P), nl.
explain1(C, E, P):-
p(C0, E, P0),
maplist(explain1, C1, C0, P1),
flatten(C1, C),
append([P0], P1, P2),
flatten(P2, P3),
foldl(multiply, P3, 1, P),
write('Explaining '), write(E),
write('. An explanation is: '), write(C),
write(' with probability '), write(P), nl.
explain2(C, E, P, T):-
C = ['True'],
p(C, E, P),
T = [C, E, P].
explain2(C, E, P, T):-
p(C, E, P),
not(C = ['True']),
T = [C, E, P].
explain2(C, E, P, T):-
p(C0, E, P0),
maplist(explain2, C1, C0, P1, _),
flatten(C1, C),
append([P0], P1, P2),
flatten(P2, P3),
foldl(multiply, P3, 1, P),
T = [C, E, P].
multiply(V1, V2, R) :- R is V1 * V2.
p(['True'], wins(john), 0.7).
p([wins(john)], rich(john), 0.3).
p(['True'], healthy(john), 0.9).
p([rich(john), healthy(john)], happy(john), 0.6).
main1的输出：
Explaining happy(john). An explanation is: [rich(john), healthy(john)] with probability 0.6
Explaining rich(john). An explanation is: [wins(john)] with probability 0.3
Explaining healthy(john). An explanation is: [True] with probability 0.9
Explaining happy(john). An explanation is: [wins(john), True] with probability 0.162
Explaining wins(john). An explanation is: [True] with probability 0.7
Explaining rich(john). An explanation is: [True] with probability 0.21
Explaining healthy(john). An explanation is: [True] with probability 0.9
Explaining happy(john). An explanation is: [True, True] with probability 0.1134
main2的输出：
[[rich(john), healthy(john)], happy(john), 0.6]
[[wins(john), True], happy(john), 0.162]
[[True, True], happy(john), 0.1134]
我不清楚这个元解释器的概率部分，但我实际上认为它是你的问题的附带所以我将尝试勾勒出我将如何处理这个问题。
您可以将call/1视为Prolog的原型解释器，因为它只是证明了一个目标。所以看起来你想要的API就像prove(+Goal, -Proof)，其中Goal就像它与call/1一样得到证明，但是你得到了第二件事，这是某种证明。
当正常的Prolog看到像Goal1, Goal2这样的表达时，你可以想到它扩展到call(Goal1), call(Goal2)。那么你的证据返回元解释器在这种情况下做了什么呢？它应该证明两个目标，然后以某种方式结合这些“subproofs”。
所有这些都向我表明，你的观念中缺少的是，证据的结构是什么？我会认真考虑你要回来的东西，因为如果你不想要一个字符串，你会想要一些你可以更容易穿越的东西。最终可能会出现类似于Prolog所做的树结构（除了没有失败分支）。因此我希望它有某种嵌套，它肯定会以某种方式“类似”调用堆栈，虽然我希望这会限制它的实用程序（你如何有效地遍历那个树用于通用查询？）。
让我们考虑你的基本情况。它可能是这样的：
prove(true, true) :- !.
真实本质上是正确的，因为它是真的。
我感兴趣的下一个案例是“和”。
prove((G1, G2), (P1, P2)) :-
!,
prove(G1, P1),
prove(G2, P2).
这看起来相当重言，但关键的想法是我们在证明中将G1和G2的证明与(P1, P2)结合起来。
下一个案例可能是“或”：
prove((G1;_), P1) :- prove(G1, P1).
prove((_;G2), P2) :- !, prove(G2, P2).
这是我们失去失败分支的部分。如果第一个分支成功，它的证明将出现在结果中;如果第二个分支成功，它的证明将出现在结果中。但它们不会同时出现在结果中。
最后，我们必须处理内置和用户谓词，每个a question I asked some time ago：
prove(H, subproof(H, Subproof)) :- clause(H, Body), prove(Body, Subproof).
prove(H, builtin(H)) :- call(H).
在这一点上，我们有一个metainterpreter，可以生成非常简单的证明。我将添加一些子句，然后使用我们的metainterpreter尝试：
mortal(X) :- man(X).
man(socrates).
这是查询：
?- prove((member(X, [bread,socrates]), mortal(X)), Proof).
X = socrates,
Proof = (builtin(member(socrates, [bread, socrates])),
subproof(mortal(socrates),
subproof(man(socrates), true)))
由于我还不了解的原因，member/2的使用将在第二次查询时爆炸。我有opened a question about that on the SWI forum，当我发现那里发生了什么时，我会更新这个答案。
更新。这个问题与使用library(lists)时发生的member/2的自动加载有关。在第一次调用时，member/2没有子句，因此它进入call/1，它调用自动加载器然后将其作为内置调用。在随后的尝试中，member/2有条款，但它们的主体涉及lists模块中的谓词，而这个元解释器不能正确处理模块。一个快速而肮脏的解决方案是将第三个子句更改为：
prove(H, subproof(H, Subproof)) :-
\+ predicate_property(H, imported_from(_)),
clause(H, Body),
prove(Body, Subproof).
我希望这有帮助！