CS245 Study Guide - The Algorithm, Propositional Calculus, Constructive Proof
Document Summary
It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing that if a set of clauses is unsatis able, then it must have a resolution refutation. As a consequence, none of these proofs actually gives an algorithm for producing a resolution refutation from an unsatis able set of clauses. In this note, we give a simple and constructive proof of the completeness of propositional resolution which consists of an algorithm together with a proof of its correctness. The resolution method for (propositional) logic due to j. a. Robinson [4] (1965) is well-known to be a sound and complete procedure for checking the unsatis ability of a set of clauses. In particular, none of these proofs yields (directly) an algorithm producing a resolution refutation from an unsatis able set of clauses.
