A non-deterministic semantics for tractable inference

Unit resolution is arguably the most useful known algorithm for tractable reasoning in propositional logic. Intuitively, if one knows a, b, and a boolean AND b superset of c, then c should be an obvious implication. 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.