Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

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.

• Type: Conference
• Year: 2009
• Where: FROCOS
• Authors: Stéphane Lescuyer, Sylvain Conchon
• Keywords: Control Systems, Coq Proof Assistant, FROCOS 2009, Lazy Cnf Conversion, State-of-the-art Sat Solver