Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4662715 | Annals of Pure and Applied Logic | 2009 | 12 Pages |
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. This 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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic