INCREMENTAL RECOMPILATION OF KNOWLEDGE

Approximating a general formula from above and below by Horn formulas (its Horn envelope and Horn core, respectively) was proposed by Selman and Kautz (1991, 1996) as a form of ''knowledge compilation,'' suppor ting rapid approximate reasoning; on the negative side, this scheme is static in that it supports no updates, and has certain complexity dra wbacks pointed out by Kavvadias, Papadimitriou and Sideri (1993). On t he other hand, the many frameworks and schemes proposed in the literat ure for theory update and revision are plagued by serious complexity-t heoretic impediments, even in the Horn case, as was pointed out by Eit er and Gottlob (1992), and is further demonstrated in the present pape r. More fundamentally, these schemes are not inductive, in that they m ay lose in a single update any positive properties of the represented sets of formulas (small size, Horn structure, etc.). In this paper we propose a new scheme, incremental recompilation, which combines Horn a pproximation and model-based updates; this scheme is inductive and ver y efficient, free of the problems facing its constituents A set of for mulas is represented by an upper and lower Horn approximation. To upda te, we replace the upper Horn formula by the Horn envelope of its mini mum-change update, and similarly the lower one by the Horn core of its update; the key fact which enables this scheme is that Horn envelopes and cores are easy to compute when the underlying formula is the resu lt of a minimum-change update of a Horn formula by a clause. We conjec ture that efficient algorithms are possible for more complex updates.