Semantical and Computational Aspects of Horn Approximations

Abstract

In a recent study Selman and Kautz proposed a method, called Horn approzimation, for speeding up inference in propositional Knowledge Bases. Their technique is based on the compilation of a propositional formula into a pair of Horn formulae: a Horn Greatest Lower Bound (GLB) and a Horn Least Upper Bound (LUB). In this paper we address two questions that have been only marginally addressed so far: 1) what is the semantics of the Horn approximations? 2) what is the exact complexity of finding Horn approximations? We obtain semantical as well as computational results. The major results of the former kind are: Horn GLBs are closely related to models of the circumscription; reasoning wrt the Horn L UB can be mapped into classical reasoning. The major results of the latter kind are: finding a Horn GLB is "mildly" harder than solving the original inference problem; finding the Horn LUB is a search problem that cannot be parallelized. We believe that our results provide useful criteria that may help finding a knowledge compilation policy.