FOL (一阶逻辑) 中的归结

一阶逻辑 (FOL) 中的归结是应用于自动推理和逻辑编程的基本推理规则。它将命题逻辑中的归结原理推广到量词和谓词情况。该方法在合取范式 (CNF) 的子句上替换文字。它解析互补文字对并生成一个新子句，直到达到矛盾或无法进行更多归结。基于逻辑的人工智能和定理证明通常在归结方面进行推广。

归结是一种定理证明技术，它通过构建反驳证明来进行，即反证法。它由数学家 John Alan Robinson 于 1965 年发明。当给出各种陈述且我们需要从中证明一个结论时，就会使用归结。合一 (Unification) 是归结证明中的一个关键概念。归结是一种单一推理规则，可以有效地作用于合取范式或子句形式。

子句 (Clause): 文字的析取 (一个原子句) 称为子句。它也称为单元子句。

合取范式 (Conjunctive Normal Form): 表示为子句合取的句子称为合取范式或 CNF。

为什么使用归结？

归结是一种通用的方法，应用于与 AI 和自动推理相关的许多领域。以下是一些关于为什么选择归结的要点：

逻辑地证明陈述，归结应用矛盾来确定一个陈述是否为真。

自动化逻辑推理 - 使计算机能够进行逻辑推理，并从给定的事实中逻辑地推断出结论。

解决 AI 和逻辑编程中的问题 - 应用于 Prolog 和其他基于规则处理器的 AI 软件包。

知识库系统中的一致性 - 有助于识别不一致并保留有效信息。

验证软件和系统 - 它们确保软件、安全协议和硬件能够完美运行。

归结的关键组成部分

一阶逻辑 (FOL) 中的归结依赖于一些有影响力的方面，这些方面可以改进推理过程。它们是：

条款

子句是析取，这是基于归结证明的最简单形式。为了更好地理解子句，下面给出了一些示例：

P(x)¬Q(x) → 这样的表达式由两个用 OR 连接的文字组成；

¬ABC → 鉴于此表达式有三个文字，这意味着其中至少一个为真。

字面量

文字是原子命题 (事实) 或其否定。文字是子句的组成部分。文字看起来是这样的：

P(x) 是一个正文字，它为真或为假。

¬Q(y) 是事实的否定，是一个负文字。

合一 (Unification)

合一是连接两个 逻辑运算 的过程，其中为运算的歧义建立了值，以便它们的值相等。下面是一个合一的例子。

我们有两个谓词 - 谓词 1：Loves (x, Mary)。

谓词 2：Loves (John, y)。

为了合一这两个谓词，我们必须找到 x 和 y 的匹配项，使它们可以相等。通过将 x=John 和 y=Mary 代入，我们得到 Loves(John, Mary)。所以，合一后，这两个谓词就相同了。

替代

替换是指在逻辑语句中为特定表达式替换变量，使其等于特定值或词语。它有助于为合一、归结和推理规则做出具体的逻辑假设。下面给出一个替换的例子：

考虑带函数的谓词：Teaches(Prof, Subject)。替换 = {Prof/Dr. Smith, Subject/Mathematics} 得到 Teaches(Dr. Smith, Mathematics) 的结果。

斯科伦化 (Skolemization)

斯科伦化是通过引入斯科伦函数或常数来从公式中消除存在量词 () 的过程。

让我们考虑一个语句 x y Loves(x, y)，意思是“对每个 x，都存在某个 y，使得 x 爱 y”。

为了消除 y，我们用斯科伦函数 f(x) 来代替它，使得 x Loves(x, f(x))，因此 f(x) 指的是 x 所爱的一个特定人，所以上述语句就完全无量词了。

归结推理规则

一阶逻辑的归结规则只是命题规则的一个提升版本。当两个子句包含互补文字时，归结可以进行归结，假设这些文字已经标准化，以至于它们不共享变量。

其中，

• li 和 mj 是互补文字。
• 此规则也称为二元归结规则，因为它只归结精确的两个文字。

示例

我们可以归结两个子句，如下所示：

