It is well known that the resolution method (for propositional logic) iscomplete. However, completeness proofs found in the literature use an argumentby contradiction showing that if a set of clauses is unsatisfiable, then itmust have a resolution refutation. As a consequence, none of these proofsactually gives an algorithm for producing a resolution refutation from anunsatisfiable set of clauses. In this note, we give a simple and constructiveproof of the completeness of propositional resolution which consists of analgorithm together with a proof of its correctness.
展开▼
