本文概述
解析度
解析是一种定理证明技术，通过建立反驳证明（即，矛盾证明）来进行。它是由数学家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）得到解析。
