对于即将到来的考试，我有以下复习问题，希望得到一些帮助。我必须使用分辨率回答"玛丽只用青苹果做馅饼"的问题。我目前的知识库和语言是以下句子：
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)
最新更新：
我将尝试在总体上更具体。我想证明的是"玛丽只用青苹果做馅饼"。写这个逻辑我得到：
玛丽只用青苹果做馅饼：π，一个馅饼（π） 一个制造（M， π， a） => 绿色（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形式否定此陈述（我们将在决议中用于证明）：
馅饼（π） A制造（M， π， a） A ⌐绿色（a）
现在，当对一阶逻辑使用分辨率时:(http://en.wikipedia.org/wiki/Resolution_（逻辑））
这是对的吗！？还是我弄错了？
我不确定你是否正确地处理了这个问题。 第一步是将这三个陈述（"苹果要么是绿色的要么是红色的"，"约翰只种青苹果"，"玛丽只用约翰的苹果做馅饼"）编码成幽闭形式，你还没有做过。
第二步是将你试图证明的陈述的否定（"玛丽只用青苹果做馅饼"）编码成幽闭形式。 我不认为你已经这样做了，我认为你已经编码了积极的陈述。 也许我错过了什么。 但是，对查询语句的否定进行编码最终会得到四个与 AND 串在一起的短语句，每个语句都可以被视为知识库中的一个语句。
从那里开始，减少是机械的。
更新：再一次，您需要添加对要证明的陈述的否定。 你没有这样做，你是在添加声明本身和另一个关于苹果是绿色的声明。 别这样。 你不是想证明一个关于苹果是绿色的说法，你试图证明一个关于玛丽只用青苹果做馅饼的说法。 否定该语句，用其他三个知识库语句解决它，并提取一个矛盾（也就是说，对于某些语句 X，一起解决 X 和非 X。
这就是算法。 它有效。 如果你不这样做，无论你是否"需要"这样做，你都在做分辨率算法以外的事情，如果我给你的家庭作业/考试评分，我会把它评为不正确。
更新 2：你越来越近了，但你的查询语句需要一个关于 a 是苹果（即 Apple（a））的附加子句，就像你的其他几个语句已经有的那样。 它看起来应该几乎完全像关于玛丽只使用约翰的苹果的陈述（然后否定，因为它是查询。 它的形式是正确的，小子句与 AND 串在一起，你只是缺少一个。
但请注意，一旦你有了它，这些小子句中的每一个（因为它们与 AND 串在一起）都可以作为知识库中的一个独立语句。 例如，按照您现在的表述方式，您可以使用第三个语句的表达式解析 Pie（p）。 分辨率证明中有很多步骤，但是一旦你完全编码了查询否定，它们都是这样的小步骤。
作为一般信息，您需要在 CNF 中拥有知识库，以及否定目标（也在 CNF 中）。然后，通过统一和应用分辨率，您需要有一个零解决方案或目标状态本身。另一种选择是无法找到其中任何一个并无限解决。
如果
Make(p,π,a)
在您的知识库中，然后统一并应用解决方案，最后一种解决方案是：
⌐Make(M,π,a)
给你一个零的决心。此时，您可以停止并得出结论。