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

TL;DR

This paper presents a straightforward, constructive proof of the completeness of propositional resolution, providing an explicit algorithm for generating resolution refutations from unsatisfiable clause sets.

Contribution

It introduces a simple, constructive proof that includes an algorithm for producing resolution refutations, improving upon traditional contradiction-based proofs.

Findings

Provides an explicit algorithm for resolution refutation construction

Proves the correctness of the algorithm for all unsatisfiable clause sets

Simplifies understanding of propositional resolution completeness

Abstract

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.