Improving Coq Propositional Reasoning Using A Lazy Cnf Conversion Scheme

In all attempt to improve automation capabilities in the Coq proof assistant, we develop a tactic for the propositional fragment based oil 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 oil 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.