Skip to main content


eCommons@Cornell

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: http://hdl.handle.net/1813/5754
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
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2061
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.
URI: http://hdl.handle.net/1813/5754
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