自动推理（一）

一、简介

1.1 问题领域

1.2 语言表示

2. 演绎演算

2.1 分辨率

2.2 顺序推导

2.3 自然演绎

2.4 矩阵连接方法

2.5 术语重写

2.6 数学归纳法

3.其他逻辑

3.1 高阶逻辑

3.2 非经典逻辑

4. 应用

4.1 逻辑编程

4.2 SAT 求解器

4.3 演绎计算机代数

4.4 硬件的形式化验证

4.5 软件的形式化验证

4.6 逻辑与哲学

4.7 数学

4.8 人工智能

5. 结论

参考书目

学术工具

其他互联网资源

相关条目

一、简介

向自动推理程序提出的问题由两个主要项目组成，即表达所提出的特定问题的语句（称为问题的结论）和表达程序可用的所有相关信息（问题的假设）的语句集合。解决问题意味着通过系统地应用推理程序中嵌入的演绎规则来证明给定假设的结论。当找到这样一个证明时、当程序能够检测到证明不存在时、或者当它耗尽资源时，问题解决过程就会结束。

1.1 问题领域

自动推理程序设计中的第一个重要考虑因素是描述程序需要解决的问题类别——问题域。该域可以非常大，如一阶逻辑的通用定理证明器的情况，或者在范围上受到更多限制，如塔斯基几何或模态逻辑 K 的专用定理证明器。设计自动推理程序的典型方法是首先为其提供足够的逻辑能力（例如一阶逻辑），然后进一步将其范围划分为由一组领域公理定义的特定感兴趣领域。为了说明这一点，EQP（一个方程逻辑定理证明程序）被用来解决罗宾斯代数中的一个开放问题（McCune 1997）：所有罗宾斯代数都是布尔值吗？为此，该程序提供了定义罗宾斯代数的公理：

x+y=y+x（交换律）

( x+y)+z=x+(y+z) （结合性）

−(−( x+y)+−(x+−y))=x （罗宾斯方程）

然后该程序用于显示使用亨廷顿方程的布尔代数的表征，

−(−x+y)+−(−x+−y)=x，

由公理得出。我们应该指出，这个问题并不简单，因为确定有限方程组是否为布尔代数提供基础是不可判定的，也就是说，它不允许算法表示；此外，罗宾斯、亨廷顿、塔斯基和他的许多学生也对这个问题进行了研究，但没有成功。关键步骤是确定所有罗宾斯代数都满足

∃x∃y(x+y=x),

因为众所周知，这个公式是罗宾斯代数成为布尔代数的充分条件。当 EQP 获得这条信息时，程序通过自动完成证明提供了宝贵的帮助。

专用定理证明器的主要好处并不是通过将其注意力限制在领域公理上，而是从以下事实中获得：该领域可能享有特定的定理证明技术，这些技术可以在推理程序本身内进行硬连线（编码），并且可能会导致更有效的逻辑实现。 EQP 在解决罗宾斯问题方面的成功很大程度上归功于其内置的联想交换推理机制。

1.2 语言表示

构建自动推理程序的第二个重要考虑因素是决定（1）如何将其领域中的问题呈现给推理程序； (2) 它们在程序内部的实际表现如何； (3) 如何将找到的解决方案（完成的证明）显示回用户。有几种形式可用于此，并且选择取决于问题域和推理程序使用的基础演绎演算。最常用的形式包括标准一阶逻辑、类型化 λ 演算和子句逻辑。我们在这里讨论子句逻辑，并假设读者熟悉一阶逻辑的基础知识；对于类型化 λ 演算，读者可能需要查看 Church 1940。子句逻辑是一阶逻辑的无量词变体，并且是自动推理社区中使用最广泛的表示法。一些定义是按顺序排列的：术语是常量、变量或函数，其参数本身就是术语。例如，a,x,f(x) 和 h(c,f(z),y) 都是项。文字可以是原子公式，例如F(x)，或原子公式的否定，例如∼R(x,f(a))。如果一个文字是另一个文字的否定，则两个文字是互补的。子句是文字 l1∨…∨ln 的（可能为空）有限析取，其中文字在子句中不会出现多次（也就是说，子句也可以被视为文字集）。基本术语、基本文字和基本子句没有变量。空子句 [ ] 是没有文字的子句，因此是不可满足的——在任何解释下都是假的。一些例子：∼R(a,b) 和 F(a)∨∼R(f(x),b)∨F(z) 都是从句的例子，但只有前者是基础。总体思路是能够将问题的表述表达为一组子句，或者等效地，表达为合取范式 (CNF) 的公式，即子句的合取。

