定理证明机

9.5.7 定理证明机

定理证明机（也称自动推理机）和逻辑程序设计语言在两个方面有差异。首先，大多数逻辑程序设计语言只处理霍恩子句，而定理证明机接受全部一阶逻辑。其次，Prolog程序中逻辑和控制缠绕在一起。程序员选择A :- B而不是A :- C,B将会影响程序的执行。在大多数定理证明机里，语句句法形式的选择不会影响结果。定理证明机依然需要控制信息以有效运转，但是该信息通常不同于知识库，并不是作为知识表示自身的一部分。定理证明机中的大部分研究涉及寻找一般情况下有用的控制策略，以及提高速度的方法。

一、定理证明机的设计

在这部分内容里，我们将描述定理证明机OTTER（Organized Technique for Theorem proving and Effective Research，定理证明和有效搜索的组织化技术）（McCune，1992），并特别关注它的控制策略。在为OTTER准备一个问题的时候，用户必须将知识分解成4个部分：

• 称为支撑集（set of support，或称sos）的一个子句集，该集合定义了与问题有关的重要事实。每一步归结都用支撑集的一个成员和另外一条公理进行归结，因此搜索将集中于支撑集。

• 支撑集之外的可用公理集。这些公理提供了关于问题领域的背景知识。问题的部分（并因此放在sos中）和背景知识之间的界限取决于用户的判断。

• 一个被称为重写或者解调器的等式集。虽然解调器是等式，但是它们总是按照从左到右的方向被应用。因此，它们定义了一个规范形式，所有的项都要被简化成为这样的规范形式。例如，解调器x+0 = x意思是每一个形为x+0的项都应该被项x取代。

• 一个定义控制策略的参数和子句集。特别是，用户要指定一个用于控制搜索的启发式函数以及一个用于消除某些不感兴趣的子目标的过滤函数。

OTTER的工作原理是对某个可用公理持续归结支撑集中的某一个元素。和Prolog不同，它采用最佳优先搜索的一种形式。它的启发式函数度量每个子句的“重量”，比较轻的子句优先级高。启发式的确切选择在于用户，但是一般来说，子句的重量应该和它们的大小和难度有关。单元子句被认为是轻的；搜索因此可以被视为单元优先策略的一般化。在每一步，OTTER将支撑集中“最轻”子句移动到可用表中，并把最轻子句与可用表的元素归结得到的某些直接结果添加到可用表中。当找到一个否证或者当支撑集中不再有子句时，OTTER就会停机。详细的算法如图9.14所示。

图9.14 OTTER定理证明机的架构。在对“最轻”子句的选择中和从考虑中排除不感兴趣的子句的FILTER函数中应用了启发式控制

二、扩展Prolog

构造定理证明机的另一种方法是从Prolog编译器开始，对它进行扩展，以得到一个可靠的、完备的完全一阶逻辑推理机。这是Prolog技术定理证明机（Prolog Technology Theorem Prover，PTTP）（Stickel, 1988）中采用的方法。PTTP包含了对Prolog进行的5项意义重大的改变，以恢复完备性和表达能力：

• 为了使合一例程可靠，发生检测被放回到合一例程中。

• 用迭代深入搜索取代深度优先搜索。这使得搜索策略完备，且只增加了常量时间。

• 否定文字（诸如¬P(x)）是允许的。在实现中，有两个独立的例程，一个试图证明P，另一个试图证明¬P。

• 一个有n个原子项的子句以n条不同的规则存储。例如，A ⇐ B∧C也会被保存为¬B ⇐ C∧¬A和¬C ⇐ B∧¬A。这项技术被称为锁定，表示当前目标只需要与每个子句的头合一，不过它还考虑到对否定子句进行适当的处理。

• 增加线性归结规则以使推理完备（甚至对于非霍恩子句也是完备的）：如果当前目标与栈中的某个目标的否定合一，那么可以认为那个目标已经解决。这是通过反证进行推理的方法。假设原目标为P，并且通过一系列推理归约到目标¬P，这确定了¬P P，它逻辑等价于P。

除了这些变化以外，PTTP保留了使得Prolog运行快速的特性。合一仍然是通过直接对变量进行修改来完成的，而解除绑定是通过在回溯过程中对踪迹栈进行退栈操作来完成的。搜索策略仍然基于输入归结，意味着每次归结都针对问题的原始语句中给出的某个子句（而不是导出子句）进行。这使得它适合用于对问题原始语句中的所有子句进行编译。

PTTP 的主要缺点在于：用户不得不放弃对归结搜索的所有控制。每条推理规则以其原始形式和逆否命题形式被系统所使用。例如，考虑如下规则：

