📜  一阶逻辑解析

📅  最后修改于: 2020-09-23 08:38:23             🧑  作者: Mango

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)得到解析。