AI FOL解决方案
解决方案
解决方案是一种定理证明技术，通过建立反驳证明(即矛盾证明)来进行。它是由数学家约翰·艾伦·罗宾逊(John Alan Robinson)于1965年发明的。
如果给出各种陈述，则使用解决方案，我们需要证明这些陈述的结论。统一是决议证明中的关键概念。解析是一个单一的推理规则，可以有效地对合取范式或从句形式进行操作。
子句: 文字(原子句)的析取被称为条款。
合取范式: 表示为从句连词的句子称为合取范式或 CNF 。
注意: 为了更好地理解该主题，首先学习AI中的FOL。
分辨率推断规则:
一阶逻辑的分辨率规则只是命题规则的提升版本。如果两个子句包含互补的文字，则解析可以解析两个子句，假定它们是分开标准化的，因此它们不共享任何变量。
其中 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
第一步，我们将所有给定的语句转换为一阶逻辑。
步骤-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步: 绘制分辨率图:
现在，在此步骤中，我们将使用替换通过分辨率树解决问题。对于上述问题，将给出以下信息:
因此，结论的否定已被证明与给定的陈述完全矛盾。
"分辨率"图的说明:
在分辨率图的第一步中，通过替换来解决¬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）得到解析。
