Algorithms for Propositional KB Approximation

Abstract

One of the obstacles to the effective compilation of propositional knowledge bases (KBs) using Horn ap-proximations, as introduced by (Selman & Kautz 1991), is the lack of computationally feasible meth-ods for generating Horn bounds. In this paper new al-gorithms for generating Horn Greatest Lower Bounds (GLB) that can apply to large size KBs, are presented. The approach is extended through a more general tar-get language: the renamable Horn class. The condi-tions under which a renamable Horn formula is a re-namable Horn GLB of a KB are established and algo-rithms for computing it are derived. These algorithms can be used in the other approaches based on computa-tion of Horn or renamable lower bounds as (Boufkhad et al. 1997). The efficiency of these algorithms and the tightness with respect to the KB in terms of number of models of the bounds, are experimentally evaluated. The renamable Horn GLB proves to be closer to the KB than the Horn GLB.