Incremental Recompilation of Knowledge

Nonmonotonic Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Belief Revision

Approximating a general formula from above and below by Horn formulas (its Horn envelope and Horn core, respectively) was proposed in [SIC] as a form of "' knowledge compilation," supporting rapid approximate reasoning; on the negative side, this scheme is static in that it supports no updates, and has certain complexity drawbacks pointed out in [KPS]. On the other hand, the many frameworks and schemes proposed in the literature for theory update and revision are plagued by serious complexity-theoretic impediments, even in the Horn case, as was pointed out in [EG2] and the present paper. More fundamentally, these schemes are not inductive, in that they lose in a single update any positive properties of the represented sets of formulas (small size, Horn, etc.). In this paper we propose a new scheme, incremental recompilation, combining Horn approximation and model-based updates; this scheme is inductive and very efficient, free of the problems facing its constituents. A set of formulas is represented by an upper and lower Horn approximation. To update, we replace the upper Horn formula by the Horn envelope of its minimum-change update, and similarly the lower one by the Horn core of its update; the key fact is that Horn envelopes and cores are easy to compute when the underlying formula is the result of a minimum-change update of a Horn formula by a clause. We conjecture that eficient algorithms are possible for more complex updates.