Complexity of Nested Circumscription and Abnormality Theories

1 Introduction

Circumscription is a very powerful method for knowledge representation and common-sense reasoning, which has been used for a variety of tasks, including temporal reasoning, diagnosis, and reasoning in inheritance networks. The basic semantical notion underlying circumscription is minimization of the extension of selected predicates. This is especially useful when a predicate is meant to represent an abnormality condition, e.g., a bird which does not fly. Circumscription is applied to a formula ✠ , either propositional or first-order, and it is used to eliminate some unintended models of ✠ .

Since the seminal definition of circumscription in [McCarthy, 1980], several extensions have been proposed (see, e.g., Lifschitz's survey [1994]), all of them retaining the basic idea of minimization. In this paper, we propose a0 ✁ ✄ ✆ ✞ , a language which extends propositional circumscription in two important and rather natural ways:

1. on one hand, we allow the propositional combination of circumscriptive theories;
2. on the other hand, we allow nesting of circumscriptions.

As for the former extension, we claim that it can be useful in several cases. As an example, when different sources of knowledge ☛ ☞ ✌ ✍ ✏ ✠ ✓ ✕ and ☛ ☞ ✌ ✍ ✏ ✠ ✗ ✕ coming from two equally trustable agents who perform circumscription are to be integrated, it seems plausible to take their disjunction, i.e., Thomas Eiter Georg Gottlob Institut f¨ ur Informationssysteme Technische Universit¨ at Wien Favoritenstrasse 9, A-1040 Wien, Austria eiter@kr.tuwien.ac.at gottlob@dbai.tuwien.ac.at

☛ ☞ ✌ ✍ ✏ ✠ ✓ ✕ ✚ ☛ ☞ ✌ ✍ ✏ ✠ ✗ ✕ 1 . In a0 ✁ ✄ ✆ ✞ , all propositional connectives are allowed.

As for the latter extension, the original idea of nested abnormality theories (NATs) has been proposed by Lifschitz [1995], and its usefulness for the formalization of narratives has been shown by Baral et al. [1998]. Nesting circumscription is useful for the modularization of a knowledge base. As an example concerning diagnosis of an artifact designed in a modular way, e.g., a car, a piece of knowledge ☛ ☞ ✌ ✍ ✏ ✠ ✓ ✕ may model the intended behavior of a subpart, e.g., the engine. Analogously, ☛ ☞ ✌ ✍ ✏ ✠ ✗ ✕ may model the intended behavior of the electrical part. Further unintended models can be eliminated by taking the circumscription of a suitable propositional combination of ☛ ☞ ✌ ✍ ✏ ✠ ✓ ✕ , ☛ ☞ ✌ ✍ ✏ ✠ ✗ ✕ , and a plain propositional formula encoding observations.

In this paper, we are mainly concerned with the computational properties of a0 ✁ ✄ ✆ ✞ and NATs and with their relationship to plain circumscription. In particular, we tackle the following questions:

• ✦ Can NATs be embedded into a0 ✁ ✄ ✆ ✞ ?
• ✦ What is the precise complexity of reasoning under nested circumscription? By reasoning, we mean both model checking and formula inference from an a0 ✁ ✄ ✆ ✞ or NAT theory.
• ✦ Is there a simple restriction of NATs (and thus of a0 ✁ ✄ ✆ ✞ ) for which some relevant reasoning tasks are feasible in polynomial time?

We are able to give a satisfactory answer to all these questions. In particular, in Section 3, after providing a precise definition of a0 ✁ ✄ ✆ ✞ , we prove the main results about its complexity: model checking and inference are shown to be PSPACEcomplete (the latter even for literals); moreover, complexity is proven to increase w.r.t. the nesting. It appears that nesting, and not propositional combination, is responsible for the increase in complexity. Similar results are proven for NATs in Section 4, where we also prove that every NAT can be easily (and polynomially) translated into a formula of a0 ✁ ✄ ✆ ✞ .

Given the high complexity of nested circumscription, we look for significant fragments of the languages in which complexity is lower, and focus on Horn NATs: it is proven in Section 4 that here nesting can be efficiently eliminated if fixed variables ❆ are not allowed, and both model checking and inference are polynomial. Section 5 compares a0 ✁ ✄ ✆ ✞ and NATs to other generalizations of circumscription such as prioritized circumscription [Lifschitz, 1985; 1994] and theory curbing [Eiter et al., 1993; Eiter and Gottlob, 2000].

1 We remind that ✩ ✪ ✬ ✭ ✮ ✰ ✲ ✳ ✵ ✩ ✪ ✬ ✭ ✮ ✰ ✸ ✳ ✻ ✼ ✩ ✪ ✬ ✭ ✮ ✰ ✲ ✵ ✰ ✸ ✳ in general (take, e.g., ✰ ✲ ❀ ❁ ❂ ❄ , ✰ ✸ ❀ ❄ ).

Our results prove that the expressive power that makes a0 ✁ ✄ ✆ ✞ andNATs useful tools for themodularization of knowledge has indeed a cost, because the complexity of reasoning in such languages is higher than reasoning in a "flat" circumscriptive knowledge base. Anyway the PSPACE upper bound of the complexity of reasoning, and the similarity of their semantics with that of quantified Boolean formulas (QBFs), makes fast implementations possible by translating them into a QBF and then using one of the several available solvers, e.g., [Rintanen, 1999]. This approach could be used also for implementing meaningful fragments of NATs, such as the one in [Baral et al., 1998], although this might be inefficient, like using a first-order theorem prover for propositional logic.

Given that QBFs can be polynomially encoded into NATs, we can show (in the full paper) that nested circumscription is more succinct than plain (unnested) circumscription, i.e., by nesting ❇ ❈ ❊ ● operators (or NATs), we can express some circumscriptive theories in polynomial space, while they could be written in exponential space only, if nesting were not allowed. In this sense, we add new results to the comparative linguistics of knowledge representation [Gogic et al., 1995].

2 Preliminaries

We assume a finite set ❍ ■ of propositional atoms, and let a0 ✏ ❍ ■ ✕ (for short, a0 , if ❍ ■ does not matter or is clear from the context) be a standard propositional language over ❍ ■ . For any formula ◆ ❖ a0 , we denote by ◗ ❘ ❚ ✏ ◆ ✕ the set of its models. Capitals ❱ , ❲ , ❳ etc stand for ordered sets of atoms, which we also view as lists. If ❨ ❩ ❭ ❫ ✓ ❴ ❵ ❵ ❵ ❴ ❫ ❛ ❝ and ❨ ❞ ❩ ❭ ❫ ❞ ✓ ❴ ❵ ❵ ❵ ❴ ❫ ❞ ❛ ❝ , then ❨ ❣ ❨ ❞ denotes the formula ❥ ❛ ❦ ❧ ✓ ✏ ❫ ❦ ♥ ❫ ❞ ❦ ✕ .

The extension of a model ♣ on atoms ❍ is denoted by ♣ a113 ❍ a115 . We denote by ❣ ✉ ✈ ✇ the preference relation on models which minimizes ❱ in parallel while ❳ is varying and all other atoms are fixed; i.e., ♣ ❣ ✉ ✈ ✇ ♣ ❞ (♣ is more or equally preferable to ♣ ❞ ) iff ♣ a113 ❱ a115 ① ♣ ❞ a113 ❱ a115 and ♣ a113 ❲ a115 ❩ ♣ ❞ a113 ❲ a115 , where ❲ ❩ ❍ ■ ⑧ ❱ ⑨ ❳ and ① and ❩ are taken componentwise. As usual, ♣ ❷ ✉ ✈ ✇ ♣ ❞ means ♣ ❣ ✉ ✈ ✇ ♣ ❞ ❹ ♣ ❼ ❩ ♣ ❞ .

We denote by ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ the second-order circumscription [Lifschitz, 1985] of the formula ◆ where the atoms in ❱ are minimized, the atoms in ❳ float, and all other atoms are fixed, which is defined as the following formula:

Here ❱ ❞ and ❳ ❞ are lists of fresh atoms (not occurring in ◆ ) corresponding to ❱ and ❳ , respectively. The second-order formula (1) is a quantified Boolean formula (QBF) with free variables, whose semantics is defined in the standard way. Its models, i.e., assignments to the free variables such that the resulting sentence is valid, are the models ♣ of ◆ which are

❱ ❿ ❳ -minimal, where a model ♣ of ◆ is ❱ ❿ ❳ -minimal, if no model ♣ ❞ of ◆ exists such that ♣ ❞ ❷ ✉ ✈ ✇ ♣ .

3 Language ➉ ➊ ➌ ➎ ➏

The language a0 ✁ ✄ ✆ ✞ extends the standard propositional language a0 (over a set of atoms ❍ ■ ) by circumscriptive atoms. Formulas of a0 ✁ ✄ ✆ ✞ are inductively built as follows:

1. ➐ ❖ a0 ✁ ✄ ✆ ✞ , for every ➐ ❖ ❍ ■ ;
2. if ◆ , ➒ are in a0 ✁ ✄ ✆ ✞ , then ◆ ❹ ➒ and ➓ ◆ are in a0 ✁ ✄ ✆ ✞ ;
3. if ◆ ❖ a0 ✁ ✄ ✆ ✞ and ❱ ❴ ❳ are disjoint lists of atoms, then ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ is in a0 ✁ ✄ ✆ ✞ (called circumscriptive atom).

Further Boolean connectives ( ✚ , ♥ , etc) are defined as usual. The semantics of any formula ◆ from a0 ✁ ✄ ✆ ✞ is given in terms of models of a naturally associated QBF → ✏ ◆ ✕ , which is inductively defined as follows:

1. → ✏ ➐ ✕ ❩ ➐ , if ◆ is an atom ➐ ❖ ❍ ■ ; 2. → ✏ ◆ ❹ ➒ ✕ ❩ → ✏ ◆ ✕ ❹ → ✏ ➒ ✕ and → ✏ ➓ ◆ ✕ ❩ ➓ → ✏ ◆ ✕ ;

Note that in 3, the second-order definition of circumscription is used to map the circumscriptive atom to a QBF which generalizes the circumscription formula in (1). In particular, if ◆ is an "ordinary" propositional formula (◆ ❖ a0 ), then → ✏ ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ ✕ coincides with the formula in (1).

Example 1 Consider the formula

• ◆ ❩ ❇ ❈ ❊ ● ✏ ❇ ❈ ❊ ● ✏ ➐ ✚ ➳ ❿ ➐ ❿ ➳ ✕ ✚ ❇ ❈ ❊ ● ✏ ➳ ✚ ✍ ❿ ➳ ❿ ✍ ✕ ❿ ➐ ❿ ✍ ✕ ❵ Applying rule 3 to inner circumscriptions we get → ✏ ◆ ✕ ❩ ❇ ❈ ❊ ● ✏ ✏ ➳ ❹ ➓ ➐ ✕ ✚ ✏ ✍ ❹ ➓ ➳ ✕ ❿ ➐ ❿ ✍ ✕ . Applying rule 3 again we get → ✏ ◆ ✕ ❩ ✏ ➓ ➐ ❹ ➓ ➳ ❹ ✍ ✕ ✚ ✏ ➓ ➐ ❹ ➳ ✕ ❩ ➓ ➐ ❹ ✏ ➳ ✚ ✍ ✕ .

As usual, we write ♣ ➽ ❩ ◆ if ♣ is a model of ◆ , and ◆ ➽ ❩ ➒ if ➒ is a logical consequence of ◆ .

Eliminating fixed letters

As shown in [de Kleer and Konolige, 1989], the fixed letters can be removed from an ordinary circumscription. The same technique can be applied for formulas from a0 ✁ ✄ ✆ ✞ as well. More precisely, let ◆ ❩ ❇ ❈ ❊ ● ✏ ➒ ❿ ❱ ❿ ❳ ✕ be a circumscriptive atom. For each letter ➪ ➶ ❖ ❱ ⑨ ❳ , introduce a fresh letter ➹ ➪ , add ➪ , ➹ ➪ to ❱ , and add a conjunct ➪ ➘ ➓ ➹ ➪ to ➒ . Let ◆ ❞ ❩ ❇ ❈ ❊ ● ✏ ➒ ❞ ❿ ❱ ❞ ❿ ❳ ✕ be the resulting circumscriptive atom. Then, the following holds.

Proposition 1 ◆ and ◆ ❞ are equivalent modulo the set of all auxiliary letters ➹ ➪ .

Using this equivalence, we can eliminate all fixed letters from a formula ➴ ❖ a0 ✁ ✄ ✆ ✞ , by replacing each circumscriptive atom ◆ in ➴ with ◆ ❞ , where the fresh atoms ➹ ➪ are made floating inside ◆ ❞ and outside ◆ . Note that the resulting formula ➴ ❞ has size polynomial in the size of ➴ .

3.1 Complexity results

Let the ❇ ❈ ❊ ● -nesting depth (for short, nesting depth) of ◆ ❖ a0 ✁ ✄ ✆ ✞ , denoted ➬ ➮ ✏ ◆ ✕ , be the maximum number of circumscriptive atoms along any path in the formula tree of ◆ .

Theorem 1 Model checking for a0 ✁ ✄ ✆ ✞ , i.e., deciding whether a given ➱ interpretation ♣ is a model of a given formula ◆ ❖ a0 ✁ ✄ ✆ ✞ , is PSPACE-complete. If ➬ ➮ ✏ ◆ ✕ ❣ ❐ for a constant ❐ ❮ ❰ , then the problem is complete for a207 ✉ a208 a209 ✓ a113 a210 ✏ a211 a212 a213 ➬ ✕ a115 , i.e., polynomial time with a210 ✏ a211 a212 a213 ➬ ✕ many calls to an oracle for a214 ✉ a208 , where ➬ is the input size.

Proof: (Sketch) Clearly, any formula ◆ ❖ a0 ✁ ✄ ✆ ✞ can be encoded, by definition, to aQBF → ✏ ◆ ✕ (not necessarily in prenex form) in polynomial time. Thus deciding, ♣ ➽ ❩ ◆ is in PSPACE. By an inductive argument, we can see that for any circumscriptive atom ◆ ❩ ❇ ❈ ❊ ● ✏ ➒ ❿ ❱ ❿ ❳ ✕ such that ➬ ➮ ✏ ◆ ✕ ❣ ❐ , deciding ♣ ➽ ❩ ◆ is in a217 ✉ a208 . Thus for any Boolean combination ◆ of atoms and circumscriptive atoms ◆ ✓ ❴ ❵ ❵ ❵ ❴ ◆ a218 such that ➬ ➮ ✏ ◆ ✕ ✏ ❩ a219 a220 a221 a218 ❦ ❧ ✓ ➬ ➮ ✏ ◆ ❦ ✕ ✕ ❣ ❐ , deciding ♣ ➽ ❩ ◆ is possible in a207 ✉ a208 a209 ✓ a223 , i.e., polynomial time with one round of parallel a214 ✉ a208 oracle calls. Since a207 ✉ a208 a209 ✓ a223 ❩ a207 ✉ a208 a209 ✓ a113 a210 ✏ a211 a212 a213 ➬ ✕ a115 , this proves the membership part for ➬ ➮ ✏ ◆ ✕ ❣ ❐ .

PSPACE-hardness of ♣ ➽ ❩ ◆ for general ◆ follows directly from the PSPACE-hardness of model checking for NAT theories shown below in Theorem 4, and from the fact that NATs can be polynomial-time embedded into a0 ✁ ✄ ✆ ✞ (Corollary 2). Similarly, from the respective results on NATs we obtain that for circumscriptive atoms ◆ with ➬ ➮ ✏ ◆ ✕ ❣ ❐ the problem is a217 ✉ a208 -hard (and thus a217 ✉ a208 -complete).

The a207 ✉ a208 a209 ✓ a113 a210 ✏ a211 a212 a213 ➬ ✕ a115 -hardness part for the case where ◆ is a Boolean combination of formulas ◆ ✓ ❴ ❵ ❵ ❵ ❴ ◆ a218 ❖ a0 ✁ ✄ ✆ ✞ such that a219 a220 a221 a218 ❦ ❧ ✓ ➬ ➮ ✏ ◆ ❦ ✕ ❣ ❐ is then shown by a reduction from deciding, given a227 instances ✏ ♣ ✓ ❴ ◆ ✓ ✕ ,. . . , ✏ ♣ ❛ ❴ ◆ a218 ✕ of the model checking problem for circumscriptive atoms, whether the number of yes-instances among them is even. The a207 ✉ a208 a209 ✓ a113 a210 ✏ a211 a212 a213 ➬ ✕ a115 -completeness of this problem is an instance of Wagner's [1990] general result for all a217 ✉ a208 -complete problems. Moreover, we may use that all instances are on disjoint alphabets and the assertion [Wagner, 1990] that ✏ ♣ ❦ ❴ ◆ ❦ ✕ is a yes-instance only if ✏ ♣ ❦ a209 ✓ ❴ ◆ ❦ a209 ✓ ✕ is a yes-instance, for all ☞ ❖ ❭ a229 ❴ ❵ ❵ ❵ ❴ a227 a230 a229 ❝ . Then, we can define

where a231 is a fresh letter. The interpretation ♣ ❩ a239 a218 ❦ ❧ ✓ ♣ ❦ ⑨ ❭ a231 ❝ is a model of ◆ if and only if the number of yes-instances among ✏ ♣ ✓ ❴ ◆ ✓ ✕ ,. . . , ✏ ♣ ❛ ❴ ◆ a218 ✕ is even. Clearly, ◆ and ♣ can be constructed in polynomial time. a240

Theorem 2 Deciding, given formulas ◆ ❴ ➒ ❖ a0 ✁ ✄ ✆ ✞ whether ◆ ➽ ❩ ➒ is PSPACE-complete. Hardness holds even if ➒ ❖ a0 . If the nesting depth of ◆ and ➒ is bounded by the constant ❐ a241 ❰ , then the problem is a217 ✉ a208 a209 ✓ -complete.

Proof: The problem is in PSPACE (resp., a217 ✉ a208 a209 ✓ ): An interpretation ♣ such that ♣ ➽ ❩ ◆ ❹ ➓ ➒ can be guessed and verified in polynomial space (resp., a207 ✉ a208 a209 ✓ a113 a210 ✏ a211 a212 a213 ➬ ✕ a115 , thus in polynomial time with an oracle for a217 ✉ a208 ). Hence the problem is in NPSPACE = PSPACE (resp., a217 ✉ a208 a209 ✓ ). Hardness follows from the polynomial time embedding of NATs into a0 ✁ ✄ ✆ ✞ (Corollary 2) and Theorem 3. a240

Corollary 1 Deciding satisfiability of a given formula ◆ ❖ a0 ✁ ✄ ✆ ✞ is PSPACE-complete. If the nesting depth is bounded by a constant ❐ a241 ❰ , then the problem is a214 ✉ a208 a209 ✓ -complete.

4 Nested Abnormality Theories (NATs)

Lifschitz [1995] proposed the hierarchical use of the circumscription principle, applied to building blocks of a more complex theory. This method was used, e.g., in [Baral et al., 1998] for defining the formal semantics of narratives.

We assume that the atoms ❍ ■ include a set of distinguished atoms ❍ ➳ ❩ ❭ ➐ ➳ ✓ ❴ ❵ ❵ ❵ ❴ ➐ ➳ a208 ❝ (which intuitively represent abnormality properties). Blocks are defined as the smallest set such that if ✍ ✓ ❴ ❵ ❵ ❵ ❴ ✍ a218 are distinct atoms not in ❍ ➳ , and each of a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ is either a formula in a0 or a block, then

is a block [Lifschitz, 1995], where ✍ ✓ ❴ ❵ ❵ ❵ ❴ ✍ a218 are called described by this block. The nesting depth of a242 , denoted ➬ ➮ ✏ a242 ✕ , is 0 if every a242 ❦ is from a0 , and a229 a244 a219 a220 a221 ❭ ➬ ➮ ✏ a242 ❦ ✕ ➽ a229 ❣ ☞ ❣ ➬ ❝ otherwise.

A nested abnormality theory (NAT) [Lifschitz, 1995] is a collection a245 ❩ a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ of blocks; its nesting depth, ➬ ➮ ✏ a245 ✕ , is defined as a219 a220 a221 ❭ ➬ ➮ ✏ a242 ❦ ✕ ➽ a229 ❣ ☞ ❣ ➬ ❝ .

The semantics of a NAT a245 is defined by a mapping a247 ✏ a245 ✕ to a QBF as follows: a247 ✏ a245 ✕ ❩ ❥ a248 a249 a250 a247 ✏ a242 ✕ , where for any block a242 ❩ ❭ ☛ a243 a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ ❝ ,

given that a247 ✏ a242 ❦ ✕ ❩ a242 ❦ if a242 ❦ is a formula in a0 .

Thus, a standard circumscription ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ , where ◆ ❖ a0 , is equivalent to a NAT a245 ❩ ❭ ❳ a243 ◆ ❝ where ❱ is viewed as the set of abnormality letters ❍ ➳ ; notice that ➬ ➮ ✏ a245 ✕ ❩ ❰ .

We note the following useful proposition.

Proposition 2 Let a245 ❩ a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ be any NAT. Let a245 ❞ ❩ ❭ ❳ a243 a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ ❝ where ❳ is any subset of the atoms (disjoint with ❍ ➳ ). Then, a245 and a245 ❞ have the same models.

Indeed, a245 ❞ has void minimization of ❍ ➳ (making each ➐ ➳ a236 in ❍ ➳ false), and fixed and floating letters can have any values.

Embedding NATs into a0 ✁ ✄ ✆ ✞

In the translation a247 ✏ a245 ✕ , theminimized letters ❍ ➳ are under an existential quantifier, and thus "projected" from the models of the formula ❇ ❈ ❊ ● ✏ a254 a254 a254 ✕ . We can, modulo auxiliary letters, eliminate existential quantifiers as follows:

1. Rename every quantifier a251 ❍ ➳ in a247 ✏ a245 ✕ such that every quantified variable is different from any other variable.
2. In every circumscriptive subformula ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ of the renamed formula, add to the floating atoms all variables which are quantified in ◆ (including subformulas).

3. Drop all quantifiers.

Let a247 a255 ✏ a245 ✕ be the resulting formula. Note that its size is polynomial (quadratic) in the size of a247 ✏ a245 ✕ .

Example 2 Let ❍ a242 ❩ ❭ ➐ ➳ ✓ ❴ ➐ ➳ ✗ ❝ and a245 ❩ ❭ ✁ a243 a245 ✓ ❴ ➐ ➳ ✓ ➘ ✁ ❝ , where a245 ✓ ❩ ❭ ✁ a243 ➐ ➳ ✓ ➘ ➓ ➐ ➳ ✗ ❴ ➐ ➳ ✓ ➘ ✁ ❝ . Then,

In Step 1, we rename ➐ ➳ ✓ and ➐ ➳ ✗ in a247 ✏ a245 ✓ ✕ to ➐ ➳ ✂ and ➐ ➳ ☎ , respectively ✝ , and add in Step 2 ➐ ➳ ✂ ❴ ➐ ➳ ☎ to the floating letter ✁ of a245 . After dropping quantifiers in Step 3, we obtain:

Let ❍ ✟ ✏ a245 ✕ be the set of atoms from Step 3 of the embedding a247 a255 ✏ a245 ✕ . The following result, which can be proven by induction on the nesting depth of a245 , states the correctness of a247 a255 .

Proposition 3 For any NAT a245 , the formulas a247 ✏ a245 ✕ and a247 a255 ✏ a245 ✕ are equivalent modulo ❍ ✟ ✏ a245 ✕ .

Corollary 2 Modulo auxiliary letters, NAT is (semantically) a fragment of a0 ✁ ✄ ✆ ✞ , and polynomial-time embedded via a247 a255 .

Notice that is not possible to add in Step 2 of the embedding a247 a255 ✏ a245 ✕ the quantified variables in ◆ to the fixed atoms.

Example 3 Reconsider the NAT a245 in Ex. 2. Note that ✠ is the unique model of a247 ✏ a245 ✕ . The formula a247 a255 ✏ a245 ✓ ✕ has, if we disregard ➐ ➳ ✓ ❴ ➐ ➳ ✗ (which are fixed in it), the models ♣ ✓ ❩ ❭ ➐ ➳ ✂ ❴ ✁ ❝ and ♣ ✗ ❩ ❭ ➐ ➳ ☎ ❝ . They give rise to the two models ✡ ✓ ❩ ❭ ➐ ➳ ✓ ❴ ✁ ❴ ➐ ➳ ✂ ❝ and ✡ ✗ ❩ ❭ ➐ ➳ ☎ ❝ of a247 a255 ✏ a245 ✓ ✕ ❹ ✏ ➐ ➳ ✓ ➘ ✁ ✕ , of which ✡ ✗ is ➐ ➳ ✓ ❴ ➐ ➳ ✗ ❿ ➐ ➳ ✂ ❴ ➐ ➳ ☎ ❴ ✁ -minimal.

However, if ➐ ➳ ✂ , ➐ ➳ ☎ were fixed in a247 a255 ✏ a245 ✕ , then both ✡ ✓ and ✡ ✗ would be models of a247 a255 ✏ a245 ✕ , as they are ➐ ➳ ✓ ❴ ➐ ➳ ✗ ❿ ✁ - minimal. Therefore, Proposition 3 would fail.

Eliminating fixed letters

Every fixed letter ➪ can be removed from a NAT a245 similarly as from a formula ◆ ❖ a0 ✁ ✄ ✆ ✞ . However, we must take into account that a fixed letter ➪ may not be simply declared as a minimized letter in the rewriting, since there is a special set ❍ ➳ of minimized letter which has restricted uses. We surpass this by introducing two special abnormality letters ➐ ➳ ☛ and ➐ ➳ ☛ in ❍ ➳ , and by adding the formula ✏ ➪ ➘ ➐ ➳ ☛ ✕ ❹ ✏ ➐ ➳ ☛ ➘ ➓ ➐ ➳ ☛ ✕ as a new block to a245 , a well as ➐ ➳ ☛ ➘ ➓ ➐ ➳ ☛ in every other block of a245 . The letter ➪ is declared floating in a245 .

4.1 Complexity of NATs

Ordinary circumscription can express a QBF sentence ✌ ❩ ➄ ❨ a251 ✍ ➒ (where ➒ ❖ a0 ) as follows. Let ✏ be a fresh variable.

Lemma 1 (cf. [Eiter and Gottlob, 1993]) ✌ is true if and only if ❇ ❈ ❊ ● ✏ ◆ ❿ ✏ ❿ ✍ ✕ ➽ ❩ ➓ ✏ , where ◆ ❩ ➒ ✚ ✏ .

This circumscription can be easily stated as a NAT. Set

Then Lemma 1 implies that a245 ✓ ➽ ❩ ➓ ✏ iff ✌ is true. In fact, denote for any interpretation ♣ and set of atoms ✖ by ■ ✗ ✏ ✖ ✕ the assignment to ✖ as given by ♣ . Then, every model ♣ of a245 ✓ must be, if we fix the atoms in ❨ to ■ ✗ ✏ ❨ ✕ , a model of ◆ such that ♣ ➽ ❩ ✏ if and only if ➒ a113 ❨ ➶ ■ ✗ ✏ ❨ ✕ a115 is unsatisfiable.

Starting from this result, we prove PSPACE-hardness of inference a245 ➽ ❩ ◆ from a NAT theory a245 . The basic technique is to introduce further variables as parameters ✚ into the formula ✌ from Lemma 1, which are kept fixed at the inner levels. At a new outermost level to be added, the letter ✏ is used for evaluating the formula at a certain level. We must in alternation minimize and maximize the value of ✏ .

Consider the case of a QBF ✌ ❩ ➄ ❨ a251 ✍ ➒ a113 ✚ a115 , where ✚ are free variables in it, considered as "parameters". We nest a245 ✓ into the following theory a245 ✗ :

This amounts to the following circumscription:

The outer circumscription minimizes ➐ ➳ and thus maximizes ✏ . a247 ✏ a245 ✗ ✕ is, by Proposition 3, equivalent to the formula

modulo the atoms ➐ ✓ and ➐ ✗ . The following can be shown:

Lemma 2 a245 ✗ ➽ ❩ ✏ if and only if for every assignment ✤ ✏ ✚ ✕ , the QBF a251 ❨ ➄ ✍ ➓ ➒ a113 ✚ ➶ ✤ ✏ ✚ ✕ a115 is true (i.e., ✌ a113 ✚ ➶ ✤ ✏ ✚ ✕ a115 is false).

It follows from the lemma that deciding, given a NAT a245 ✗ of nesting depth 1 and ➒ ❖ a0 , whether a245 ✗ ➽ ❩ ➒ is a217 ✉ ✂ -hard.

We generalize this pattern to encode the evaluation of a QBF

where the quantifiers ❲ ❦ alternate, into inference a245 ➽ ❩ ➒ from a NAT theory a245 as follows.

Let ◆ ❩ ➒ ✚ ✏ , where ✏ is a fresh atom. Define inductively

for all ✩ ❐ ❴ ✩ ❐ a244 a229 ❖ ❭ ✩ ❴ ❵ ❵ ❵ ❴ ➬ ❝ , and let a245 a233 ❩ ❭ a243 ◆ ❝ . Note that a245 a233 is equivalent to ◆ , and that ➬ ➮ ✏ a245 ❦ ✕ ❩ ☞ a230 a229 , for all ☞ ❖ ❭ a229 ❴ ❵ ❵ ❵ ❴ ➬ ❝ while ➬ ➮ ✏ a245 a233 ✕ ❩ ❰ . We obtain the following.

Lemma 3 For every ➬ a241 a229 , a245 ❛ ✦ ✓ has some model, and

• ✦ if ➬ is odd, then a245 ❛ ✦ ✓ ➽ ❩ ✏ iff ✌ is false, i.e., ➓ ✌ is true;
• ✦ if ➬ is even, then a245 ❛ ✦ ✓ ➽ ❩ ➓ ✏ iff ✌ is true.

This statement can be proved by induction on ➬ a241 a229 .

Lemma 4 Model checking for NATs, i.e., deciding whether a given interpretation ♣ is a model of a given NAT a245 , is in PSPACE. If ➬ ➮ ✏ a245 ✕ ❣ ❐ for constant ❐ a241 ❰ , then it is in a217 ✉ a208 a209 ✓ .

Proof: For ❐ ❩ ❰ , the problem amounts to model checking for ordinary circumscription, which is in ✭ a212 ✮ ✰ . For ❐ ❮ ❰ , we can test recursively for each block a242 of a245 whether ♣ is a model of each block a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ in a242 ❩ ❭ ☛ a243 a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ ❝ , and that nomodel ✡ of a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ exists such that ✡ ❷ ✲ ✴ ✈ ✶ ♣ . The recursion depth is linear, and the procedure runs in quadratic space. Moreover, if ➬ ➮ ✏ a245 ✕ is bounded by a constant ❐ , then the check for ♣ and the existence of ✡ witnessing that ♣ is not model of a242 , can be done in nondeterministic polynomial time with an oracle for a217 ✉ a208 . Thus, the problem is in PSPACE (resp., in a217 ✉ a208 a209 ✓ ). a240

The construction in Lemma 2 shows how it is possible to polynomially embed QBF evaluation into inference wrt a NAT. In turn, Proposition 3 shows that a NAT can be polynomially embedded into an a0 ✁ ✄ ✆ ✞ formula. The following theorem highlights the consequences of such relations on complexity of inference wrt a NAT.

Theorem 3 Deciding, given a NAT theory a245 and a propositional ✷ formula ◆ , whether a245 ➽ ❩ ◆ is PSPACE-complete. If ➬ ➮ ✏ a245 ✕ ❣ ❐ for constant ❐ a241 ❰ , then it is a217 ✉ a208 a209 ✗ -complete.

Proof: The hardness part follows from Lemma 3 above. As for the membership part, a model ♣ of a245 such that ♣ ❼ ➽ ❩ ◆ can be guessed and verified in PSPACE (resp., with the help of a a217 ✉ a208 a209 ✓ -oracle). Thus the problem is in co-NPSPACE = PSPACE (resp., a217 ✉ a208 a209 ✗ ). a240

The next theorem shows that the upper bounds on model checking for NATs have matching lower bounds. (This is expected from Theorem 3: if model checking were in the Polynomial Hierarchy (PH), then also inference would be in PH.)

Theorem 4 Given a NAT theory a245 and an interpretation ♣ , deciding whether ♣ ➽ ❩ a245 is PSPACE-complete. If ➬ ➮ ✏ a245 ✕ ❣ ❐ for a constant ❐ a241 ❰ , then the problem is a217 ✉ a208 a209 ✓ -complete.

Proof: (Sketch) By Lemma 4, it remains to show the hardness parts. Note that for ❐ ❩ ❰ , this is immediate from results in [Eiter and Gottlob, 1993]. We can slightly adapt the above encoding of QBFs into NATs. Given a QBF ✌ as in Eq. (2), let the NATs a245 a233 , . . . , a245 ❛ be as there, with the only difference that ◆ ❩ ➒ ✚ ✏ is replaced by

where ✺ ❛ ❩ ❭ ✏ ❝ if ➬ is odd and ✺ ❛ ❩ ❭ ➓ ✏ ❝ otherwise. Here ✹ is a new letter, defined (i.e., floating) in a245 ❛ and fixed elsewhere; ❨ ❛ resp. ❨ ✓ ⑨ a254 a254 a254 ⑨ ❨ ❛ ✦ ✓ ⑨ ✺ ❛ is viewed as conjunction of its formulas. Let a245 ❞ a233 ❴ ❵ ❵ ❵ ❴ a245 ❞ ❛ be the resulting NATs.

Define ♣ ❩ a239 ❛ ❦ ❧ ✓ ❨ ❦ ⑨ ❭ ✹ ❴ ✏ ❝ if ➬ is odd and ♣ ❩ a239 ❛ ❦ ❧ ✓ ❨ ❦ ⑨ ❭ ✹ ❝ if ➬ is even. Note that ♣ ➽ ❩ ◆ ❞ and ♣ is, modulo ✏ , the only candidate for a model of a245 ❞ ❛ in which ❨ ❛ and ✹ are true: any such model must satisfy ◆ ❞ , and if ❨ ❛ ❹ ✹ are true, then all other atoms have a unique truth value.

It holds that ♣ is a model of a245 ❞ ❛ iff the QBF ✌ is false (resp., true). It follows that model checking is PSPACEhard and a217 ✉ a208 a209 ✓ -hard if ➬ ➮ ✏ a245 ✕ ❣ ❐ for constant ❐ ; note that ➬ ➮ ✏ a245 ❞ ❛ ✕ ❩ ➬ a230 a229 . a240

4.2 A polynomial-time fragment

We call a block ❭ ☛ a243 a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ ❝ Horn, if each a242 ❦ is a Horn CNF if a242 ❦ ❖ a0 , and recursively a242 ❦ is Horn otherwise. ANAT a245 is Horn, if each of its blocks is Horn.

In [Cadoli and Lenzerini, 1994], it was shown that deciding ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ✠ ✕ ➽ ❩ ➓ ✏ , where ◆ is a propositional Horn CNF and ✏ is an atom, is ✭ a212 ✮ ✰ -complete. That is, already for Horn NATs a245 without nesting (i.e., ➬ ➮ ✏ a245 ✕ ❩ ❰ ) inference is intractable, and nesting may further add on complexity.

Horn NATs without fixed letters

The technique of removing fixed letters from a Horn NAT does not work, since it uses non-Horn clauses. Thus, Horn NATs without fixed letters do not immediately inherit complexity, in particular intractability, from general Horn NATs.

In fact, for this class we obtain positive results. Note that here still minimization of atoms ➪ is possible via auxiliary atoms ➐ ➳ ☛ ❖ ❍ ➳ and Horn axioms ➪ ♥ ➐ ➳ ☛ , ➐ ➳ ☛ ♥ ➪ in a245 .

Call any ❱ ❿ ❳ -minimal model of a NAT a245 such that ❱ ❩ ❍ ■ ⑧ ❍ ➳ and ❳ ❩ ✠ a minimal model of a245 .

Theorem 5 Let a245 be aHornNAT without fixed letters. Then, (1) a245 has a least (i.e., a unique minimal) model, and (2) a245 is equivalent to a Horn CNF ◆ ✏ a245 ✕ . Furthermore, both ◆ ✏ a245 ✕ and ♣ ✏ a245 ✕ are computable in polynomial time.

Proof: (Sketch) Let, for any Horn CNF ➒ and model ♣ ① ❍ ■ , be ➒ ✗ the Horn CNF resulting from ➒ after substituting each ➐ ➳ a236 ❖ ❍ ➳ by ❀ (true) if ♣ ➽ ❩ ➐ ➳ a236 and by ❁ (false) if ♣ ➽ ❩ ➓ ➐ ➳ a236 and subsequent standard simplifications.

Let a245 be a single block a242 ❩ ❭ ❳ a243 a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ ❝ , where ❳ ❩ ❍ ■ ⑧ ❍ ➳ . Define the Horn CNF ◆ ✏ a242 ✕ recursively by

where ♣ a233 ❩ ♣ a233 ✏ a242 ✕ is the least model of the Horn CNF

and

Then, by induction on ➬ ➮ ✏ a242 ✕ a241 ❰ , we can show that (1) ♣ ✏ a242 ✕ is the least model of a242 , and (2) ◆ ✏ a242 ✕ is equivalent to a242 .

Let, for any formula ➴ , block a242 , NAT a245 etc denote a223 ➴ a223 , a223 a242 a223 , a223 a245 a223 etc the representation size of the respective object. Obviously, we can compute ◆ ✏ a242 ✕ inductively. For the Horn CNFs ➒ ✏ a242 ✕ and ◆ ✏ a242 ✕ , we have a223 ➒ ✏ a242 ✕ a223 ❣ a223 a242 a223 and a223 ◆ ✏ a242 ✕ a223 ❣ a223 a242 a223 . Of the model ♣ a233 , we only need its restriction ♣ a233 a113 ❍ a115 to the atoms ❍ occurring in a242 (all other atoms are irrelevant for computing ◆ ✏ a242 ✕ ). We can compute ♣ a233 a113 ❍ a115 from ➒ ✏ a242 ✕ in a210 ✏ a223 a242 a223 ✕ time (recall that the least model of a Horn CNF ➴ is computable in a210 ✏ a223 ➴ a223 ✕ time), and ❥ a248 ❂ a249 ❄ a242 ✗ ❆ ❦ from ♣ a233 a113 ❍ a115 in a210 ✏ a223 a242 a223 ✕ time. Overall, it follows that for a245 ❩ a242 , we can compute both ◆ ✏ a245 ✕ and its least model ♣ ✏ a245 ✕ in time a210 ✏ ❉ ➳ ✏ a245 ✕ a223 a245 a223 ✕ , where ❉ ➳ ✏ a245 ✕ is the number of (recursive) blocks in a245 , thus in polynomial time.

By Prop. 2, we can replace a multiple block a245 ❩ a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ by a245 ❞ ❩ ❭ ❍ ■ ⑧ ❍ ➳ a243 a242 ✓ ❴ ❵ ❵ ❵ ❴ a242 ❛ ❝ , which is Horn and without fixed letters, and obtain analogous results. a240

Using sophisticated data structures, the (relevant parts of) models ♣ a233 ✏ a242 ✕ above can be computed incrementally, where each clause in ◆ ✏ a242 ✕ is fired at most once. Overall, ◆ ✏ a245 ✕ and ♣ ✏ a245 ✕ are computable in a210 ✏ a223 a245 a223 ✕ time. We thus have:

Theorem 6 (Flat Normal Form) Every Horn NAT a245 without fixed letters can be rewritten to an equivalent Horn NAT ❭ ❳ a243 ◆ ❝ without fixed letters, where ◆ ❖ a0 is a Horn CNF, in a210 ✏ a223 a245 a223 ✕ time (i.e., in linear time).

Thus, nesting in Horn NATs without fixed letters does not increase the expressiveness, and can be efficiently eliminated. We note some easy corollaries of the previous result.

Corollary 3 Deciding satisfiability of a given Horn NAT a245 without fixed letters is polynomial.

Corollary 4 Model checking for a given Horn NAT a245 without fixed letters and model ♣ is polynomial.

For the inference problem, we obtain the following result.

Theorem 7 Given a Horn NAT a245 without fixed letters and ◆ ❖ a0 , deciding a245 ➽ ❩ ◆ is ✭ a212 ✮ ✰ -complete. If ◆ is a CNF, then the problem is polynomial.

Proof: Since model checking is polynomial, the problem is clearly ❋ in ✭ a212 ✮ ✰ . The ✭ a212 ✮ ✰ -hardness part follows from ✭ a212 ✮ ✰ -completeness of validity checking for a given ◆ ❖ a0 (ask whether ❭ ❳ a243 ❀ ❝ ➽ ❩ ◆ , where ❳ contains all letters).

We can reduce a245 ➽ ❩ ➒ to ◆ ✏ a245 ✕ ➽ ❩ ➒ in a210 ✏ a223 a245 a223 ✕ time, where ◆ ✏ a245 ✕ is a Horn CNF. If ➒ ❩ ❥ a218 ❦ ❧ ✓ ➴ ❦ is a CNF of clauses ➴ ❦ , the latter can be checked in a210 ✏ a227 a223 ◆ ✏ a245 ✕ a223 a244 a223 ➒ a223 ✕ time, thus in a210 ✏ a227 a223 a245 a223 a244 a223 ➒ a223 ✕ time (check ◆ ✏ a245 ✕ ➽ ❩ ➴ ❦ , which is a210 ✏ a223 ◆ ✏ a245 ✕ a223 a244 a223 ➴ ❦ a223 ✕ time, for all ☞ ❖ ❭ a229 ❴ ❵ ❵ ❵ ❵ a227 ❝ ). a240

5 Other Generalizations of Circumscription

As we have discussed above, fixed letters can be removed from a0 ✁ ✄ ✆ ✞ and NAT theories, respectively. Using these techniques, the hardness results of Sections 3.1 and 4.1 can be sharpened to theories without fixed letters.

Prioritized circumscription generalizes circumscription ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ by partitioning the letters ❱ into priority levels ❱ ✓ ❮ ❱ ✗ ❮ a254 a254 a254 ❮ ❱ ❛ , and informally pruning all models of ◆ which are not minimal on ❱ ❦ , while ❳ ⑨ ❱ ❦ a209 ✓ ⑨ a254 a254 a254 ⑨ ❱ ❛ floats and ❱ ✓ ⑨ a254 a254 a254 ⑨ ❱ ❦ ✦ ✓ is fixed, for ☞ ❩ a229 ❴ ❵ ❵ ❵ ❴ ➬ (cf. [Lifschitz, 1994]). This can be readily expressed as the nested circumscription ❇ ❈ ❊ ● ✏ a254 a254 a254 ❇ ❈ ❊ ● ✏ ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ✓ ❿ ❳ ⑨ ❱ ✗ ⑨ a254 a254 a254 ⑨ ❱ ❛ ✕ ❿ ❱ ✗ ❿ ❳ ⑨ ❱ ✂ ⑨ a254 a254 a254 ⑨ ❱ ❛ ✕ a254 a254 a254 ✕ . This generalization differs from a0 ✁ ✄ ✆ ✞ and NATs: The complexity does not increase, as inference and model checking remain a217 ✉ ✗ -complete and ✭ a212 ✮ ✰ -complete, respectively. Intuitively, the reason is that prioritization allows only for a restricted change of the role of the same letter in iterations (floating to minimized and minimized to fixed) and forbids reconsidering minimized letters.

Curbing is yet another extension of circumscription [Eiter et al., 1993; Eiter and Gottlob, 2000]. Rather than the (hierarchical) use of circumscription applied to blocks, curbing aims at softening minimization, and allows for inclusive interpretation of disjunction where ordinary circumscription returns exclusive disjunction. Semantically, ❇ ● ❊ ■ ✏ ◆ ❿ ❱ ❿ ❳ ✕ for a formula ◆ ❖ a0 is the smallest set ❏ ① ◗ ❘ ❚ ✏ ◆ ✕ which contains all models of ❇ ❈ ❊ ● ✏ ◆ ❿ ❱ ❿ ❳ ✕ and is closed under minimal upper bounds in ◗ ❘ ❚ ✏ ◆ ✕ . A minimal upper bound (mub) of a set ❏ ❞ of models in ◗ ❘ ❚ ✏ ◆ ✕ is a model ♣ ❖ ◗ ❘ ❚ ✏ ◆ ✕ such that (1) ♣ ❞ ❣ ✉ ✈ ✇ ♣ , for every ♣ ❞ ❖ ❏ ❞ , and (2) there exists no ✡ ❖ ◗ ❘ ❚ ✏ ◆ ✕ satisfying item1 such that ✡ ❷ ✉ ✈ ✇ ♣ ❞ .

For example, ◆ ❩ ➐ ✚ ➳ has two minimal models, if all letters are minimized (❱ ❩ ❍ ■ ❩ ❭ ➐ ❴ ➳ ❝ ): ❭ ➐ ❝ and ❭ ➳ ❝ . The model ❭ ➐ ❴ ➳ ❝ is not a minimal model of ◆ , but is a curbmodel of ◆ . Thus, ❇ ● ❊ ■ ✏ ➐ ✚ ➳ ✕ ▲ ➐ ✚ ➳ . On the other hand, if ❍ ■ ❩ ❭ ➐ ❴ ➳ ❴ ✍ ❝ , then ❇ ● ❊ ■ ✏ ➐ ✚ ➳ ✕ ▲ ✏ ➐ ✚ ➳ ✕ ❹ ➓ ✍ is different from ➐ ✚ ➳ ; the unsupported letter ✍ is set to false. Note that ❇ ❈ ❊ ● ✏ ➐ ✚ ➳ ✕ ▲ ✏ ➐ ➘ ➓ ➳ ✕ ❹ ✍ is different from ❇ ● ❊ ■ ✏ ➐ ✚ ➳ ✕ .

Like for a0 ✁ ✄ ✆ ✞ and NATs, inference and model checking for ❇ ● ❊ ■ ✏ ◆ ❿ ❱ ❿ ❳ ✕ are PSPACE-complete [Eiter and Gottlob, 2000]. However, in the first-order case, the formalisms have different expressiveness. Let us consider theories in a function-free language under domain closure (DC) and the unique names assumption (UNA), i.e., the (finite) "datalog" case. In this case, curbing can express some problems which a0 ✁ ✄ ✆ ✞ and NATs can not. We can, e.g., write a (fixed) interpreter ✠ ❖ in this language for curbing varying propositional 3CNF formulas ◆ , input as ground facts a80 ✏ ◆ ✕ , such that the curb models of ✠ ❖ ⑨ a80 ✏ ◆ ✕ and ◆ are in 1-1 correspondence. Notice that curbing such 3CNFs ◆ is PSPACE-complete, and thus, by well-known results in complexity, this is not expressible by a fixed a0 ✁ ✄ ✆ ✞ or NAT theory (unless PH=PSPACE).

Further relationships between a0 ✁ ✄ ✆ ✞ resp. NATs and curbing, as well as other expressive KR formalisms [Baral et al., 2000; Pollett and Remmel, 1997], remain to be explored.

Acknowledgments

This work was supported by the Austrian Science Fund (FWF) Project N. Z29-INF.