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

冯维直 等: 带递归定义的 SMT 公式求解技术综述 525

even(σ 0 ) (4)

σ 0 , add(hal f(σ 0 ),hal f(σ 0 )) (5)
其中, σ 0 为常数 (类似于 SMT 中的斯科伦常数).
对于推理规则 Ind, Regar 等人 [51] 引入了结构归纳 (structural induction) 和良基归纳 (well-founded induction) 两
种归纳模式, 上述归纳模式均定义在代数数据类型理论上, 而 Hozzová等人 [55] 则考虑对整数理论的归纳推理进行
增强, 引入了整数归纳 (integer induction) 归纳模式. Hajdú等人 [54] 则区别于引入固定归纳模式的思路, 而是考虑基
于公理前提中递归函数的定义 (induction with recursive function definitions) 来生成规模模式, 使推理系统在选择归
纳模式时具有更高的灵活性和与公理前提的相关性. 下面分别对这些归纳模式进行介绍.
代数数据类型理论上的结构归纳: 基于结构归纳法的归纳模式分别选择代数数据类型的基础构造子和其他构
nat 理论上即实例化为公式 (3). 假设我们对公式 (5) 应用 Ind 规则,
造子作为基础步骤与归纳步骤的假设, 例如在
那么将得到对应 F → ∀x. L(x) 的公式为:

(O = add(hal f(O),half(O)))∧ (∀z ∈ nat. z = add(hal f(z),half(z)) → s(z) = add(hal f(s(z)),half(s(z))))
→ ∀x ∈ nat. x = add(hal f(x),hal f(x)),
然后这一公式中对应 F 的部分将如我们前文所述取反, 转换为相应子句加入推理系统当前的搜索空间之中.
代数数据类型理论上的良基归纳: 良基归纳模式和第 2.3 节中对 SMT 求解器引入归纳增强的原理类似. 实际
上结构归纳模式也可以视作良基归纳模式的一种特例. 定义项上的二元良基关系 R. 良基归纳的原理对应的形式
化公式如下:

∀x. (¬L[x] → ∃y. (R(y, x)∧¬L[y])) → ∀x. L[x] (6)
注意到这里的公式形式与第 2.3 节中公式 (2) 的形式略有区别, 但所表示意义是相同的 (实际上对公式 (2) 稍
作变形即可以得到公式 (6). 将 ∀x. (¬L[x] → ∃y. (R(y, x)∧¬L[y])) 转换为等价公式 ∀x. (L[x]∨∃y. (R(y, x)∧¬L[y])),
我们可以理解为要么对于任意项 x, 命题 L[x] 成立, 要么存在一个 R 关系下最小的项 y, 使得 L[y] 不成立.
良基归纳方法的实例同样类似于第 2.3 节, 实际推理系统中考虑 R 为代数数据类型中基于构造子和析构子
nat, 公式
的直接子项关系. 例如对于自然数的归纳定义 (6) 中的 R(y, x) 表示为 y 是 x 的直接子项 p(x), 于是 ∃y. (R(y,
x)∧¬L[y]) 实例化为 ∃y. (y = p(x)∧¬L[p(x)]).
整数归纳: 对于递归函数相关公式进行证明时, 往往需要考虑对整数理论或代数数据结构与整数的混合问题.
而现有工作往往专注于研究在代数数据结构理论的公式项上引入归纳推理, 而忽视整数理论的问题. 即使支持整
数理论的求解, 也只有最简单的实现, 例如 SMT 求解器中引入的归纳推理增强方法, 对于整数问题, 假设待验证函
数只考虑自然数区间, 并且取良基关系 R(s,t) 为 0 ⩽ s = t −1. 这一处理方式可以理解为 SMT 求解器对于整数理论
的问题只支持使用弱数学归纳法进行求解. Hozzová等人 [55] 则考虑整数理论问题中当变量定义在整数 Z 上时, 其
中的大于或小于关系不再是良基关系. 那么需要引入新的归纳推理模式来处理这一情况. 将原简单的自然数区间
Z 的具有上限 (upper bound) 或下限 (lower bound) 的子集. 那么此时这一个子集中的大于或小于
扩展为考虑任意
号具有良基性质, 可以进行归纳推理. 具体来讲, 引入如下 4 种归纳模式:

F[b]∧∀y ∈ Z. (y ⩽ b∧ F[y] → F[y−1]) → ∀x ∈ Z. (x ⩽ b → F[x]) (7)

F[b]∧∀y ∈ Z. (y ⩾ b∧ F[y] → F[y+1]) → ∀x ∈ Z. (x ⩾ b → F[x]) (8)

F[b 2 ]∧∀y ∈ Z. (b 1 < y ⩽ b 2 ∧ F[y] → F[y−1]) → ∀x ∈ Z. (b 1 ⩽ x ⩽ b 2 → F[x]) (9)

F[b 1 ]∧∀y ∈ Z. (b 1 ⩽ y < b 2 ∧ F[y] → F[y+1]) → ∀x ∈ Z. (b 1 ⩽ x ⩽ b 2 → F[x]) (10)
公式 (7)–(10) 分别描述了对于整数变量在指定符号化的上界、下界、区间约束下的归纳推理模式. 这些归纳
模式的引入可以扩展自动推理系统对整数理论问题的归纳推理能力, 处理形式更丰富的问题类型, 而不局限于将
变量定义域固定为自然数, 且递归函数的基础构造子只能从常数开始的问题.
例 11: 假设我们定义一个在 SMT 中整数理论下的函数 sum, 它用于计算从整数 n 到整数 m 的求和, 即对任意