Abstract. A tableau calculus for ﬁrst-order circumscriptive reason-ing is developed. Parallel circumscription with ﬁxed and varyingpredicates with respect to Herbrand models is treated. First a newclausal tableau calculus for ﬁrst-order reasoning is developed whereahyper-typeruleiscombined witharestrictedanalytical cut rule.Theuse of a cut rule offersthe advantages that when deciding logical con-sequence the space of counter-models is searched with a preferenceto(subset) minimal (Herbrand) models and each counter-model isnotgenerated more than once. Then the calculus is extended to handleparallel circumscription. The circumscriptive calculus is sound in thegeneral case and complete when no function symbols are allowed.Low space complexity is obtained by employing a groundednessproperty of minimal models that enables a one branch at a time ap-proach to constructing tableaux for circumscriptive inference. 1 INTRODUCTION We study the automation of ﬁrst-order circumscriptive reasoning.Circumscription is a leading non-monotonic logic [6] and ithas beenapplied to formalizing inheritance reasoning, actions, plans, and thesemanticsoflogicprograms. Forexample, insomeofthemost promi-nent semantics of disjunctive logic programs circumscriptive reason-ing plays a key role [14].A number of approaches have been proposed to implement cir-cumscriptive inference [9, 7, 13, 12, 8, 10, 4, 1]. In some cases cir-cumscription can be replaced by equivalent ﬁrst-order formulas (see,e.g., [9, 4]). Some of the direct implementation approaches [8, 1]consider only a special subclass of circumscription which we callminimal model reasoning where there are no ﬁxed and varying pred-icates and all predicates are minimized. The approaches [7, 10, 12]handling more general forms of circumscription are essentially re-stricted to the case where the Herbrand universe is ﬁnite. The mostgeneral existing approach appears to be that of Przymusinski [13].He presents a resolution-based method for handling parallel circum-scription in the ground case and then outlines how the method canbe extended to cope with the non-ground case, too. However, themethod has some computationally unattractive features and it seemsto be unable to handle larger examples. This also holds for the otherapproaches [7, 10, 12, 8, 1] because of their exponential worst-casespace requirements.The goal of the paper is to develop a theorem proving method fora general form of circumscription with low space complexity. Werestrict ourselves to Herbrand models and consider parallel circum-scription [9] with both ﬁxed and varying predicates.Asabasisofourapproachweuseanalytictableauxbecausetableaumethods seem to be lend themselves to implementations of classicalreasoning with restricted space complexity. In order to achieve low
['Ilkka Niemelä']
Implementing Circumscription Using a Tableau Method