[Animal (g(x) V Loves (f(x), x)] 和 [￢ Loves(a, b) V ￢Kills(a, b)]

其中两个互补文字是：Loves (f(x), x) 和 ￢ Loves (a, b)

这些文字可以通过合一 θ= [a/f(x), and b/x] 进行合一，它将生成一个归结子句：

[Animal (g(x) V ￢ Kills(f(x), x)].

归结步骤

• 将事实转换为一阶逻辑。
• 将 FOL 陈述转换为 CNF。
• 否定需要证明的陈述 (反证法)。
• 绘制归结图 (合一)。
• 为了更好地理解以上所有步骤，我们将举一个例子，其中我们将应用归结。

示例

1. 约翰喜欢所有种类的食物。
2. 苹果和蔬菜是食物。
3. 任何人吃的东西且未被杀死的就是食物。
4. Anil 吃花生并且仍然活着。
5. Harry 吃 Anil 吃的一切。
6. 约翰喜欢花生。

步骤 1：将事实转换为 FOL

在第一步中，我们将所有给定的陈述转换为它们的一阶逻辑形式。

步骤 2：将 FOL 转换为 CNF

在一阶逻辑归结中，FOL 必须转换为 CNF，因为 CNF 形式使归结证明更容易。

消除所有蕴涵 (→) 并重写

1. ∀x ¬ food(x) V likes(John, x)
2. food(Apple) Λ food(vegetables)
3. ∀x ∀y ¬ [eats(x, y) Λ ¬ killed(x)] V food(y)
4. eats (Anil, Peanuts) Λ alive(Anil)
5. ∀x ¬ eats(Anil, x) V eats(Harry, x)
6. ∀x¬ [¬ killed(x) ] V alive(x)
7. ∀x ¬ alive(x) V ¬ killed(x)
8. Likes (John, Peanuts)。

将否定 (¬) 向内移动并重写

1. ∀x ¬ food(x) V likes(John, x)
2. food(Apple) Λ food(vegetables)
3. ∀x ∀y ¬ eats(x, y) V killed(x) V food(y)
4. eats (Anil, Peanuts) Λ alive(Anil)
5. ∀x ¬ eats(Anil, x) V eats(Harry, x)
6. ∀x ¬killed(x) ] V alive(x)
7. ∀x ¬ alive(x) V ¬ killed(x)
8. Likes (John, Peanuts)。

重命名变量或标准化变量

1. ∀x ¬ food(x) V likes(John, x)
2. food(Apple) Λ food(vegetables)
3. ∀y ∀z ¬ eats(y, z) V killed(y) V food(z)
4. eats (Anil, Peanuts) Λ alive(Anil)
5. ∀w¬ eats(Anil, w) V eats(Harry, w)
6. ∀g ¬killed(g) ] V alive(g)
7. ∀k ¬ alive(k) V ¬ killed(k)
8. Likes (John, Peanuts)。

通过消除存在量词的实例化

在此步骤中，我们将消除存在量词 ∃，这个过程称为斯科伦化。然而，在此示例问题中，由于没有存在量词，所有陈述在此步骤中都将保持不变。

删除全称量词

在此步骤中，我们将删除所有全称量词，因为所有陈述都已隐式量化，所以我们不需要它们。

1. ¬ food(x) V likes(John, x)
2. food(Apple)
3. food(vegetables)
4. ¬ eats(y, z) V killed(y) V food(z)
5. eats (Anil, Peanuts)
6. alive(Anil)
7. ¬ eats(Anil, w) V eats(Harry, w)
8. killed(g) V alive(g)
9. ¬ alive(k) V ¬ killed(k)
10. Likes (John, Peanuts)。

分配合取 ∧ 到析取 ¬ 上。

此步骤在此问题中不会有任何变化。

步骤 3：否定要证明的陈述

在此陈述中，我们将对结论陈述应用否定，将被写成 ¬likes (John, Peanuts)

步骤 4：绘制归结图

现在，在此步骤中，我们将通过使用归结树和替换来解决问题。对于上述问题，如下所示：

因此，结论的否定已被证明与给定陈述集完全矛盾。

归结图解释

• 在归结图的第一步中，¬likes(John, Peanuts) 和 likes(John, x) 通过替换 {Peanuts/x} 进行归结 (取消)，我们剩下 ¬ food(Peanuts)。
• 在归结图的第二步中，¬ food(Peanuts) 和 food(z) 通过替换 { Peanuts/z} 进行归结 (取消)，我们剩下 ¬ eats(y, Peanuts) V killed(y)。
• 在归结图的第三步中，¬ eats(y, Peanuts) 和 eats (Anil, Peanuts) 通过替换 {Anil/y} 进行归结，我们剩下 Killed(Anil)。
• 在归结图的第四步中，Killed(Anil) 和 ¬ killed(k) 通过替换 {Anil/k} 进行归结，我们剩下 ¬ alive(Anil)。
• 在归结图的最后一步中，¬ alive(Anil) 和 alive(Anil) 被归结。

AI 中归结的示例

归结是许多 AI 应用 (自动推理和逻辑推理) 的基础。这是如何看到实现归结到 AI 的一些关键示例。

AI 对自动定理证明的影响 - 归结用于在没有人为干预的情况下证明数学定理。归结用于 Lean theorem prover 和 Coq proof assistant 程序中测试数学证明。

专家系统 - AI 系统用于进行逻辑推理的规则推理过程。在医学诊断领域，MYCIN 等专家系统使用归结根据症状和患者来推断疾病。

自然语言处理 (NLP) - 无论您看向何处，我们都能找到 NLP 模型，如 IBM Watson 或每个人都喜欢的 Google 已经有些年头的 BERT，它们使用归结方法来发现单词之间的逻辑关系并改进语言理解过程。

归结的局限性

以下是逻辑推理中归结方法的局限性：

计算复杂度：它会生成许多中间子句，因此在使用大型知识库时速度很慢。

表达能力不足：转换为 CNF 限制了一种逻辑命题的表达能力。

处理无限域：递归定义、无限问题集，这些都是问题。

结论

在一阶逻辑 (FOL) 中，归结是一种强大的证明方法，通过从要从一组前提中推导出的内容的否定中推导出矛盾来实现。它通过将陈述转换为子句形式，并使用归结规则来达到矛盾。该方法合并具有公理化对偶文字的子句对，从而产生一个归结子句。

因此，一旦导出空子句，就意味着不一致，从而证明了该定理。归结可以完全且可靠地应用于 FOL，这意味着任何逻辑上有效的结论都可以根据可用信息的数量进行推导。尽管如此，由于 FOL 的声明性，其计算复杂度可能非常高。