FOL中的分辨率

解析度

解析是一种定理证明技术，通过建立反驳证明(即矛盾证明)来进行。它是由数学家JohnAlanRobinson于1965年发明的。

如果给出各种陈述，则使用解决方案，我们需要证明这些陈述的结论。统一是通过决议证明的关键概念。解析是一个单一的推理规则，可以有效地处理合取范式或从句形式。

子句：文字(原子句)的析取称为子句。它也被称为单位条款。

连词范式：表示为从句连词的句子称为连词范式或CNF。

注意：为了更好地理解该主题，首先要学习AI中的FOL。

分辨率推断规则：

一阶逻辑的解决规则只是命题规则的提升版本。如果两个子句包含互补的文字，则解析可以解析两个子句，假定它们是分开标准化的，因此它们不共享任何变量。

其中li和mj是互补文字。

此规则也称为二进制解析规则，因为它仅精确地解析两个文字。

例：

我们可以解决下面给出的两个子句：

[动物(g(x)V爱(f(x)，x)]和[￢Loves(a，b)V￢杀(a，b)]

其中两个互补文字是：Loves(f(x)，x)和￢Loves(a，b)

这些文字可以使用统一符θ=[a/f(x)和b/x]统一，它将生成一个resolvent子句：

[动物(g(x)V￢Kills(f(x)，x)]。

解决步骤：

• 将事实转换为一阶逻辑。
• 将FOL语句转换为CNF
• 否定需要证明的陈述(矛盾证明)
• 绘制分辨率图(统一)。

为了更好地理解上述所有步骤，我们将举一个应用分辨率的示例。

例：

• 约翰喜欢所有食物。
• 苹果和蔬菜是食物
• 任何人吃饭而不被杀死的都是食物。
• 阿尼尔(Anil)吃花生，还活着
• 哈利吃了安尼尔吃的所有东西。
  通过分辨率证明：
• 约翰喜欢花生。

步骤1：将事实转换为FOL

第一步，我们将所有给定的语句转换为其一阶逻辑。

步骤2：将FOL转换为CNF

在一阶逻辑解析中，需要将FOL转换为CNF，因为CNF形式使解析证明更容易。

• 消除所有隐含(→)并重写
  1. ∀x¬食物(x)V喜欢(John，x)
  2. 食物(苹果)Λ食物(蔬菜)
  3. ∀x∀y¬[吃(x，y)Λ¬被杀死(x)] V食物(y)
  4. 吃(茴香，花生)Λalive(茴香)
  5. ∀x¬吃(Anil，x)V吃(Harry，x)
  6. ∀x¬[¬被杀死(x)]活着(x)
  7. ∀x¬存活(x)V¬被杀死(x)
  8. 喜欢(约翰，花生)。
• 向内移动负(¬)并重写
  1. ∀x¬食物(x)V喜欢(John，x)
  2. 食物(苹果)Λ食物(蔬菜)
  3. ∀x∀y¬吃(x，y)杀死V(x)V食物(y)
  4. 吃(茴香，花生)Λalive(茴香)
  5. ∀x¬吃(Anil，x)V吃(Harry，x)
  6. ∀x杀(x)]活着(x)
  7. ∀x¬存活(x)V¬被杀死(x)
  8. 喜欢(约翰，花生)。
• 重命名变量或标准化变量
  1. ∀x¬食物(x)V喜欢(John，x)
  2. 食物(苹果)Λ食物(蔬菜)
  3. ∀y∀z¬吃(y，z)V杀死(y)V食物(z)
  4. 吃(茴香，花生)Λalive(茴香)
  5. ∀吃(阿尼尔，w)eat吃(哈利，w)
  6. 被杀死(g)V存活(g)
  7. ∀k¬存活(k)V¬被杀死(k)
  8. 喜欢(约翰，花生)。
• 通过消除消除存在的实例化量词。
  在这一步中，我们将消除存在量词∃，该过程称为Skolemization 。但是在此示例问题中，因为没有存在的量词，所以在此步骤中所有语句将保持不变。
• 删除通用量词。
  在这一步中，我们将删除所有通用量词，因为并非所有语句都被隐式量化，因此我们不需要它。
  1. ¬食物(x)V喜欢(约翰，x)
  2. 食品(苹果)
  3. 食物(蔬菜)
  4. ¬吃(y，z)V被杀死(y)V食物(z)
  5. 吃(茴香，花生)
  6. 活着的(Anil)
  7. ¬吃(Anil，w)V吃(Harry，w)
  8. 被杀死(g)活着(g)
  9. ¬存活(k)V¬被杀死(k)
  10. 喜欢(约翰，花生)。

注意：可以在两个单独的语句中编写“食品(苹果)Λ食品(蔬菜)”和“食用(茴香，花生)Λ活(茴香)”的语句。

• 将合取词∧分布在合取词¬之上。
  此步骤不会对此问题进行任何更改。

步骤3：否定要证明的陈述

在此陈述中，我们将对结论陈述应用否定，将其写为“likes”(约翰，花生)

步骤4：绘制分辨率图：

现在，在此步骤中，我们将使用替换通过分辨率树解决问题。对于上述问题，将给出以下内容：

因此，结论的否定被证明与给定的陈述完全矛盾。

分辨率图说明：

• 在分辨率图的第一步中，通过替换{Peanuts / x}来解决¬likes(John，Peanuts)和likes(John，x ) ，然后剩下¬food (Peanuts)
• 在分辨率图的第二步中，通过替换{Peanuts / z}来解决¬food(Peanuts)和food(z) ，并剩下¬eats(y，Peanuts)V kill(y ) 。
• 在分辨率图的第三步中， ¬eats(y，Peanuts)和eats(Anil，Peanuts)通过替换{Anil / y}进行解析，剩下Killed(Anil) 。
• 在分辨率图的第四步中， Killed(Anil)和¬kill(k)通过替换{Anil / k}得到解析，剩下¬alive(Anil) 。
• 在分辨率图的最后一步中， alive(Anil)和alive(Anil)得到解析。