\input zb-basic
\input zb-ioport
\iteman{io-port 05200144}
\itemau{Gallier, Jean H.}
\itemti{The completeness of propositional resolution: A simple and constructive proof.}
\itemso{Log. Methods Comput. Sci. 2, No. 5, Paper 3, 7 p., electronic only (2006).}
\itemab
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 unsatisfiable, 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 unsatisfiable 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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.2168/LMCS-2(5:3)2006}
\end