A New Method for Consequence Finding and Compilation in Restricted Languages

Abstract

SFK (skip-filtered, kernel) resolution is a new method for finding "interesting" consequences of a first order clausal theory \\Sigma, namely those in some restricted target language LT . In its more restrictive form, SFK resolution corresponds to a relatively efficient SAT method, directional resolution; in its more general form, to a full prime implicate algorithm, namely Tison 's. It generalizes both of them by offering much more flexible search, first order completeness, and a much wider range of inferential capabilities. SFK resolution has many applications: computing "characteristic" clauses for task-specific languages in abduction, explanation and non-monotonic reasoning (Inoue 1992); obtaining LUB approximations of the input theory (Selman and Kautz 1996) which are of polynomial size; incremental and lazy exact knowledge compilation (del Val 1994); and compilation into a tractable form for restricted target languages, independently of the tractability of inference in the given ...