使用逻辑编程符号，给定以下子句：
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 显示这个？换句话说，我如何证明你可以从C 派生出D？
【问题讨论】：
标签： prolog logic first-order-logic
您在我的第一篇文章后澄清了您的问题，但下面已经有一些讨论。为防止混淆，我不会编辑它，而是写第二个：
你不能直接把你的问题写成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
cmets 应该或多或少不言自明：copy_terms 创建输入子句的变体，否则您可能会丢失解析器。然后你选择第二个子句主体的第一个元素并尝试统一。实际上，这种统一足以正确地实例化两个子句。现在我们创建我们的 resolvent 子句：第 1 子句的头部被继承（以 unifier 替换为模），resolvent 的主体是第 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_resolvent 的演绎闭包来扩展程序以查看任意解析序列（您可能希望确定链接顺序，否则会遇到无限递归）。
玩得开心！
【讨论】：
与一般的解析相比，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) 的解析的无限推导序列隐藏）。
我希望，这有助于了解正在发生的事情。如果没有，我总是可以添加更多；）
附：我做了一个小的教学跳跃 - 查询是对您需要提供给定理证明者的纯否定子句的否定。由于查询是用户定义的，因此您只需考虑 Prolog 派生它而不是用它的否定来解决。这也使您不必引入 skolem 符号。
【讨论】：
C1 解析C3。