Paper Info
Title
The Completeness of Propositional Resolution: A Simple and Constructive Proof.
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.
Year
DOI
Venue
2006
10.2168/LMCS-2(5:3)2006
LOGICAL METHODS IN COMPUTER SCIENCE
Keywords
DocType
Volume
Resolution method,Unsatisfiability,Completeness,Constructive proof
Journal
2
Issue
ISSN
Citations 
5
1860-5974
1
PageRank 
References 
Authors
0.45
1
1
Name
Order
Citations
PageRank
Jean H. Gallier1749111.86