A New Method for Consequence Finding and Compilation in Restricted Languages

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Knowledge Representation

We introduce kernel resolution, a new complete method for first order consequence finding. The method generalizes Tison’s method for computing the prime implicates of a propositional theory, in three ways: it is first order, it supports incremental and lazy computation, and it is independent of any given search strategy. We also present two applications of the method. First, in the restricted form of skip-filtered kernel (SFK) deduction, it can be used for consequence-finding in restricted sublanguages, and for the related task of finding the LUB approximation of a theory; of special interest is its ability to obtain approximations of polynomial size (e.g. all implicates of size less than some constant). Directional resolution turns out to be an special case of SFK resolution. Second, we define an incremental version of one of the most successful knowledge compilation algorithms, with support for lazy and query-directed compilation.