Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
复制标题
使用惰性 CNF 转换方案改进 Coq 命题推理
DOI：
10.1007/978-3-642-04222-5_18
复制
发表时间：
2009
期刊：
影响因子：
2.9
通讯作者：
S. Conchon
中科院分区：
文献类型：
--
作者：
Stéphane Lescuyer;S. Conchon
In an attempt to improve automation capabilities in the Coq proof assistant, we develop a tactic for the propositional fragment based on the DPLL procedure. Although formulas naturally arising in interactive proofs do not require a state-of-the-art SAT solver, the conversion to clausal form required by DPLL strongly damages the performance of the procedure. In this paper, we present a reflexive DPLL algorithm formalized in Coq which outperforms the existing tactics. It is tightly coupled with a lazy CNF conversion scheme which, unlike Tseitin-style approaches, does not disrupt the procedure. This conversion relies on a lazy mechanism which requires slight adaptations of the original DPLL. As far as we know, this is the first formal proof of this mechanism and its Coq implementation raises interesting challenges.
