A New Method for Consequence Finding and Compilation in Restricted Languages

SFK (skip-filtered, kernel) resolutionis a newmethod for finding"interesting"consequences of a first order clausaltheoryE, namely thosein some restricted target language£T. In its morerestrictive form, SFK resolution corresponds to a relatively efficient SAT method, directional resolution; in its moregeneral form, to a full primeimplicatealgorithm, namely Tison’s. It generalizesboth of themby offering much moreflexible search, first ordercompleteness, anda much widerrangeof inferentialcapabilities. SFKresolution has manyapplications: computing "characteristic"clausesfor task-specificlanguages in abduction, explanationand non-monotonic reasoning (Inoue 1992); obtaining LUB approximationsof the input theory (Selmanand Kautz1996)whichaxe polynomial size; incrementalandlazy exact knowledgecompilation (del Val1994); andcompilation into a tractable formfor restricted target languages, independently of the tractability of inferencein the given target language.

Authors

• Alvaro del Val Universidad Autónoma de Madrid
• Universidad Autènoma de Madrid

Keywords

No keywords are indexed for this paper.