我有一个即将到来的考试的复习问题，希望能得到一些帮助。我需要使用分辨法回答“玛丽只用绿苹果做馅饼”这个查询。我当前的知识库和语言是以下句子：

Mary only uses apples from John to make pies: ∀π,a(Apple(a) ∧ Pie(π) ∧ Make(M,π,a) => Grows(J,a))(⌐Apple(a) V ⌐Pie(π) V ⌐Make(M, π, a) V Grows(J,a))    (in CNF)

最新更新：

我会尽量更具体一些。我想要证明的是“玛丽只用绿苹果做馅饼”。写出这个逻辑，我得到：

Mary only uses green apples to make pies: π,a Pie(π) A Make(M, π, a) => Green(a)

将其翻译成CNF形式的步骤（http://en.wikipedia.org/wiki/Conjunctive_normal_form）：

π,a ⌐(Pie(π) A Make(M, π, a)) V Green(a) π,a (⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) (⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) ⌐Pie(π) V ⌐Make(M, π, a) V Green(a) (CNF form)

这个陈述的否定形式在CNF形式中（我们将在分辨证明中使用）：

Pie(π) A Make(M, π, a) A ⌐Green(a)

现在在使用一阶逻辑的分辨法时：(http://en.wikipedia.org/wiki/Resolution_(logic))

这是对的吗？还是我弄错了？

回答：

我不确定你是否正确地处理了这个问题。第一步是将三个陈述（“苹果要么是绿色的，要么是红色的”，“约翰只种植绿苹果”，“玛丽只用约翰的苹果做馅饼”）编码成子句形式，你还没有这样做。

第二步是将你试图证明的陈述的否定（“玛丽只用绿苹果做馅饼”）也编码成子句形式。我认为你没有这样做，我认为你编码的是正面陈述。也许我错过了什么。但是对查询陈述的否定编码最终会得到四个用AND连接的简短陈述，每个都可以作为知识库中的一个陈述来处理。

从那里开始，简化就是机械的过程了。

更新： 再一次，你需要添加你试图证明的陈述的否定。你没有这样做，你添加了陈述本身和另一个关于苹果是绿色的陈述。不要这样做。你不是在试图证明关于苹果是绿色的陈述，你是在试图证明关于玛丽只用绿苹果做馅饼的陈述。否定那个陈述，与你的其他三个知识库陈述一起进行分辨，并提取出矛盾（也就是说，将X和非X一起分辨，对于某个陈述X）。

这就是算法。它有效。如果你不这样做，无论你“需要”与否，你做的都是分辨算法之外的事情，如果我在评分你的作业/考试，我会判定为错误。

更新2：你越来越接近了，但你的查询陈述需要增加一个关于a是苹果（即，Apple(a)）的额外子句，因为你的其他几个陈述已经有了。它应该看起来几乎和关于玛丽只用约翰的苹果的陈述一样（然后因为它是查询而被否定）。它的形式是正确的，小子句用AND连接，你只是缺少了一个。

但是一旦你有了那个，请注意，每个小子句（因为它们是用AND连接的）都可以作为知识库中的独立陈述来处理。所以例如，按照你现在的表述，你可以将Pie(p)与你的第三个陈述的表达式进行分辨。分辨证明中有很多步骤，但是一旦你完全编码了查询否定，它们都是像这样的微小步骤。