James M. Crawford, David W. Etherington
Unit resolution is arguably the most useful known algorithm for tractable reasoning in propositional logic. However, devising a tractable semantics that allows unit resolution has proven to be an elusive goal. We propose a 3-valued semantics for a tractable fragment of propositional logic that is inherently non-deterministic: the denotation of a formula is not uniquely determined by the denotation of the variables it contains. We show that this semantics yields a tractable, sound and complete, decision procedure. We generalize this semantics to a family of semantics, tied to Dalal’s notion of intricacy, of increasing deductive power and computational complexity.