Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus

Abstract

We prove constructively that for any propositional formula $\phi$ in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of $\phi$ showing that it is unsatisfiable. This refutation is a resolution proof of $\lnot \phi$. From the formalization of our proof in Coq, we extract Robinson's famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.