AI FOL解决方案

AI FOL解决方案

解决方案

解决方案是一种定理证明技术,通过建立反驳证明(即矛盾证明)来进行。它是由数学家约翰·艾伦·罗宾逊(John Alan Robinson)于1965年发明的。
如果给出各种陈述,则使用解决方案,我们需要证明这些陈述的结论。统一是决议证明中的关键概念。解析是一个单一的推理规则,可以有效地对合取范式或从句形式进行操作。
子句: 文字(原子句)的析取被称为条款。
合取范式: 表示为从句连词的句子称为合取范式或 CNF 。
注意: 为了更好地理解该主题,首先学习AI中的FOL。

分辨率推断规则:

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

AI FOL解决方案_https://bianchenghao6.com_【ai 教程】_第1张

其中 l
i 和 m
j
此规则也称为二进制解析规则,因为它只能解析两个文字。

示例:

我们可以解析下面给出的两个子句:
[动物(g(x)V爱[f(x),x)]和[[Loves(a,b)V ¬Kills(a,b)]
其中两个互补的文字是: Loves(f(x),x)和¬ Loves(a,b)
这些文字可以使用统一符θ= [a/f(x)和b/x]统一起来,它将生成一个解析子句:
[动物(g(x)V ¬ Kills(f(x),x)]。

解决步骤:

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

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

示例:

约翰喜欢各种食物。
苹果和蔬菜是食物
任何人吃饭而不被杀死都是食物。
Anil吃着花生,还活着
Harry吃掉了Anil吃的一切。
通过决议证明:

约翰喜欢花生。

步骤1: 将事实转换为FOL
第一步,我们将所有给定的语句转换为一阶逻辑。

AI FOL解决方案_https://bianchenghao6.com_【ai 教程】_第2张

步骤-2: 将FOL转换为CNF
在一阶逻辑解析中,需要将FOL转换为CNF,因为CNF形式使解析证明更容易。

消除所有含义(→)并重写 ∀x ¬ food(x) V likes(John, x) food(Apple) Λ food(vegetables) ∀x ∀y ¬ [eats(x, y) Λ ¬ killed(x)] V food(y) eats (Anil, Peanuts) Λ alive(Anil) ∀x ¬ eats(Anil, x) V eats(Harry, x) ∀x¬ [¬ killed(x) ] V alive(x) ∀x ¬ alive(x) V ¬ killed(x) likes(John, Peanuts).
向内移动取反(¬)并重写 ∀x ¬ food(x) V likes(John, x) food(Apple) Λ food(vegetables) ∀x ∀y ¬ eats(x, y) V killed(x) V food(y) eats (Anil, Peanuts) Λ alive(Anil) ∀x ¬ eats(Anil, x) V eats(Harry, x) ∀x ¬killed(x) ] V alive(x) ∀x ¬ alive(x) V ¬ killed(x) likes(John, Peanuts).
重命名变量或标准化变量 ∀x ¬ food(x) V likes(John, x) food(Apple) Λ food(vegetables) ∀y ∀z ¬ eats(y, z) V killed(y) V food(z) eats (Anil, Peanuts) Λ alive(Anil) ∀w¬ eats(Anil, w) V eats(Harry, w) ∀g ¬killed(g) ] V alive(g) ∀k ¬ alive(k) V ¬ killed(k) likes(John, Peanuts).
通过消除消除存在的实例化量词。
在这一步中,我们将消除存在量词∃,该过程称为 Skolemization 。但是在此示例问题中,由于没有存在量词,因此所有语句在此步骤中将保持不变。

丢弃通用量词。
在这一步中,我们将删除所有通用量词,因为并非所有语句都被隐式量化,因此我们不需要它。 ¬ food(x) V likes(John, x) food(Apple) food(vegetables) ¬ eats(y, z) V killed(y) V food(z) eats (Anil, Peanuts) alive(Anil) ¬ eats(Anil, w) V eats(Harry, w) killed(g) V alive(g) ¬ alive(k) V ¬ killed(k) likes(John, Peanuts).

注意: 语句" food(Apple)Λfood(vegetables)"和" eats(Anil,Peanuts)Λalive(Anil)"可以用两个单独的语句编写。

将相合词∧分布在不相交对象¬上。
此步骤不会对此问题做出任何更改。

第3步: 否定要证明的陈述
在此陈述中,我们将否定应用于结论陈述,即将被写为like(约翰,花生)
第4步: 绘制分辨率图:
现在,在此步骤中,我们将使用替换通过分辨率树解决问题。对于上述问题,将给出以下信息:
AI FOL解决方案_https://bianchenghao6.com_【ai 教程】_第3张因此,结论的否定已被证明与给定的陈述完全矛盾。

"分辨率"图的说明:

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