Jean Gallier - The Completeness of Propositional Resolution: A Simple and Constructive<br> Proof

lmcs:2234 - Logical Methods in Computer Science, November 7, 2006, Volume 2, Issue 5 - https://doi.org/10.2168/LMCS-2(5:3)2006
The Completeness of Propositional Resolution: A Simple and Constructive<br> ProofArticle

Authors: Jean Gallier

    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.


    Volume: Volume 2, Issue 5
    Published on: November 7, 2006
    Submitted on: June 9, 2006
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,F.4.1,I.2

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1433 times.
    This article's PDF has been downloaded 442 times.