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 ORCID

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.

Comment: 7 pages, submitted to LMCS

https://doi.org/10.2168/LMCS-2(5:3)2006
Source: arXiv.org:cs/0606084
Volume: Volume 2, Issue 5
Published on: November 7, 2006
Imported on: June 9, 2006
Keywords: Computer Science - Logic in Computer Science, Computer Science - Artificial Intelligence, F.4.1, I.2
Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 20201
Sources:
  • [1] zbMATH Open.

3 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3181 times.
This article's PDF has been downloaded 651 times.