使用逻辑编程表示法，给定以下子句：
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程序：
- 要在不查询的情况下解决
- 您想要查看（单个）派生步骤的解析式
因此，我们将在谓词mi_clause中对子句数据库进行编码，该谓词有两个参数：头和带正文的列表。谓词子句_子句_解析器有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会创建input子句的变体，否则可能会丢失解析符。然后，您选择第二个子句正文的第一个元素，并尝试统一。事实上，这种统一足以正确地实例化这两个子句。现在我们创建我们的resolvent子句：子句1的头被继承（取unifier替换的模），resolved的主体是子句1的主体，而第二个子句的主体前面没有resolvedliteral。
现在尝试谓词，例如在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).
作为一个很好的练习，您可以通过子句_子句_解析的演绎闭包来扩展程序，以查看任意的解析序列（您可能想确定链接顺序，或者遇到无限递归）。
玩得开心！
与一般的Resolution不同，Prolog有一个子句解析顺序。这意味着，通常情况下，不能强制prolog解决两个文本之间的冲突。Prolog中推理的主要思想是，在Horn子句（只有一个正文字，0+负文字）的情况下，在每个解析步骤之后，你都会得到一个新的Horn子句。您只能通过使用纯否定子句进行解析来完成空子句的证明。在Prolog中，此子句由用户以查询的形式提供。这个查询指导Prolog的证明策略。
也许让我们看看古典亚里士多德是一个人类的例子：
我们知道亚里士多德是一位哲学家，所有的哲学家都是人。因此亚里士多德是人。
philosopher(aristoteles). % (1)
human(X) :- philosopher(X). % (2)
现在我们制定我们的查询：
?- human(aristoteles). % (3)
Prolog寻找一个从上到下具有与（3）一致的头（正子句）的子句。第（1）条的标题不统一，所以我们尝试第（2）条，找到一个（最普遍的）统一体：X=亚里士多德。我们现在推导出条款：
:- philosopher(aristoteles). % (4)
我们可以用第（1）条来解决，同样用unifier X=亚里士多德。达到空条款-万岁，我们有证据！
在这个派生中，最重要的是查询。在您的情况下，我们实际上可以制定一个查询，它将执行您想要的操作。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符号的必要性。