在Rocq中对DPLL转换系统的验证
Verification of a DPLL Transition System in Rocq
AI总结：
该研究在Rocq证明助手中对DPLL过程的抽象转换系统进行形式验证，形式化相关语法语义，证明关键属性，扩展系统，基于此引入策略概念并导出终止求解器且实现具体策略并验证其符合规范。
AI中文摘要：
我们在Rocq证明助手对Davis-Putnam-Logemann-Loveland（DPLL）过程的抽象转换系统表示进行形式验证。按照Nieuwenhuis等人的方法，SAT求解被建模为状态间基于规则的转换集而非具体算法。我们形式化命题公式的语法和语义，定义经典和基本DPLL转换系统并证明其关键元理论属性。特别地，建立了关于可满足性的正确性和完备性，通过表明转换关系是良基的来证明终止性。形式化还包括纯文字规则扩展原始抽象系统。基于已验证的转换系统，引入策略的抽象概念并从满足适当条件的任何策略导出终止求解器。然后在Rocq中实现具体策略并表明其满足策略规范。
英文摘要：
We present a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwenhuis et al., SAT solving is modeled as a set of rule-based transitions between states rather than as a concrete algorithm. We formalize the syntax and semantics of propositional formulas, define the classical and base DPLL transition systems, and prove their key metatheoretic properties. In particular, we establish correctness and completeness with respect to satisfiability, and we prove termination by showing that the transition relation is well-founded. The formalization extends the original abstract system by also including the pure literal rule. Building on the verified transition system, we introduce an abstract notion of strategy and derive a terminating solver from any strategy satisfying suitable conditions. We then implement a concrete strategy in Rocq and show that it satisfies the strategy specification.
