*Goran Gogic, Christos H. Papadimitriou, Martha Sideri*

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.