Reasoning with Models

Abstract

We develop a model-based approach to reasoning, in which the knowledge base is represented as a set of models (satisfying assignments) rather then a logical formula, and the set of queries is restricted. We show that for every propositional knowledge base (KB) there exists a set of characteristic models with the property that a query is true in KB if and only if it is satisfied by the models in this set. We fully characterize a set of theories for which the model-based representation is compact and provides efficient reasoning. These include cases where the formula-based representation does not support efficient reasoning. In addition, we consider the model-based approach to abductive reasoning and show that for any propositional KB, reasoning with its model-based representation yields an abductive explanation in time that is polynomial in its size. Some of our technical results make use of the Monotone Theory, a new characterization of Boolean functions introduced in [Bsh93]. The notion of restricted queries is inherent to our approach. This is a wide class of queries for which reasoning is very efficient and exact, even when the model-based representation KB provides only an approximate representation of the "world". Moreover, we show that the theory developed here generalizes the model-based approach to reasoning with Horn theories [KKS93], and captures even the notion of reasoning with Horn-approximations [SK91]. Our result characterizes the Horn theories for which the approach suggested in [KKS93] is useful and the phenomena observed there, regarding the relative sizes of the formula-based representation and model-based representation of KB is explained and put in a wider context.