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

**Previous Versions: Cornell Digital Repository:
http://dspace.library.cornell.edu/handle/1813/5754**

unofficial copies
[PDF],

by Wojciech Moczydlowski and Robert L. Constable

Cornell University Technical Report 2006-2061. Proceedings of Symposium on Logical Foundations of Computer Science (LFCS 2007), LNCS 4514, 147-161, Springer. Invited to the special issue of Annals of Pure and Applied Logic.

**Abstract**

We prove constructively that for any propositional formula
*Ø *in Conjunctive Normal Form, we can either
find a satisfying assignment of true and false to its variables, or a refutation
of *Ø *showing that it is unsatisfiable. T his refutation is a resolution
proof of *¬Ø. *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.