Semantics of an Anytime Family of Reasoners.

Abstract

. An anytime family of propositional reasoners is a sequence R 0 ; R 1 ; : : : of inference relations such that each R i is sound, tractable, and makes more inferences than R i\\Gamma1 , and each theory has a complete reasoner in the family. Anytime families are useful for resource-bounded reasoning in knowledge representation systems. Although several anytime families have been proposed in the literature, only one of them has been provided with a model-theoretic semantics. We present model-theoretic semantics for a new anytime family of reasonersthat are basedon Boolean Constraint Propagation. For proving soundness and completeness results, we develop a new knowledge compilation technique called vivification. This allows us to obtain logically equivalent theories for which Boolean Constraint Propagation efficiently makes all logical inferences. 1 INTRODUCTION Since deductive reasoning is intractable for propositional knowledge representation systems, several tractable approaches for ...