Page 35 - 《软件学报》2026年第2期

514 软件学报 2026 年第 37 卷第 2 期

1.4 Superposition 演算

Superposition 演算是定理证明系统中最主流的推理系统 (inference system) [8,11,27] 之一. 定理证明问题可以视作
由特定理论下的一组公理 (axiom) 和一个待证明的断言 (conjecture) 组成.
推理 (inference): 大多数定理证明器基于一个推理系统来自动地化简和生成公式. 这一过程被称为推理
(inference), 由如下的规则 (rule) 表示:

F 1 ,F 2 ,...,F n
,
G
其中, F 1 ,F 2 ,...,F n 被称为前件 (premise), G 被称为推理的结论 (conclusion). 没有前件的推理称为公理 (axiom). 一
些推理规则的集合构成一个推理系统 (inference system). 在推理系统中作为输入的公式通常为合取范式 (clausal
normal form, CNF). 一般用 cnf(F) 来表示将公式 F 转为 CNF 形式的子句集合.
化简 (simplifying): 当一个或多个前件因为他们对给出结论冗余, 能够从公式集合中去掉时, 称这个操作为化
简 (simplify): 如 / F 1 ,F 2 ,...,F n 表示可将前件中的 F 1 消去.
G
合理和完备 (sound & complete): 当一个推理规则的结论在逻辑上由它的前件推出, 则该规则被称为合理的
(sound), 当一个推理系统的所有规则都是合理的, 则称这个推理系统为合理的; 当一个推理系统所有有效的公式集
合都能在该系统中被证明为 true, 则该推理系统被称为完备的 (complete).
反证完备 (refutationally complete): 我们称在推理系统中结论为否定 (一般用 ⊥ 表示) 的推理为“反证 (refutation)”.
反证完备指对任意不满足的公式集合, 都可以推理出空子句.
化简序 (simplification ordering): 在对 superposition 推理系统的具体推理规则进行介绍前, 我们首先引入化简
序 (simplification ordering) 概念. 化简序是通过在推理系统中引入一个“优先级”来在指导推理过程中如何选择和
化简子句: 选择子句指的是决定推理过程中需要被优先处理哪些子句, 化简子句指的是如何基于一些规则来删除
冗余子句或者简化复杂子句, 从而减少搜索空间.
l
我们用符号 ≻ 来表示化简序, 并将其扩展到文字、子句和等式上. 一个等式两边的 和 r, 如果有 l ≻ r, 则它们
的方向为 l = r. 项上的一个序 ≻ 若满足以下 4 种性质, 则称之为化简序: 1) ≻ 是良基的, 即存在项的有限序列
s s[l] ≻ s[r]. 3)
t 0 ,...,t n , 使得 t 0 ≻ t 1 ≻ ... ≻ t n . 2) ≻ 是单调的, 即如果 l ≻ r, 那么对任意项 , ≻ 在替换下保持稳定, 即如
θ lθ ≻ rθ. 4)
r
l
果 l ≻ r, 那么对任意替换 , ≻ 具有子项性质, 如果 是 的子项, 且 l , r, 那么 l ≻ r. 定义化简序的直观意
义是为了描述表达式之间“谁更加简单”, 从而更适合被推理系统优先处理.
例如当使用字典序作为化简序时, 基于符号字母顺序来定义序关系, 对于项 f(a,b) 和项 f(a,c), 字典序 a ≻ b ≻ c,
因此 f(a,b) ≻ f(a,c).
一种常用的化简序是 KBO (Knuth-Bendix ordering), 它基于权重和符号优先级. 预先定义符号的权重和优先
级, 先比较权重, 相同时再比较符号优先级来确定项之间的化简序.
,
例如定义符号优先级 f > g > a > b > c, 权重 w( f) = 2 w(g) = w(a) = w(b) = w(c) = 1, 表示令二元函数 f 的权重
,
,
要大于一元函数和常量. 那么对于项 f(a,b) 和 g(g(c)) w( f(a,b)) = w( f)+w(a)+w(b) = 4 w(g(g(c))) = w(g)+w(g)+
w(c) = 3, 于是 f(a,b) ≻ g(g(c)).
Superposition 演算: 大多数现代一阶定理证明器使用 superposition 演算作为他们的推理系统, 通常将 super-
.
position 推理系统简称为 Sup Sup 是合理 (sound) 且反证完备 (refutationally complete) 的. Sup 基于反证法来证明
公式成立, 称为 saturation-based proof search 过程 (将在第 3.1 节进行介绍).
Sup 推理系统的核心规则是 superposition 规则, 该规则最早提出是为了扩展归结 (resolution) 规则, 引入基于

等式的重写操作来化简公式. Superposition 名称的来源没有官方公认的说法, 原词字面意思是“叠加”或“重叠”, 可
能是由于 superposition 规则一般通过“等式理论”, 将公式项中某一位置的子项替换为另一个项, 然后基于归结原
理进行推理. 这一个操作是多个步骤的叠加, 也是将信息重叠到逻辑公式中某一位置的项进行传递.
Superposition 演算的推理规则如下.