A Non-Deterministic Semantics for Tractable Inference

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.