Horn belief contraction: Remainders, envelopes and complexity

Belief change studies how to update knowledge bases used for reasoning. Traditionally belief revision has been based on full propositional logic. However, reasoning with full propo-sitional knowledge bases is computationally hard, whereas reasoning with Horn knowledge bases is fast. In the past several years, there has been considerable work in belief revision theory on developing a theory of belief contraction for knowledge represented in Horn form. Our main focus here is the computational complexity of belief contraction, and, in particular, of various methods and approaches suggested in the literature. This is a natural and important question, especially in connection with one of the primary motivations for considering Horn representation: efficiency. The problems considered lead to questions about Horn envelopes (or Horn LUBs), introduced earlier in the context of knowledge compilation. This work gives a syntactic characterization of the remainders of a Horn belief set with respect to a consequence to be contracted, as the Horn envelopes of the belief set and an elementary conjunction corresponding to a truth assignment satisfying a certain explicitly given formula. This gives an efficient algorithm to generate all remainders, each represented by a truth assignment. On the negative side, examples are given of Horn belief sets and consequences where Horn formulas representing the result of contraction, based either on remainders or on weak remainders, must have exponential size for almost all possible choice functions (i.e., different possible choices of partial meet contraction). Therefore using the Horn framework for belief contraction does not by itself give us computational efficiency. Further work is required to explore the possibilities for efficient belief change methods.