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

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

,
n,m ∈ Z n ⩽ m, 定义 sum(n,m) = n+(n+1)+...+m, 这里我们与前面的例子一样直接用公理形式表示函数定义:


∀n ∈ Z. sum(n,n) = n
 .

 ∀n,m ∈ Z. n ⩽ m → sum(n,m) = n+ sum(n+1,m)
φ = ∀n,m ∈ Z. n ⩽ m → 2×sum(n,m) = m×(m+1)−n×(n−1).
待验证断言为
从该问题中递归函数的定义可以看出, 对于 n 的定义区间不是常数, 且 sum(n,m) 的结果依赖 sum(n+1,m), 这
与简单的递归函数问题定义方向相反, 于是如 SMT 求解器中简单的数学归纳法实现无法处理这种类型的问题, 而
基于整数归纳模式公式 (7), 则例 11 的问题可以得到证明.
基于递归定义函数的归纳: 前面我们介绍了通过考虑固定的归纳推理函数模式, 如结构归纳和良基归纳等, 来
应用推理规则 Ind 的方法, Hajdú等人 [54] 则从另一种思路: 通过利用递归定义函数的方式来生成推理规则 Ind 中的
¯ s
归纳公式. 对于一个 n 元函数 f, 假设 f 的函数定义对应的公理子句为 f(¯s) = t ∨C, 这里 表示一个参数向量. 称
f(¯s) 为函数头 (function header), 称任意 f(¯s ) ⊴ t (这里 ⊴ 表示 f(¯s ) 是 t 的子项) 为这个函数头 f 的递归调用 (recursive
′
′
call). 对于函数 f 的第 i 个参数对应的递归调用 f(s i ), 这里 1 ⩽ i ⩽ n s i 是一个只包含构造子和变量的代数数据类型
,
项, 那么称这个 s i 为归纳参数. 于是可以通过函数定义的归纳参数生成归纳模式.
例 12: 以例 10 中的 half 函数为例, half 的递归定义公理分别为 half(O) = O half(s(O)) = O 以及 ∀z ∈ nat. half
,
(s(s(z))) = s(half(z)). 那么归纳模式的基础步骤可以由前两个公理中函数头的第 1 个参数 O 和 s(O) 生成. 归纳步骤
也对应于第 3 个公理. 其中函数头 half(s(s(z))) 有唯一的参数 s(s(z)). 这是一个代数数据类型项, 且对于递归调用
half(z) 的第 1 个参数 z, 有 z ⊴ s(s(z)). 于是这一公理可生成归纳模式的归纳步骤. 最终生成如下归纳模式的公式:

F(O)∧ F[s(O)]∧∀z. (F[z] → F[s(s(z))]) → ∀x. F[x].
从本例中可看出基于归纳函数定义的归纳模式生成方法, 可以更灵活地在推理系统中引入归纳模式, 而不局
限于固定的模式模板.
前面我们主要介绍了如何生成合适的归纳模式的一系列工作, 下面将介绍在帮助提升推理系统中进行归纳推
理效率的几种主要技术.
泛化归纳技术: 这一技术由 Hajdú等人 [53] 引入 superposition 推理系统中, 思路类似于第 2.3 节中引入子目标来
A 的一个泛化 (generalization)
证明原有命题: 当公式 A 难以直接证明时, 改为证明 B, 且 B → A. 这一过程称为证明
B. 在 SMT 求解以及定理证明工具中通常会基于一些启发式方法来猜测这样的一个子目标 (或者称为引理). 但在
基于 saturation 的推理证明过程中只能通过推理规则的形式来修改搜索的子句空间, 而不能直接用生成的子目标
公式来替换原目标公式, 因此为了在推理系统中使用子目标生成技术, Hajdú等人 [53] 提出推理系统中的泛化归纳技
术: 引入一个新的推理规则 IndGen, 使得推理中可以添加所生成的辅助公式 B 的实例, 然后可以使用在这些实例
上进行归纳推理. 这一规则公式如下:

¬L[t]∨C
(IndGen),
cn f(F → ∀x. L [x])
′
类似 Ind 规则, 这里 t 是基项, L 是基文字, C 是子句, F → ∀x. L [x] 是一个有效的归纳模式, 主要不同点在于这里
′
′
t
L [x] 是通过从 L[t] 中将某些 的出现替换为 x 获得.
例 x ∈ nat, 我们希望验证如下结合律性质成立:
13: 假设对于任意
∀x ∈ nat. (x+(x+ x)) = ((x+ x)+ x) (11)
对公式 (11) 使用 Ind 规则, 选择基于公式 (3) 中定义的归纳模式, 得到如下公式:

((0+(0+0)) =(0+0)+0∧∀x. (x+(x+ x) = (x+ x)+ x → s(x)+(s(x)+ s(x)) = (s(x)+ s(x))+ s(x))) →
∀y. (y+(y+y) = (y+y)+y) (12)
然后取反再进行斯科伦化, 得到下面两个子句:

0+(0+0) , (0+0)+0∨σ+(σ+σ) = (σ+σ)+σ (13)

0+(0+0) , (0+0)+0∨σ+(s(σ)+ s(σ)) = (s(σ)+ s(σ))+ s(σ) (14)
这一步之后推理系统无法进行进一步有效的推理. 但引入 IndGen 规则后, 令 t 是 σ 1 ¬L[t] 是 σ 1 +(σ 1 +σ 1 ) , (σ 1 +
,