对于已经用标准逻辑符号表示的公式，有一个系统的两步过程将它们转换为合取范式。第一步是将公式重新表达为 prenex 范式中语义上等价的公式 (θx1)…(θxn)α(x1,…,xn)，由一串量词 (θx1)…(θxn) 组成由称为矩阵的无量词表达式 α(x1,…,xn) 表示。转换的第二步首先使用众所周知的逻辑等价（例如德摩根定律、分布、双重否定等）将矩阵转换为合取范式；然后，根据一定的规则删除现在处于合取范式的矩阵前面的量词。在存在量词的情况下，后一步并不总是保持等价性，并且需要引入 Skolem 函数，其作用是“模拟”存在量化变量的行为。例如，将 skolemizing 过程应用于公式

∀x∃y∀z∃u∀v[R(x,y,v)∨∼K(x,z,u,v)]

需要引入一位和两位 Skolem 函数，分别为 f 和 g，得出公式

∀x∀z∀v[R(x,f(x),v)∨∼K(x,z,g(x,z),v)]

然后可以删除全称量词以获得最终子句，在我们的示例中，R(x,f(x),v)∨∼K(x,z,g(x,z),v)。 Skolemizing 过程可能不会保留等价性，但会保持可满足性，这对于基于子句的自动推理来说已经足够了。

尽管从句形式提供了更统一、更经济的表示法（没有量词并且所有公式都是析取），但它也有一定的缺点。一个缺点是当从标准逻辑符号转换为分句形式时，结果公式的大小会增加。规模的增加伴随着认知复杂性的增加，这使得人类更难阅读用子句编写的证明。另一个缺点是，标准逻辑符号中公式的句法结构可以用来指导证明的构造，但该信息在转换为分句形式时完全丢失。

2. 演绎演算

构建自动推理程序的第三个重要考虑因素是选择程序将使用的实际演绎演算来执行其推理。如前所述，选择高度依赖于问题域的性质，并且有相当多的可用选项：通用定理证明和问题解决（一阶逻辑、简单类型论）、程序验证（一阶逻辑）顺序逻辑）、分布式和并发系统（模态和时态逻辑）、程序规范（直觉逻辑）、硬件验证（高阶逻辑）、逻辑编程（Horn 逻辑）、约束满足（命题子句逻辑）、数学（高阶逻辑）命令逻辑）、计算形而上学（高阶模态逻辑）等。

演绎演算由一组逻辑公理和一组演绎规则组成，用于从先前导出的公式导出新公式。解决程序问题域中的问题实际上意味着从由逻辑公理、域公理和问题假设组成的扩展集 Γ 中建立一个特定的公式 α（问题的结论）。也就是说，程序需要确定 Γ 是否蕴含 α,Γ⊨α。当然，程序如何建立这个语义事实取决于它实现的微积分。有些程序可能会采取非常直接的路线，并尝试通过实际从 Γ 构建 α 的逐步证明来建立 Γ⊨α 。如果成功，这当然表明 Г 导出——证明——α，我们用 Г⊢α 来表示这一事实。其他推理程序可能会选择更间接的方法，并尝试通过证明 Г∪{∼α} 不一致来建立 Ш⊨α，而这又通过从集合 Г∪{ 导出矛盾 ⊥ 来证明。 ∼α}。实现前一种方法的自动化系统包括自然演绎系统；后一种方法由基于解析、顺序演绎和矩阵连接方法的系统使用。

健全性和完整性是微积分的两个（元理论）属性，对于自动演绎尤为重要。稳健性表明微积分的规则是保真的。对于直接微积分，这意味着如果 Г⊢α 则 Г⊨α。对于间接演算，健全性意味着如果 Г∪{∼α}⊢⊥ 则 Г⊨α。直接微积分的完备性表明，如果 Г⊨α 则 Г⊢α。对于间接演算，完备性是用反驳的形式来表达的，因为我们通过证明证明的存在性来建立 Γ⊨α，而不是证明来自 Γ 的 α，而是证明来自 Γ∪{∼α} 的 ⊥。因此，如果 Γ⊨α 蕴涵 Γ∪{∼α}⊢⊥，则间接微积分反驳完成。在这两个属性中，稳健性是最理想的。不完全演算表明演算内部存在无法建立的蕴涵关系。对于自动推理程序来说，这非正式地意味着存在程序无法证明的真实陈述。不完整性可能是一件不幸的事情，但缺乏健全性是一个真正有问题的情况，因为不健全的推理程序将能够从完全真实的信息中生成错误的结论。

