2

使用逻辑编程符号，给定以下子句：

C = m(P,X) <- m(Q,X), m(R,X)

可以用 C' 的第一个正文文字来解析 C 的头部，以给出替换{P/Q',X/X'}和子句：

D = m(P',X') <- m(Q,X'), m(R,X'), m(R',X').

我怎样才能用 Prolog 展示这个？换句话说，我怎样才能证明你可以D从C?

4

2 回答 2

2

你在我的第一篇文章后澄清了你的问题，但下面已经有一些讨论了。为了防止混淆，我不会编辑它，而是写第二个：

您不能直接将问题写成 prolog 程序有两个原因：

  • 你想不经询问就解决
  • 您想查看（单个）推导步骤的解决方案

因此，我们将在谓词 mi_clause 中对子句数据库进行编码，该谓词具有两个参数：头部和带有主体的列表。谓词 Clause_clause_resolvent 有 6 个参数：每个子句的头部和主体以及解析器。在这里，解析器是在第二个子句的开头与第一个子句正文的第一个元素解析的结果。反过来做也可以。

mi_clause(m(_P,X), [m(_Q,X), m(_R,X)]). % your original clause, anonymous variables are prefixed with _ for compiler reasons

clause_clause_resolvent( Head1, Body1, Head2, Body2, RHead, RBody) :- 
    copy_term(clause(Head1,Body1), clause(H1,B1)), % create a variant of the first clause
    copy_term(clause(Head2,Body2), clause(H2,B2)), % same for second clause
    B1 = [H2|Rest1],                               % the prolog execution order always uses the first literal
    H1 = RHead,                                    % head of resolvent is the same (is only resolved with the query)
    append(Rest1, B2, RBody).                      % create the new body

注释应该或多或少不言自明：copy_terms 创建输入子句的变体，否则您可能会丢失解析器。然后你选择第二个子句主体的第一个元素并尝试统一。实际上，这种统一足以正确地实例化两个子句。现在我们创建我们的解析子句：第 1 条的头部被继承（以统一符替换为模），解析器的主体是第 1 条的主体，没有在第二个子句主体的主体之前添加解析的文字。

现在试试谓词，例如在 SWI Prolog 中：

?- mi_clause(H1,B1), mi_clause(H2,B2), clause_clause_resolvent(H1,B1,H2,B2,RH,RB).
H1 = m(_G1028, _G1029),
B1 = [m(_G1034, _G1029), m(_G1040, _G1029)],
H2 = m(_G1043, _G1044),
B2 = [m(_G1049, _G1044), m(_G1055, _G1044)],
RH = m(_G1068, _G1069),
RB = [m(_G1080, _G1069), m(_G1099, _G1069), m(_G1105, _G1069)].

如您所见，H1 和 H2 是包含新匿名变量的子句头部的变体。RB 的所有元素仍然是 m(_, _G1069) 的形式，获得您期望的子句的变体。

如果要检查一般解决步骤，请将 B1 = [H2|Rest1] 行替换为 member_of_rest(H2, B1, Rest1) 并将其定义为：

member_of_rest(X, [X|Xs], Xs).
member_of_rest(X, [H|Xs], [H|Ys]) :-
    member_of_rest(X, Xs, Ys).

作为一个很好的练习，您可以通过对 clause_clause_resolvent 的演绎闭包来扩展程序以查看任意解析序列（您可能希望确定链接顺序，否则会遇到无限递归）。

玩得开心！

于 2014-10-27T22:27:40.237 回答
1

与一般的解析相比，Prolog 具有解析子句的顺序。这意味着，一般来说，您不能强制 prolog 将两个文字相互解析。Prolog 中推理的主要思想是，在 Horn 子句的情况下（只有一个正面文字，0+ 负面文字），在每个解决步骤之后，您都会得到一个新的 Horn 子句。您只能通过使用纯否定子句解决来完成空子句的证明。在 Prolog 中，此子句由用户以查询的形式提供。该查询指导 Prolog 的证明策略。

或许让我们看看经典的亚里士多德是一个人类的例子：

我们知道亚里士多德是一位哲学家（1），所有的哲学家都是人（2）。因此亚里士多德是人。

philosopher(aristoteles).   % (1)
human(X) :- philosopher(X). % (2)

现在我们制定我们的查询：

?- human(aristoteles). % (3)

Prolog 从上到下查找带有 (3) 的头部的子句（肯定子句）。子句（1）的头部没有统一，所以我们尝试子句（2）并找到一个（最一般的）统一词：X = aristoteles。我们现在导出子句：

:- philosopher(aristoteles). % (4)

我们可以用子句 (1) 来解决，同样用统一词 X = aristoteles。到达空子句 - 万岁，我们有证据！

在这个推导中最重要的是查询。在您的情况下，我们实际上可以制定一个查询来满足您的需求。C1和C2是同一个子句（变量取模重命名），所以我们写下：

m(P,X) :- m(Q,X), m(R,X). % (5)

如果我们现在查询 m(A,Y)，我们将启动一个推导过程，该过程模拟您想要的步骤。用 (5) 解决查询，可以代入 P = A，X = Y 并得到：

:- m(Q,A), m(R,A). % (6)

我们首先尝试解决 m(Q,A)，它再次与规则 (5) 匹配 P = Q，A = X：

:- m(Q,A), m(R,A). % (7)

由于第 (6) 和 (7) 条是相同的，很明显没有任何解决步骤将到达空子句。换句话说，Prolog 将陷入无限循环（取决于优化，它甚至可能不会填满执行堆栈并静默循环，否则会出现堆栈外错误）。

要使您的查询终止，您可以添加事实

m(a,b). % (8)

将上述推理规则 (5) 添加到您的规则数据库中。由于 Prolog 从上到下处理子句，从左到右处理文字，因此将其放在下面会将子句置于永远不会被解析的位置（它被子句 (5) 的解析的无限推导序列隐藏）。

我希望，这有助于了解正在发生的事情。如果没有，我总是可以添加更多；）

PS 我做了一个小的教学跳跃 - 查询是对您需要提供给定理证明者的纯否定子句的否定。由于查询是用户定义的，因此您只需考虑 Prolog 派生它而不是用它的否定来解决。这也让您了解引入 skolem 符号的必要性。

于 2014-10-26T15:17:05.703 回答