PB-277 Literal resolution: A Simple Proof of Resolution Completeness

Abstract

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.