理解逻辑演算与其在推理程序中相应实现之间的区别很重要。微积分的实现总是涉及对微积分进行一些修改，严格来说，这会产生新的微积分。对原始微积分最重要的修改是其演绎规则的“机械化”，即规则应用的系统方式的规范。在此过程中，必须小心保留原始微积分的元理论性质。

对自动演绎很重要的另外两个元理论属性是可判定性和复杂性。如果微积分承认一种算法表示，那么它是可判定的，也就是说，如果存在一种算法，对于任何给定的 Γ 和 α，它可以在有限的时间内确定该问题的答案“是”或“否”问题“是否有 γ⊨α？”微积分可能是不可判定的，在这种情况下需要确定要实现哪个可判定片段。微积分的时空复杂度指定了其算法表示的效率。自动推理变得更具挑战性，因为许多感兴趣的计算是不可判定的，并且复杂性度量很差，迫使研究人员在演绎能力与算法效率之间寻求权衡。

2.1 分辨率

在用于实现推理程序的众多演算中，基于消解原理的演算是最受欢迎的。解析是根据链式法则（Modus Ponens 是其中的一种特例）建模的，本质上是从 p∨q 和 ∼q∨r 可以推断出 p∨r。更正式地，令 C−l 表示删除了文字 l 的子句 C。假设 C1 和 C2 是分别包含正文字 l1 和负文字 ~l2 的基本子句，使得 l1 和 ~l2 互补。然后，地面分辨率规则指出，作为解析 C1 和 C2 的结果，可以推断 (C1−l1)∨(C2−∼l2)：

C1C2

(C1−l1)∨(C2−∼l2)

赫布兰德定理（Herbrand 1930）向我们保证，任何一组条款的不可满足性，无论有无依据，都可以通过使用依据解析来确定。这对于自动推导来说是一个非常重要的结果，因为它告诉我们，如果无限多个解释中的任何一个都不满足集合 Γ，则可以通过有限多个步骤来确定这一事实。不幸的是，使用赫布兰德定理直接实现地面分辨率需要生成大量地面项，使得这种方法效率低下。通过将地面分辨率规则推广到二进制分辨率并引入统一概念，这个问题得到了有效解决（Robinson 1965a）。统一允许解决证明被“提升”并在更一般的层面上进行；子句只需要在需要解决时实例化。此外，实例化过程产生的子句不必是基础实例，并且仍然可以包含变量。二进制解析和统一的引入被认为是自动推理领域最重要的发展之一。

统一

两个表达式（术语或从句）的统一符是一种替换，当应用于表达式时使它们相等。例如，由下式给出的替代 σ

σ:={x←b,y←b,z←f(a,b)}

是一个统一者

R(x,f(a,y))

和

R(b,z)

因为当应用于两个表达式时，它们变得相等：

R(x,f(a,y))σ =R(b,f(a,b))

=R(b,z)σ

最通用的统一符 (mgu) 生成由两个统一表达式共享的最通用的实例。在前面的示例中，替换 {x←b,y←b,z←f(a,b)} 是统一符，但不是 mgu；然而，{x←b,z←f(a,y)}是一个mgu。请注意，统一尝试“匹配”两个表达式，这一基本过程已成为大多数自动演绎程序（基于解析的程序和其他程序）的核心组成部分。理论统一是统一机制的延伸，包括内置的推理能力。例如，子句 R(g(a,b),x) 和 R(g(b,a),d) 不统一，但它们 AC 统一，其中 AC 统一是与内置结合律和交换律的统一规则例如 g(a,b)=g(b,a)。将推理能力转移到统一机制中会增加功能，但要付出代价：两个统一表达式的 mgu 的存在可能不是唯一的（实际上可能有无限多个），并且统一过程通常变得不可判定。

二进制分辨率

令 C1 和 C2 为两个子句，分别包含正文字 l1 和负文字 ∼l2，使得 l1 和 l2 与 mgu θ 统一。然后，

C1C2

(C1θ−l1θ)∨(C2θ−∼l2θ)

通过二进制分辨率； (C1θ−l1θ)∨(C2θ−∼l2θ) 子句称为 C1 和 C2 的二元解析。

保理