(f(x, y) = f(a, b)) ⇐ (x = a) ∧ (y = b)

作为Prolog的规则，这是一种证明两个f项相等的合理方式。但是PTTP还会生成逆否命题：

(x ≠ a) ⇐ (f(x, y) ≠ f(a, b)) ∧ (y = b)

这似乎是证明任意两个项x和a不相同的一种啰嗦的方法。

三、作为助手的定理证明机

到目前为止，我们已经把推理系统当作一个独立的智能体，它需要自主决策并且行动。定理证明机的另一种用途是作为助手，比方说，给数学家提供建议。这种模式下，数学家扮演监督者的角色，制定用于决定下一步如何做的策略，并要求定理证明机补充细节。这在一定程度上减轻了问题的半可判定性，因为如果查询耗费太多的时间，那么监督者可以取消查询，并尝试另外一种方法。定理证明机还可以作为证明检验机，其中证明是由人给出的一系列数量相当大的步骤；证明每个步骤都可靠所需要的单独的推理由系统来填写。

苏格拉底式推理机是一个定理证明机，它的ASK函数不完备，但是如果对它提出正确的问题序列，那么它总可以得出一个解。因此倘若有一个监督者，他给出了正确的ASK调用序列，苏格拉底式推理机就是一个优秀的助手。ONTIC（McAllester，1989）是一个用于数学的苏格拉底式推理系统。

四、定理证明机的实际应用

定理证明机已经提供了新的数学结果。SAM(Semi-Automated Mathematics，半自动数学)程序是第一个，它证明了格理论中的一个引理（Guard等人，1969）。AURA项目也回答了多个数学领域尚未解决的问题（Wos和Winker，1983）。波耶尔-摩尔定理证明机（Boyer和Moore，1986）已经得以应用并经过多年的扩展，Natarajan Shankar用它给出了哥德尔不完备性定理（Shankar，1986）的第一个充分严格的形式证明。OTTER程序是最强大的定理证明机之一，它曾经用于解决组合逻辑中的一些未决问题。这些定理证明机里最著名的一个和Robbins代数相关。1933年，Herbert Robbins提出一个似乎可以定义布尔代数的简单公理集，但是无法找到证明（尽管包括Alfred Tarski自己在内的几个数学家对此进行了认真的研究）。1996年10月10日，在经过8天的计算之后，EQP（OTTER的一个版本）找到了一个证明（McCune，1997）。

定理证明机可以在涉及硬件和软件的验证和合成的问题中应用，因为这两个领域都可以进行正确的公理化。因此，对定理证明进行研究的领域还包括硬件设计、程序设计语言和软件工程——而不只是人工智能。在软件的例子中，公理陈述了程序设计语言的每个句法元素的属性。（对程序进行推理与情景演算中对行动进行推理类似。）通过证明算法的输出符合所有输入的规格要求来对算法进行验证。RSA公钥密码算法和波耶尔-摩尔字符串匹配算法都通过这种方式进行了验证（波耶尔和摩尔，1984）。在硬件的情况中，公理描述了信号和电路元件之间的相互作用。（实例可参见第八章）。AURA对16位加法器的设计进行了验证（Wojcik，1983）。为验证而特别设计的逻辑推理机已经可以验证整个CPU，包括它们的时钟特性（Srivas和Bickford，1990）。

Cordell Green（1969a）根据先前西蒙（1963）的想法，勾勒了算法的形式合成，它是定理证明机最初的用途之一。它的思路是证明定理有这样的效果：“存在一个程序 p，它满足一定的规格。”如果证明被约束为构造性的，那么程序可以被抽取出来。尽管全自动的演绎合成，正如它的名字，还无法适用于通用的程序设计，手动指导的演绎合成已经在一些最新的复杂算法的设计中成功实现。专用程序的合成也是一个活跃的研究领域。在硬件合成领域中，AURA定理证明机已经应用于设计比先前的任何设计更紧凑的电路（Wojciechowski和Wojcik，1983）。对于很多电路设计，命题逻辑就足以满足要求，因为需要关注的命题集被电路元件集合所限定。现在，命题推理在硬件合成中的应用已经成为一项标准技术，有很多大规模的具体应用（例如，参见Nowick等人（1993））。

同样的这些技术现在也逐渐通过诸如SPIN模型检验器（Holzmann, 1997）之类的系统应用于软件验证中。例如，远程智能体宇宙飞船控制程序在飞行之前和之后都需要进行检验（Havelund等人，2000）。