一阶逻辑中的人工智能解释一阶逻辑中AI解释|人工智能

本文概述

解析度
解释推断规则
解决步骤
解释图的说明

解析度解析是一种定理证明技术，通过建立反驳证明（即，矛盾证明）来进行。它是由数学家John Alan Robinson于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形式使解析证明更容易。

消除所有隐含（→）并重写?x?食物（x）V赞（John，x）食物（Apple）Λ食物（蔬菜）?x?y?[eats（x，y）Λ?被杀死（x）] V食物（y）吃（Anil，花生）Λalive（Anil）?x?吃（Anil，x）V吃（Harry，x）?x?[?被杀死（x）] V alive（x）?x? alive（x）V?kill（x）喜欢（John，Peanuts）。
向内移动否定（?）并重写?x?食物（x）V喜欢（John，x）食物（Apple）Λ食物（蔬菜）?x?y?吃（x，y）V杀死（x）V食物（ y）吃（Anil，花生）Λalive（Anil）?x?吃（Anil，x）V吃（Harry，x）?x杀死（x）] V alive（x）?x?alive（x）V ?被杀（x）喜欢（John，Peanuts）。
重命名变量或标准化变量?x?食物（x）V赞（John，x）食物（苹果）Λ食物（蔬菜）?y?z?食用（y，z）杀死（y）V食用（z）吃（Anil，Peanuts）Λalive（Anil）?w?eats（Anil，w）V eats（Harry，w）?g?killed（g）] V alive（g）?k?live（k）V?killed（ k）点赞（John，Peanuts）。
通过消除消除存在的实例化量词。在这一步中，我们将消除存在量词?，此过程称为Skolemization。但是在此示例问题中，由于没有存在量词，因此在此步骤中所有语句将保持不变。
删除通用量词。在这一步中，我们将删除所有通用量词，因为并非所有语句都被隐式量化，因此我们不需要它。 ?食物（x）V喜欢（约翰，x）食物（Apple）食物（蔬菜）?吃（y，z）V被杀死（y）V食物（z）吃（Anil，花生）活着（Anil）?吃（ Anil，w）V吃（Harry，w）被杀死（g）V alive（g）?alive（k）V?被杀死（k）喜欢（John，Peanuts）。

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

将相交∧分布在相交?之上。此步骤不会对此问题进行任何更改。

步骤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）得到解析。