PB-277 Literal resolution: A Simple Proof of Resolution Completeness
DOI:
https://doi.org/10.7146/dpb.v18i277.6654Abstract
Literal resolution (LR) is a new resolution strategy for propositional calculus. Each step of LR involves a literal A. At an A-step of LR the old clause set S is replaced by a new clause set S' consisting of all the resolvents from S which involve A, together with those clauses of S which do not contain A or its negation. LR repeatedly formulates new clause sets in this way and further resolution does not need any old clause. LR is sound and complete. It is conceptually simple and easy to understand, and it provides an intuitive and straightforward proof for the completeness of the propositional version of Robinson resolution.Downloads
Published
1989-01-04
How to Cite
Zhang, G. Q. (1989). PB-277 Literal resolution: A Simple Proof of Resolution Completeness. DAIMI Report Series, 18(277). https://doi.org/10.7146/dpb.v18i277.6654
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.