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

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

∗ , app(x,nil) 进
余闭包 U 会增加等价类 {rev(x)} {app(rev(x),nil)} 和 {rev(app(rev(x),nil))}. 由于 app(rev(x),nil) 可由
行替换 σ := {x 7→ rev(x)} 得到, 且 app(x,nil) = x. 可将 {rev(x)} 与 {app(rev(x),nil)} 进行合并, 合并后代表项是 rev(x).
于是 app(rev(x),nil) 成为不规范 (non-canonical) 项, 从而子目标 φ 在 M 中可被过滤. 事实上由于等价类关系, φ 等
价于 ψ = ∀x. rev(rev(x)) = x, 因此 φ 被认为是冗余的候选子公式, 在生成中更倾向于保留 ψ 来替代 φ.
3) 基于基础事实 (ground fact) 过滤. 这一技术的直观思路是通过找到在当前上下文中可以推出的反例实例来
∀¯x. f(¯x) = g(¯x) 是否成立, 可通过考虑它的实例是否为
确定对应的候选子公式是否成立. 即对于 M 中候选子公式
假来判定, 如果 M 推出 ¬( f(¯x) = g(¯x))σ 对某个 ¯ x 上将自由变量替换为基项的替换 σ (称其为基础替换 grounding-
substitution, 替换后的实例称为基础实例 ground-instance) 成立, 那么显然有 ∀¯x. f(¯x) = g(¯x) 在 M 中不成立. 又由于
对公式 φ, 即使它在当前上下文中有反例, 但当上下文公式更新后, 可能并不包含这一反例, 因此对于某个候选子
M 中推出, 或只有少于某个设定的常数数量的实
公式 φ, 当它的任意基础替换得到的实例 ( f(¯x) = g(¯x))σ 都不能在
例可被推出, 也会将 φ 进行过滤.
例 7: 假设当前上下文 M = {sum(cons(O,k)) = plus(O, sum(k)), plus(O, sum(k)) = sum(k)}. 对于候选子公式 φ :=
∀x. sum(x) = s(O). 由于 φ 的任意基础替换得到的实例都不成立. 即使 φ 没有在 M 中为 false 的基础实例, 但由于 φ
的任意基础实例都不会被推出, 于是 φ 将被过滤.
上述 3 种过滤技术被实现在求解器 cvc5 中, 用于辅助归纳推理增强技术, 通过 cvc5 的选项“--quant-ind”调用,
可以较为有效地证明形式相对简单的递归函数问题. 但由于用于归纳增强的归纳模式较为简单, 这一方法无法较
好地处理形式更复杂的递归函数问题, 例如归纳基础需要考虑变量而不是常数时以及归纳定义不是简单的直接子
项时, 均无法有效完成证明. 近年来有许多工作基于 superposition 推理系统, 在自动定理证明器的推导中引入更复
杂的归纳模式, 使其可以处理递归定义更复杂的问题; 另外也有许多工作专注于提出各种子目标生成方法来更好
地在求解中生成有用的子公式从而提高命题公式求解能力. 这些技术将在后面的章节进行介绍.
2.4.2 其他子目标生成技术
在第 2.3 和 2.4.1 节中我们所介绍的技术是目前实现在主流 SMT 工具 cvc5 中的归纳推理和引理生成技术.
实际上还有许多方法/工具关注递归定义函数问题的求解, 包括 Scala 的程序验证工具 Leon/Stainless [32–34] 、交互式
定理证明器 Coq, Isabelle/HOL [35] 、半自动定理证明工具 ACL2 [36] 、自动定理证明工具 Zeno 等. 这些工具所支持
的输入形式一般是基于归纳类型构建的纯函数式语言, 如 haskell 等, 对这种语言的程序进行推理天然依赖归纳推
理技术. 其中有些工具依赖用户手动提供归纳推理过程, 如 Leon/Stainless 和 Coq 等, 而有些工具如 Zeno [37] 则实现
了自动的归纳推理. 由于这些技术主要属于程序分析/验证的层次, 且有些基于重写的证明系统与能进行 SMT 求
解的求解/推理系统具有较大区别, 为了更明确本文关注的主要问题, 不将主题范围过于扩大, 本文将不对上述技
术做详细介绍. 但这些工作中有些为求解递归定义函数的问题提出了比较通用的自动子目标生成技术, 可以在原
理上为带递归定义的 SMT 自动化证明提供一些启发思路, 因此下面我们简要对相关技术进行介绍和梳理.
基于泛化 (generalization) 生成辅助引理: 这一方法通常在基于推理系统的定理证明器中使用. 对于一个子目
标, 当无法直接证明时, 考虑引入一个假设, 或尝试将目标进行泛化. 对一个公式进行泛化, 即将原公式中的某些固
定子项用变量替换, 实际使用中需要通过一些启发式技术, 例如选取最小公共子项、反例检查等, 来选取合适的用
于泛化的子项, 并尽量避免过泛化 (over-generalization) 的情况. 如下例是一个使用泛化生成辅助引理的例子.
例 8: 考虑一个插入排序函数 list 类型:
insertsort. 它输入一个

sorted(nil) = ⊤





∀x. sorted(x) = ⊤




∀x,y,ys. sorted(x :: y :: ys) = x ⩽ y∧ sorted(y :: ys)






∀x. insert(x,nil) = x :: nil ,




∀x,y,ys. insert(x,y :: ys) = ite((x ⩽ y),(x :: y :: ys),(y :: insert(x,ys)))





insertsort(nil) = nil






∀x, xs. insertsort(x :: xs) = insert(x,insertsort(xs))