veriT与Divvy：高效定理证明工具的探索

### veriT与Divvy：高效定理证明工具的探索 在自动化定理证明（ATP）领域，随着对大型理论证明需求的增长，开发高效且可靠的求解器变得至关重要。本文将介绍两款工具：veriT和Divvy，它们分别在满足性模理论（SMT）求解和公理选择方面有着独特的设计和优势。 #### veriT：开放、可信且高效的SMT求解器 veriT是一款由南锡大学、法国国家信息与自动化研究所（INRIA）和巴西北里奥格兰德联邦大学联合开发的SMT求解器。它为无量词公式逻辑、整数和实数上的差分逻辑及其组合提供了开放、可信且相当高效的决策过程，对应于SMT - LIB基准中的QF IDL、QF RDL、QF UF和QF UFIDL逻辑。 ##### 系统核心与特殊功能 - **推理核心**：veriT的推理核心使用SAT求解器生成输入公式布尔抽象的模型，然后将这些命题赋值交给理论推理器，该推理器是Nelson - Oppen风格的完全增量式决策过程组合，通过模型相等传播技术处理理论的非凸性，等式传播由同余闭包算法控制。 - **集成一阶证明器**：veriT继承了其前身haRVey的特点，集成了一阶逻辑（FOL）叠加证明器。该证明器在Nelson - Oppen组合中被视为一个“决策过程”，但由于运行成本高且非增量性，仅在最后才会调用。它从赋值中的量化子公式计算FOL理论，抽象基础子项以减少相关符号数量，并利用同余闭包信息抽象不包含相关符号的子项。如果证明器推断出给定公式集不可满足，会解析推导树以获取相关不可满足子集，构建冲突子句；若未证明不可满足，则将基础等式和推导的基础子句传播回veriT。目前使用E - prover作为一阶证明器，未来计划集成Spass。 - **宏定义**：veriT的输入格式是扩展了宏定义的SMT - LIB语言。宏定义对于编写包含简单集合构造的公式非常有用，经过β - 约简和谓词与函数等式重写后，得到的公式为一阶公式。如果不使用函数，它们属于Bernays - Schönfinkel - Ramsey片段，veriT可以使用嵌入式FOL证明器作为该片段的决策过程。此功能在一些工具（如CRefine）中用于生成基于集合的建模语言（如Circus）的验证条件。 - **证明生成**：证明生成有两个目标，一是增加对工具的信心，通过veriT内部的独立模块检查证明；二是让怀疑论的证明助手可以使用这些证明跟踪来重建veriT证明的公式。veriT已经可以为具有任意布尔结构和未解释函数的公式生成证明，并正在扩展到线性算术。 以下是一个简单的公式及其证明输出示例： ``` (benchmark example :logic QF_UF :extrafuns ((a U) (b U) (c U) (f U U)) :extrapreds ((p U)) :formula (and (= a c) (= b c) (or (not (= (f a) (f b))) (and (p a) (not (p b)))))) 1:(input ((and (= a c) (= b c) (or (not (= (f a) (f b))) (and (p a) (not (p b))))))) 2:(and ((= a c)) 1 0) 3:(and ((= b c)) 1 1) 4:(and ((or (not (= (f a) (f b))) (and (p a) (not (p b))))) 1 2) 5:(and_pos ((not (and (p a) (not (p b)))) (p a)) 0) 6:(and_pos ((not (and (p a) (not (p b)))) (not (p b))) 1) 7:(or ((not (= (f a) (f b))) (and (p a) (not (p b)))) 4) 8:(eq_congruent ((not (= b a)) (= (f a) (f b)))) 9:(eq_transitive ((not (= b c)) (not (= ```