The Completeness of Propositional Resolution: A Simple and Constructive<br> Proof
<|reference_start|>The Completeness of Propositional Resolution: A Simple and Constructive<br> Proof: 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.<|reference_end|>
@article{gallier2006the,
    title={The Completeness of Propositional Resolution: A Simple and
  Constructive<br> Proof},
    author={Jean Gallier},
    journal={Logical Methods in Computer Science, Volume 2, Issue 5 (November
  7, 2006) lmcs:2234},
    year={2006},
    doi={10.2168/LMCS-2(5:3)2006},
    archivePrefix={arXiv},
    eprint={cs/0606084},
    primaryClass={cs.LO cs.AI}
}