Page 48 - 《软件学报》2026年第2期
P. 48

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


                 σ 1 )+σ 1 , 我们可以对公式  (11) 应用  IndGen  规则得到如下公式:

                                   ((0+(σ 1 +σ 1 )) = (0+σ 1 )+σ 1 ∧
                                   ∀x. (x+(σ 1 +σ 1 ) = (x+σ 1 )+σ 1 → s(x)+(σ 1 +σ 1 = (s(x)+σ 1 )+σ 1 )
                                   → ∀y. (y+(σ 1 +σ 1 ) = (y+σ 1 )+σ 1 )                             (15)
                    结合公式    (15) 和公式  (12), 则可以证明原命题, 一个完全的推理过程详见文献             [53].
                    归纳假设重写技术: 为了提升基于           saturation  的搜索证明过程效率, 通常我们需要确保在推理中规模大的项或
                 者文字总能被规模小的所重写           (这里的大小一般基于我们前面所定义的某种化简序关系                   ≻). 但在归纳推理中往往
                 经常需要使用归纳假设来重写结论, 而归纳假设的规模一般会更大, 这会与通常的规定产生冲突. Hajdú等人                               [54] 提
                 出归纳假设重写技术来克服这一冲突. 引入一个新的推理规则:

                                                 l = r ∨ D s[l] , t ∨C
                                                                  (IndHRW),
                                               cn f(F → ∀x. (s[r] = t)[x])
                                                                     ,
                                                                         ,
                 其中,   s[l] , t 是一个归纳结论的文字, 它对应的归纳假设文字是           l = r l ≺ r F → ∀x. (s[r] = t)[x] 是一个有效的归纳
                 公式. 这一规则的引入: 1) 使推理系统可以对归纳结论文字的一边用它的归纳假设进行重写                            (可以违反序关系限
                 制). 2) 可以在重写的归纳结论文字上进行归纳推理且不增加搜索空间.
                    上面我们介绍了在基于         superposition  的推理系统中引入归纳推理的主流归纳推理技术, 除此之外还有一些工
                 作有类似的尝试.
                    Cruanes 等人  [8] 将递归定义函数转换为推理系统中的重写规则, 然后基于                splitting  规则和一些启发式方法来
                 进行归纳推理中的子句选取和子目标引理生成. Cruanes 等人                [8] 的方法实现在  Zipperposition  这一工具中, 其主要
                 局限是只支持对代数数据类型的问题进行结构归纳, 另外他们的算法作为比较早期的尝试, 依赖集成在                                 AVATAR
                 的定理证明框架中进行逐例分析和引入特定的启发式优化.
                    Echenheim  等人  [52] 通过定义一系列推理规则增量式地生成归纳不变式的方式在自动定理证明系统中进行归
                 纳推理, 但他们的方法同样只适用于基于子项顺序定义的代数数据类型问题, 然后他们的算法需要在子句层面引
                 入一些额外约束条件, 然后在约束子句上将原来标准的重复子句消去算法进行扩展. 另外                            Echenheim  等人  [52] 只提
                 供了理论分析, 而没有提供将算法实现在真实工具中进行实现和对比实验的结果.
                    相比之下, Vampire 的系列工作基于        saturation  证明搜索框架这一层次进行归纳方法引入, 具有更高的抽象层
                 次, 适用性更广泛, 更易于扩展到其他定理证明系统和实现. 但他们依然在一些方面具有局限性, 例如对于公式规
                 模较大、递归结构较复杂、存在多个可归纳项的问题, 基于启发式归纳模式选择和子公式生成方法可能无法覆盖
                 到更一般的情况, 从而造成求解失败. 另外            Vampire 的系列方法所能处理的递归定义函数有限, 对于函数中包含分
                 支的附带条件或分支条件无法折叠到函数头中的更复杂的递归定义函数, 由于它们的良基性质不明显, 因此现有
                 算法还无法进行处理. 此外推理证明系统基于              saturation  的搜索证明框架, 目前还缺少对更丰富的理论进行有效求
                 解的支持, 从而可能使得自动定理证明器在求解混合理论问题上效率远低于基于                          DPLL(T) 框架的  SMT  求解器.
                  4   基于  CHC  的求解技术

                    在第  2  节和第  3  节中, 主要介绍了基于     SMT  求解器和定理证明推理系统求解带递归定义               SMT  公式的技术.
                 在本节中, 我们不直接处理通用形式的            SMT  公式, 而是考虑先将待求解的         SMT  公式转换为   CHC  形式, 然后利用
                 CHC  求解技术来进行求解. 由于       CHC  求解技术的特点, 这一种方法可以较好地作为直接求解                 SMT  公式方法的一
                 种补充. 这一点在第      5  节实验部分也将有所体现.
                    CHC  是一种特殊的一阶逻辑公式表现形式. 其最早引入是为了求解程序验证问题. 对于待验证程序, 将其编
                 码为一阶逻辑公式的验证条件后, 往往其中的变量是带有全称量词的, 而                      SMT  求解器对某些带量词的问题求解能
                 力有限. 为了对传统的       SMT  求解器进行补充, CHC     方法被提出. CHC    问题可以视作一类特殊的          SMT  问题, 它将
                 程序待验证条件表示成特殊的形式, 即            CHC  公式, 然后通过求解     CHC  公式的可满足性来对原程序待验证性质进
                 行验证. 基于   CHC  的验证方法往往有利于原程序中带有循环的问题, 因为                  CHC  求解技术通常会尝试生成循环不
   43   44   45   46   47   48   49   50   51   52   53