Bart Selman, Henry Kautz
We present a new approach to developing fast and efficient knowledge representation systems. Previous approaches to the problem of tractable inference have used restricted languages or incomplete inference mechanisms - problems include lack of expressive power, lack of inferential power, and/or lack of a formal characterization of what can and cannot be inferred. To overcome these disadvantages, we introduce a knowledge compilation method. We allow the user to enter statements in a general, unrestricted representation language, which the system compiles into a restricted language that allows for efficient inference. Since an exact translation into a tractable form is often impossible, the system searches for the best approximation of the original information. We will describe how the approximation can be used to speed up inference without giving up correctness or completeness. We illustrate our method by studying the approximation of logical theories by Horn theories. Following the formal definition of Horn approximation, we present "anytime" algorithms for generating such approximations. We subsequently discuss extensions to other useful classes of approximations.