1

对于即将到来的考试，我有以下复习题，希望得到一些帮助。我必须使用分辨率来回答“玛丽只用青苹果做馅饼”这个问题。我目前的知识库和语言是以下句子：

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 只用青苹果做馅饼： π,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 形式否定此陈述（我们将在决议中使用它来证明）：

饼图(π) A Make(M, π, a) A ⌐Green(a)

现在当对一阶逻辑使用分辨率时:(http://en.wikipedia.org/wiki/Resolution_(logic))

这是正确的吗！？还是我弄错了？

4

2 回答 2

1

我不确定你是否正确地解决了这个问题。第一步是将三个语句（“苹果是绿色的或红色的”、“约翰只种绿色的苹果”、“玛丽只用约翰的苹果做馅饼”）编码成分句形式，这是你没有做过的。

第二步是将您要证明的陈述的否定（“玛丽只用青苹果做馅饼”）也编码成从句形式。我不认为你已经这样做了，我认为你已经编码了积极的陈述。也许我错过了一些东西。但是对查询语句的否定进行编码最终会得到四个用 AND 串在一起的短语句，每个语句都可以被视为知识库中的一个语句。

从那里开始，减少是机械的。

更新： 再一次，您需要添加您要证明的陈述的否定。你没有这样做，你添加了声明本身和另一个关于苹果是绿色的声明。不要那样做。你不是要证明苹果是绿色的，而是要证明玛丽只用青苹果做馅饼的说法。否定那个陈述，用你的其他三个知识库陈述解决它，并提取一个矛盾（也就是说，对于某个陈述 X，将 X 和 not-X 一起解决。）

那就是算法。有用。如果您不这样做，无论您是否“需要”，您正在做的不是分辨率算法，如果我给您的家庭作业/考试评分，我会将其评分为不正确。

更新 2：您越来越近了，但是您的查询语句需要一个关于 a 是 Apple 的附加子句（即 Apple(a)），因为您的其他几个语句已经有。它应该看起来几乎与仅使用 John's apples 的关于 Mary 的陈述（然后因为它是查询而被否定。）它的形式是正确的，用 AND 串在一起的小子句，你只是缺少一个。

但是请注意，一旦您有了这些，每个小从句（因为它们与 AND 串在一起）都可以在您的知识库中充当独立的语句。因此，例如，按照您现在制定的方式，您可以使用第三条语句的表达式来解析 Pie(p)。解析证明中有很多步骤，但是一旦你完全编码了查询否定，它们都是这样的微小步骤。

于 2012-06-10T17:16:43.230 回答
1

作为一般信息，您需要在 CNF 中有您的知识库和一个 NEGATED 目标（也在 CNF 中）。然后通过统一和应用解决方案，您需要有一个 nil 解决方案或目标状态本身。其他选择是无法找到其中任何一个并无限解决。

如果

Make(p,π,a)

在您的知识库中，然后将其与最后一个解决方案统一并应用解决方案，即：

⌐Make(M,π,a)

给你一个零解决方案。此时你可以停下来总结一下。

于 2012-06-11T15:39:26.070 回答