Prolog 元解释器中作为输出参数的证明

Question

我正在组装一个简单的元解释器，它输出证明的步骤。我无法将证明步骤作为输出参数。我的谓词explain1 以我想要的详细形式返回证明，但不是作为输出参数。我的谓词explain2 将证明作为输出参数返回，但没有达到我想要的详细程度。可以修改explain2 使其产生与explain1 一样多的信息吗？我不需要它来输出文本“Explaining...”和“Explanation...”，只需要实际的 explanans 和 explanandum。

程序底部的玩具数据（“如果健康和富有，那么快乐”）只是一个示例，其想法是建立一个包含更多关于其他事物的事实的数据库。我想尝试制作一个接受效果的谓词，例如happy(john)，并返回解释。所以explain 的E 参数应该由用户输入；因此，另一个查询可能是explain(_, smokes(mary), _) 等等。我无法直接从解释中的C 和E 变量中得到我想要的，因为我希望程序输出证明过程中的步骤，其中C 和E 不同，例如“富足健康，如此幸福；赢如此富；真如此富；真如此幸福”等等。 IE。返回导致结果的所有因果关系。

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]

Answer 1

我不清楚这个元解释器的概率部分，但我实际上认为这与你的问题无关，所以我将尝试勾勒出我将如何处理这个问题。

您可以将call/1 视为 Prolog 的原型解释器，因为它只是证明了一个目标。所以看起来你想要的 API 类似于 prove(+Goal, -Proof)，其中 Goal 得到证明，就像它对 call/1 所做的那样，但你得到第二件事，某种证明。

当普通 Prolog 看到像 Goal1, Goal2 这样的表达式时，你可以认为它扩展为 call(Goal1), call(Goal2)。那么在这种情况下，您的证明返回元解释器会做什么呢？它应该证明两个目标，然后以某种方式结合这些“子证明”。

所有这些都向我表明，您的概念中缺少的东西是，证明的结构是什么？我会认真考虑你要返回什么样的东西，因为如果你不想要一个字符串，你会想要一些你可以更容易遍历的东西。它可能最终具有类似于 Prolog 所做的树结构（除了没有故障分支）。因此，我希望它具有某种嵌套，并且它肯定会以某种方式“类似于”调用堆栈，尽管我希望这会限制它对您的实用性（您将如何有效地遍历该树以进行通用查询？）。

让我们考虑一下您的基本情况。大概是这样的：

prove(true, true) :- !.

True 本质上是真实的，因为它是真实的。

我感兴趣的下一个案例是“and”。

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

此时我们有了一个元解释器，它可以生成非常简单的证明。我将添加一些子句，然后用我们的元解释器尝试一下：

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，当我发现那里发生了什么时会更新这个答案。

更新。该问题与使用member/2 时发生的library(lists) 的自动加载有关。在第一次调用时，member/2 没有子句，所以它输入call/1，它调用自动加载器，然后作为内置调用它。在随后的尝试中，member/2 有子句，但它们的主体涉及 lists 模块中的谓词，并且此元解释器无法正确处理模块。一个快速而肮脏的解决方案是将第三个子句更改为：

prove(H, subproof(H, Subproof)) :- 
   \+ predicate_property(H, imported_from(_)), 
   clause(H, Body), 
   prove(Body, Subproof).

我希望这会有所帮助！