如果子句 C 中出现的两个或多个文字共享一个 mgu θ，则 Cθ 是 C 的一个因子。例如，在 R(x,a)∨∼K(f(x),b)∨R(c,y) 中文字 R(x,a) 和 R(c,y) 与 mgu {x←c,y←a} 统一，因此，R(c,a)∨∼K(f(c),b) 是 a原来的因素条款。

解决原则

令C1和C2为两个子句。然后，将C1和C2解析得到的解析子定义为： (a)C1和C2的二元解析子； (b) C1 的二元解析和 C2 的因子； (c)因子C1和C2的二元解析；或者，(d)因子C1和因子C2的二元解析。

解析证明，更准确地说是反驳，是通过使用解析从 Γ∪{∼α} 导出空子句 [ ] 来构造的；如果 Γ∪{∼α} 不可满足，那么这总是可能的，因为解析是反驳完成的（Robinson 1965a）。作为解析证明的一个例子，我们证明集合 {∀x(P(x)∨Q(x)),∀x(P(x)⊃R(x)),∀x(Q(x)⊃ R(x))}，用 Γ 表示，蕴含公式 ∃xR(x)。第一步是找到 Γ∪{∼∃xR(x)} 的分句形式；所得到的子句集用 S0 表示，如下面反驳中的步骤 1 至 4 所示。反驳是通过使用水平饱和方法构建的：计算初始集合 S0 的所有解析项，将它们添加到集合中并重复该过程，直到导出空子句。 （这会产生越来越大的集合的序列：S0，S1，S2，...）我们施加的唯一约束是我们不会多次解析相同的两个子句。

S0 1 P(x)∨Q(x) 假设

2 ∼P(x)∨R(x) 假设

3 ∼Q(x)∨R(x) 假设

4 ∼R(a) 否定结论

S1 5 Q(x)∨R(x) 分辨率 1 2

6 P(x)∨R(x) 分辨率 1 3

7 ~P(a) 研究 2 4

8 ~Q(a) 研究 3 4

S2 9 Q(a) 研究 1 7

10 P(a) 研究 1 8

11 R(x) 分辨率 2 6

12 R(x) 分辨率 3 5

13 Q(a) 研究 4 5

14 P(a) 研究 4 6

15 R(a) 研究 5 8

16 R(a) 研究 6 7

S3 17 R(a) 研究 2 10

18 R(a) 研究 2 14

19 R(a) 研究 3 9

20 R(a) 研究 3 13

21 [ ] 决议 4 11

尽管解析证明成功地推导了[]，但它有一些明显的缺点。首先，反驳太长了，需要21步才能到达矛盾点[]。这是由于实现的简单暴力性质造成的。该方法不仅生成太多公式，而且有些公式显然是多余的。注意 R(a) 是如何导出六次的；此外，R(x) 比 R(a) 具有更多的“信息内容”，应该保留前者而忽略后者。与所有其他自动扣除方法一样，决议必须辅以旨在提高扣除过程效率的策略。上述示例推导有 21 个步骤，但研究型问题需要数千或数十万步的推导。

解决策略

在自动推理程序中成功实现演绎演算需要集成搜索策略，通过修剪不必要的演绎路径来减少搜索空间。有些策略一旦出现在推导中就会删除多余的子句或同义反复。另一种策略是通过称为包含的过程在存在更一般条款的情况下删除更具体的条款（Robinson 1965a）。然而，无限制包含并不能保持解析的反驳完整性，因此有必要限制其适用性（Loveland 1978）。模型消除（Loveland 1969）可以通过表明某个句子在公理的某些模型中是错误的来丢弃该句子。模型生成这一主题作为定理证明的补充过程而受到广泛关注。该方法已被自动推理程序成功使用，以显示公理集的独立性并确定满足某些给定标准的离散数学结构的存在性。

有些策略不是删除冗余子句，而是首先防止无用子句的生成。支持集策略（Wos, Carson & Robinson 1965）是此类策略中最强大的策略之一。集合 S 的子集 T，其中 S 最初是 Γ∪{∼α}，当且仅当 S−T 可满足时，称为 S 的支持集。支持集解析表明解析的子句并非都来自 S−T。支持集背后的动机是，由于集合 γ 通常是可满足的，因此最好不要解决 γ 中相互矛盾的两个子句。超分辨率（Robinson 1965b）通过将多个分辨率步骤组合成单个推理步骤来减少中间分辨率的数量。