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

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

¬p(a)∨k = b p(a)
(Bin).
k = b
由第 2 步结论 k = b 和条件 ¬p(k), 此时项中没有变量, θ 满足 k = kθ = bθ = b, 可应用 Dem 规则进行第 3 步
推理:

k = b ¬p(k)
(Dem).
¬p(bθ)
结论 ¬p(bθ) 化简为 ¬p(b). 由第 3 步结论和条件 p(b) 可由 Bin 规则进行最后一步推理:

¬p(b) p(b)
(Bin),
⊥
即假设 ¬∀x. p(x), 最终导出矛盾, 因此证明 ∀x. p(x) 成立.
3.2 在推理框架中引入自动归纳推理
在第 3.1 节介绍基于 saturation-based proof search 推理框架基础上, 我们介绍 Vampire 定理证明器近年来在这
一证明框架中引入自动归纳推理的一系列工作 [51,53–56] . 这一系列技术具有统一的思路和框架, 我们首先介绍这些
工作在自动定理证明推理系统中引入归纳推理技术的基本方法. 然后分别介绍每项工作在此基础上所提出的改进
或扩展方法. 对于待验证公式, 当尝试通过归纳推理进行推导证明时, 通常会产生两个待验证的相关子目标公式,
分别表示归纳法中的基本步骤 (base case) 和归纳步骤 (induction step case). 然后基于一种归纳模式 (induction
schema), 令推理系统可以通过归纳法的基本步骤与归纳步骤成立推导出原待验证目标成立.

例如待验证公式为 ∀x ∈ nat. F[x]. 那么会产生两个待验证子目标 F[O] 和 ∀z ∈ nat. (F[z] → F[s(z)]). 基于结构
归纳模式 (structural induction schema):

(F[O]∧∀z ∈ nat. (F[z] → F[s(z)])) → ∀x ∈ nat. F[x] (3)
可证明原公式 F. 这一过程实际上和在数学中使用结构归纳法完成数学命题的证明过程相同, 为了在推理系统中
完成证明, 2019 年 Regar 等人 [51] 提出在基于 saturation 证明搜索算法中引入一种表示归纳模式的推理规则来进行
归纳推导的方法: 在例 9 推导步骤第 2 步中, 选择表示归纳性质的公式集合 G, 然后生成一系列新的归纳公理

C 1 ,...,C n , 例如上文所提到的分别表示归纳基础步骤和归纳步骤的公式 F[O] 与 F[s(z)] 所对应的子句. 这一归纳推
理方法的实际使用主要依赖于两点: 1) 找到合适的归纳模式; 2) 开发高效的归纳推理规则来生成归纳公理或辅助
证明的公式. Regar 等人 [51] 引入如下归纳规则:

¬L[t]∨C
(Ind),
cnf(F → ∀x. L[x])
其中, t 是一个基项, L 是一个基文字 (ground literal), C 是一个子句, F → ∀x. L[x] 是一个有效的归纳模式. 这一规
则的直观思路是, 在推理证明过程中将待验证公式取反, 消去存在量词, 将得到包含基项的子句. 这一推理规则的
引入希望能使推理系统从这一待反驳子句自动生成相应的归纳模式, 即这里的推论中的公式 F → ∀x. L[x] 即对应
公式 3. F 表示基本步骤和归纳步骤的公式, ∀x. L[x] 表示待验证目标. 注意到推论公式等价于 ¬F ∨∀x. L[x], 实际
实现中会基于 binary resolution 规则, 只将 cn f(¬F ∨C) 加入当前子句的搜索空间中. 这一实现可以更好地引导推
理系统尽早选取所生成的用于归纳推理的子句进行下一步推理.
下面我们结合实际例子介绍 Vampire 的系列工作基于上述归纳推理框架分别在代数数据类型和整数类型上
的研究工作.
例 add、 hal f 分别对应如下公理:
10: 假设对于代数数据类型 nat, 递归定义函数 even 和

 add : ∀y ∈ nat. add(O,y) = y, ∀z,y ∈ nat. add(s(z),y) = s(add(z,y))





 even : even(O) = ⊤, ∀z ∈ nat. (even(s(z))) ↔ ¬even(z) .




 hal f : hal f(O) = O, hal f(s(O)) = O, ∀z ∈ nat. (half(s(s(z)))) = s(half(z))
待验证目标为 ∀x ∈ nat. even(x) → (x = add(hal f(x),hal f(x))).
在例 10 中将待验证目标取反, 再进行斯科伦化, 得到下面两个子句: