Computing intersections of Horn theories for reasoning with models

Model-based reasoning has been proposed as an alternative form of represent ing and accessing logical knowledge bases. In this approach, a knowledge ba se is represented by a set of characteristic models. In this paper, we cons ider computational issues when combining logical knowledge bases, which are represented by their characteristic models; in particular, we study taking their logical intersection. We present low-order polynomial time algorithm s or prove intractability for the major computation problems in the context of knowledge bases which are Horn theories. In particular, we show that a model of the intersection Sigma of Horn theories Sigma(1),...,Sigma(l) repr esented by their characteristic models, can be found in linear time, and th at some characteristic model of Sigma can be found in polynomial time. More over, we present an algorithm which enumerates all the models of Sigma with polynomial delay. The analogous problem for the characteristic models is p roved to be intractable, even if the possible exponential size of the outpu t is taken into account. Furthermore, we show that approximate computation of the set of characteristic models is difficult as well. Nonetheless, we s how that deduction from Sigma is possible for a large class of queries in p olynomial time, while abduction turns out to be intractable. We also consid er a generalization of Horn theories, and prove negative results for the ba sic questions, indicating that an extension of the positive results beyond Horn theories is not immediate. (C) 1999 Elsevier Science B.V. All rights r eserved.