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

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


                 原无穷域上的递归函数公式转换为一个可以保持可满足行的有限域上的公式, 进而使得传统的实例化方法能够得
                 以应用. 该技术已经实现在       cvc5 求解器中, 实验结果显示其可以有效提升递归函数问题寻找可满足性赋值的求解能力.
                    由于处理复杂量词公式和无穷域参数的问题具有相当的挑战性, 另外递归函数问题的应用背景更多来自函数
                 式程序验证问题, 递归函数的可满足性这一方向研究相对较少. 我们认为进一步的研究工作可以从如下方向着手:
                 一是发展更强大的量词处理技术, 如针对特定理论的量词消去技术; 二是引入抽象等程序分析技术, 将原问题更好
                 地进行化简, 或转换到现有方法可处理的问题范围上完成求解.

                  3   自动推理系统的归纳推理技术

                    本节主要介绍近些年在自动推理系统中引入归纳推理等技术对带有递归定义的                             SMT  公式进行推导的技术.
                 基于自动推理系统进行        SMT  求解, 与  SMT  求解器基于   DPLL(T) 的求解框架具有很大区别, 目前主流的自动定理
                 证明器一般都基于       superposition  推理系统, 通过  saturation-based proof search  框架来对目标公式进行推导. 有一系
                 列工作考虑在     superposition  推理系统中引入归纳推理    [8,51–56] , 其中  Hajdú等人  [53,54,56] 和  Hozzová等人  [55] 的一系列技
                 术实现在自动定理证明器         Vampire 中, Cruanes 等人  [8] 的工作实现在自动定理证明器      Zipperposition  中. 下面本文
                 先介绍自动定理证明系统的推理框架, 然后分别介绍基于该推理框架的归纳推理技术.

                  3.1   Saturation-based proof search  推理框架
                    给定一个子句集合       S, 我们称基于推理系统       I  从  S  开始经过一系列推理规则生成的所有         S  的逻辑推论集合的
                 称为  S 的闭包. 当闭包中包含     ⊥ 时, 原子句集合    S 是不可满足的. 这一计算闭包的过程称为            saturation. 基于  saturation
                 的证明搜索策略是现在自动定理证明器的主流技术, 为了提高实际使用中的算法效率, 实际工具中会引入许多启
                 发式方法用于选取合适的推理子句、推理规则和简化搜索空间, 这里本文对基于                           saturation 的证明过程进行简单
                 介绍.
                    假设待验证问题由给定前提           (可称为公理) 和待验证问题组成, 假设前提子句的集合为                 A, 待验证问题子句集
                 合为  B, 如例  9  中,  A = {∀x. x = a∨ x = b, p(a), p(b)} B = {∀x. p(x)}. 算法的直观思路与基于  SMT  求解器进行证明
                                                        ,
                 相同: 通过给定前提, 证明待验证公式          ¬B 的不可满足性, 这一过程称为从          A 到  ¬B 的“反驳证明   (refutation)”. 具体
                 步骤如下.
                    1) 初始化  S  集合为  A∪¬B.
                    2) 选取当前待验证的性质所对应的子句集合              G, 基于推理系统    I  生成一系列推论     C 1 ,...,C n .
                                                               ⊥, 那么表示对原待验证命题取反作为前提时, 最终会
                    3) 将推论加入    S  的集合中, 若此时   S  的集合包括空集合
                 推导出   false 的结论, 于是我们证明了待验证命题成立. 否则重复上述过程.
                    注意到上面的算法步骤中我们没有给出如何证明待验证命题为反例或算法何时终止的判断, 在实际定理证明
                 系统中需要基于推理过程中推理规则的选取、未处理子句和重复子句的处理等过程来证明反例, 另外通常在给定
                 时间或空间资源耗尽还没有返回结果时返回               unknown. 具体算法过程和优化技术详见文献           [11,57].
                    这里我们通过一个简单的例子来初步理解               superposition  演算中各种规则的应用.
                    例  9: 假设我们的符号表中常数集合为          {a,b}, 即任意变量   x, 要么   x = a, 要么  x = b, 且对于命题  p、  p(a)、 p(b)

                 均成立. 要证明公式     φ = ∀x. p(x) 成立.
                    使用反证法的原理来证明          φ 成立, 推理过程如下: 首先假设       ¬∀x. p(x), 即  ∃x. ¬p(x) 成立, 将存在量词消去  (即
                                                                         ,
                 斯科伦化), 引入斯科伦常数       k, 有  ¬p(k) 成立. 由问题叙述,  ∀x. x = a∨ x = b p(a) 和  p(b) 均为前提条件公式. 于是令
                 θ : x 7→ k, 它是  x 和   的 k  mgu, 即  xθ = kθ. 由  Sup3  规则有第  1  步推理  (其中变量   x 的公式表示该公式对任意  x 成立,
                 全称量词被隐去):

                                                   x = a∨ x = b ¬p(k)
                                                                 (Sup3).
                                                    (¬p(a)∨ x = b)θ
                    第  1                       ¬p(a)∨k = b. 由第  1               p(a), 由  Bin  规则有第  2  步推理:
                        步结论   (¬p(a)∨ x = b)θ 化简为              步推理的结论和条件
   39   40   41   42   43   44   45   46   47   48   49