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 b 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.

• Type: Conference
• Year: 1998
• Where: AAAI
• Authors: James M. Crawford, David W. Etherington
• Keywords: AAAI 1998, Intelligent Agents, Propositional Logic, Semantics, Unit Resolution