Skip to main content


eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
Authors: Constable, Robert
Moczydlowski, Wojciech
Keywords: computer science
technical report
Issue Date: 12-Dec-2006
Publisher: Cornell University
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.
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
TR2006-2061.pdf211.92 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us