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, RobertMoczydlowski, Wojciech Keywords: computer sciencetechnical 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