In: Proc. Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001.

Complexity of Nested Circumscription and Abnormality Theories

Marco Cadoli

Dipartimento di Informatica e Sistemistica Università di Roma “La Sapienza” Via Salaria 113, I-00198 Roma, Italy

cadoli@dis.uniroma1.it

Thomas Eiter Georg Gottlob Institut für Informationssysteme Technische Universität Wien

Favoritenstrasse 9, A-1040 Wien, Austria

       eiter@kr.tuwien.ac.at
    gottlob@dbai.tuwien.ac.at

Abstract

We propose L_{Circ}, an extension of circumscription by allowing propositional combinations and nesting of circumscriptive theories. As shown, Lifschitz’s nested abnormality theories (NATs, introduced in AIJ, 1995) are naturally embedded into this language. We analyze the complexity of L_{Circ} and NATs, and in particular the effect of nesting. The latter is found a source of complexity, as both formalisms are proved to be PSPACE-complete. We identify cases of lower complexity, including a tractable case. Our results give insight into the “cost” of using L_{Circ} resp. NATs as a host language for expressing other formalisms, such as narratives.

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 T, either propositional or first-order, and it is used to eliminate some unintended models of T.

Since the seminal definition of circumscription in [Mc-Carthy, 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 L_{Circ}, 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 Circ(T_{1}) and Circ(T_{2}) coming from two equally trustable agents who perform circumscription are to be integrated, it seems plausible to take their disjunction, i.e., Circ(T_{1}) ∨ Circ(T_{2})^{1}. In L_{Circ}, 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 Circ(T_{1}) may model the intended behavior of a subpart, e.g., the engine. Analogously, Circ(T_{2}) 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 Circ(T_{1}), Circ(T_{2}), and a plain propositional formula encoding observations.

In this paper, we are mainly concerned with the computational properties of L_{Circ} and NATs and with their relationship to plain circumscription. In particular, we tackle the following questions:

• Can NATs be embedded into L_{Circ}?

• What is the precise complexity of reasoning under nested circumscription? By reasoning, we mean both model checking and formula inference from an L_{Circ} or NAT theory.

• Is there a simple restriction of NATs (and thus of L_{Circ}) 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 L_{Circ}, 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 L_{Circ}.

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 L_{Circ} 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].

1We remind that Circ(T_{1}) ∨ Circ(T_{2}) ≢ Circ(T_{1} ∨ T_{2}) in general (take, e.g., T_{1} = a ∧ b, T_{2} = b).

Our results prove that the expressive power that makes L_{Circ} and NATs useful tools for the modularization 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 Circ 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 At of propositional atoms, and let L(At) (for short, L, if At does not matter or is clear from the context) be a standard propositional language over At. For any formula φ ∈ L, we denote by mod(φ) the set of its models. Capitals P, Q, Z etc stand for ordered sets of atoms, which we also view as lists. If X = {x_{1}, …, x_{n}} and X′ = {x′_{1}, …, x′_{n}}, then X ≤ X′ denotes the formula ⋀_{i=1}^{n}(x_{i} → x′_{i}).

The extension of a model M on atoms A is denoted by M[A]. We denote by ≤_{P;Z} the preference relation on models which minimizes P in parallel while Z is varying and all other atoms are fixed; i.e., M ≤_{P;Z} M′ (M is more or equally preferable to M′) iff M[P] ⊆ M′[P] and M[Q] = M′[Q], where Q = At \ P ∪ Z and ⊆ and = are taken componentwise. As usual, M <_{P;Z} M′ means M ≤_{P;Z} M′ ∧ M ≠ M′.

We denote by Circ(φ; P; Z) the second-order circumscription [Lifschitz, 1985] of the formula φ where the atoms in P are minimized, the atoms in Z float, and all other atoms are fixed, which is defined as the following formula:

Circ(φ; P; Z) =

φ[P; Z] ∧ ∀P′Z′((φ[P′; Z′] ∧ P′ ≤P) → P ≤P′). (1)

Here P′ and Z′ are lists of fresh atoms (not occurring in φ) corresponding to P and Z, 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 M of φ which are P; Z-minimal, where a model M of φ is P; Z-minimal, if no model M′ of φ exists such that M′ <_{P;Z} M.

3 Language L_{Circ}

The language L_{Circ} extends the standard propositional language L (over a set of atoms At) by circumscriptive atoms. Formulas of L_{Circ} are inductively built as follows:

1. a ∈ L_{Circ}, for every a ∈ At;

2. if φ, ψ are in L_{Circ}, then φ ∧ ψ and ¬φ are in L_{Circ};

3. if φ ∈ L_{Circ} and P, Z are disjoint lists of atoms, then Circ(φ; P; Z) is in L_{Circ} (called circumscriptive atom). Further Boolean connectives (∨, →, etc) are defined as usual. The semantics of any formula φ from L_{Circ} is given in terms of models of a naturally associated QBF τ(φ), which is inductively defined as follows:

1. τ(a) = a, if φ is an atom a ∈ At;

2. τ(φ ∧ ψ) = τ(φ) ∧ τ(ψ) and τ(¬φ) = ¬τ(φ);

3. τ(Circ(φ; P; Z)) =

τ(φ[P; Z]) ∧ ∀P′Z′((τ(φ[P′; Z′]) ∧ P′ ≤P) → P ≤P′).

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 (φ ∈ L), then τ(Circ(φ; P; Z)) coincides with the formula in (1).

Example 1 Consider the formula

φ = Circ(Circ(a ∨ b; a; b) ∨ Circ(b ∨ c; b; c); a; c). Applying rule 3 to inner circumscriptions we get τ(φ) = Circ((b ∧ ¬a) ∨ (c ∧ ¬b); a; c). Applying rule 3 again we get τ(φ) = (¬a ∧ ¬b ∧ c) ∨ (¬a ∧ b) = ¬a ∧ (b ∨ c).

As usual, we write M ⊧ φ if M 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 L_{Circ} as well. More precisely, let φ = Circ(ψ; P; Z) be a circumscriptive atom. For each letter q ∉ P ∪ Z, introduce a fresh letter q̄, add q,q̄ to P, and add a conjunct q ↔ ¬q̄ to ψ. Let φ′ = Circ(ψ′; P′; Z) be the resulting circumscriptive atom. Then, the following holds.

Proposition 1 φ and φ′ are equivalent modulo the set of all auxiliary letters q̄.

Using this equivalence, we can eliminate all fixed letters from a formula α ∈ L_{Circ}, by replacing each circumscriptive atom φ in α with φ′, where the fresh atoms q̄ are made floating inside φ′ and outside φ. Note that the resulting formula α′ has size polynomial in the size of α.

3.1 Complexity results

Let the Circ-nesting depth (for short, nesting depth) of φ ∈ L_{Circ}, denoted nd(φ), be the maximum number of circumscriptive atoms along any path in the formula tree of φ.

Theorem 1 Model checking for L_{Circ}, i.e., deciding whether a given interpretation M is a model of a given formula φ ∈ L_{Circ}, is PSPACE-complete. If nd(φ) ≤ k for a constant k > 0, then the problem is complete for Δ_{k+1}^{P}[O(log n)], i.e., polynomial time with O(log n) many calls to an oracle for Σ_{k}^{P}, where n is the input size.

Proof: (Sketch) Clearly, any formula φ ∈ L_{Circ} can be encoded, by definition, to a QBF τ(φ) (not necessarily in prenex form) in polynomial time. Thus deciding, M ⊧ φ is in PSPACE. By an inductive argument, we can see that for any circumscriptive atom φ = Circ(ψ; P; Z) such that nd(φ) ≤ k, deciding M ⊧ φ is in Π_{k}^{P}. Thus for any Boolean combination φ of atoms and circumscriptive atoms φ_{1}, …, φ_{m} such that nd(φ) (= max_{i=1}^{m} nd(φ_{i})) ≤ k, deciding M ⊧ φ is possible in Δ_{k+1}^{P}∥, i.e., polynomial time with one round of parallel Σ_{k}^{P} oracle calls. Since Δ_{k+1}^{P}∥ = Δ_{k+1}^{P}[O(log n)], this proves the membership part for nd(φ) ≤ k.

PSPACE-hardness of M ⊧ φ 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 L_{Circ} (Corollary 2). Similarly, from the respective results on NATs we obtain that for circumscriptive atoms φ with nd(φ) ≤ k the problem is Π_{k}^{P} -hard (and thus Π_{k}^{P} -complete).

The Δ_{k+1}^{P}[O(log n)]-hardness part for the case where φ is a Boolean combination of formulas φ_{1}, …, φ_{m} ∈ L_{Circ} such that max_{i=1}^{m} nd(φ_{i}) ≤ k is then shown by a reduction from deciding, given m instances (M_{1}, φ_{1}),…,(M_{n}, φ_{m}) of the model checking problem for circumscriptive atoms, whether the number of yes-instances among them is even. The Δ_{k+1}^{P}[O(log n)]-completeness of this problem is an instance of Wagner’s [1990] general result for all Π_{k}^{P} -complete problems. Moreover, we may use that all instances are on disjoint alphabets and the assertion [Wagner, 1990]that (M_{i}, φ_{i}) is a yes-instance only if (M_{i+1}, φ_{i+1}) is a yes-instance, for all i ∈ {1, …, m−1}. Then, we can define

φ = e ↔ ⋁_{0≤2i≤m} ( ⋀_{j=0}^{2i} φ_{j} ∧ ⋀_{j=2i+1}^{n} ¬φ_{j})

where e is a fresh letter. The interpretation M = ⋃_{i=1}^{m} M_{i} ∪ {e} is a model of φ if and only if the number of yes-instances among (M_{1}, φ_{1}),…, (M_{n}, φ_{m}) is even. Clearly, φ and M can be constructed in polynomial time. □

Theorem 2 Deciding, given formulas φ, ψ ∈ L_{Circ} whether φ ⊧ ψ is PSPACE-complete. Hardness holds even if ψ ∈ L. If the nesting depth of φ and ψ is bounded by the constant k ≥ 0, then the problem is Π_{k+1}^{P}-complete.

Proof: The problem is in PSPACE (resp., Π_{k+1}^{P}): An interpretation M such that M ⊧ φ ∧ ¬ψ can be guessed and verified in polynomial space (resp., Δ_{k+1}^{P}[O(log n)], thus in polynomial time with an oracle for Π_{k}^{P}). Hence the problem is in NPSPACE = PSPACE (resp., Π_{k+1}^{P}). Hardness follows from the polynomial time embedding of NATs into L_{Circ} (Corollary 2) and Theorem 3. □

Corollary 1 Deciding satisfiability of a given formula φ ∈ L_{Circ} is PSPACE-complete. If the nesting depth is bounded by a constant k ≥ 0, then the problem is Σ_{k+1}^{P}-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 At include a set of distinguished atoms Ab = {ab_{1}, …, ab_{k}} (which intuitively represent abnormality properties). Blocks are defined as the smallest set such that if c_{1}, …, c_{m} are distinct atoms not in Ab, and each of B_{1}, …, B_{n} is either a formula in L or a block, then

B = {c_{1}, …, c_{m} : B_{1}, …, B_{n}},

is a block [Lifschitz, 1995], where c_{1}, …, c_{m} are called described by this block. The nesting depth of B, denoted nd(B), is 0 if every B_{i} is from L, and 1 + max{nd(B_{i}) | 1 ≤ i ≤ n} otherwise.

A nested abnormality theory (NAT) [Lifschitz, 1995] is a collection T = B_{1}, …, B_{n} of blocks; its nesting depth, nd(T ), is defined as max{nd(B_{i}) | 1 ≤ i ≤ n}.

The semantics of a NAT T is defined by a mapping σ(T ) to a QBF as follows: σ(T ) = ⋀_{B∈T} σ(B), where for any block B = {C : B_{1}, …, B_{n}},

σ(B) = ∃Ab.Circ(⋀_{i=1}^{n} σ(B_{i}); Ab; C)

given that σ(B_{i}) = B_{i} if B_{i} is a formula in L.

Thus, a standard circumscription Circ(φ; P; Z), where φ ∈ L, is equivalent to a NAT T = {Z : φ} where P is viewed as the set of abnormality letters Ab; notice that nd(T ) = 0.

We note the following useful proposition. Proposition 2 Let T = B_{1}, …, B_{n} be any NAT. Let T′ = {Z : B_{1}, …, B_{n}} where Z is any subset of the atoms (disjoint with Ab). Then, T and T′ have the same models.

Indeed, T′ has void minimization of Ab (making each ab_{j} in Ab false), and fixed and floating letters can have any values.

Embedding NATs into L_{Circ}

In the translation σ(T ), the minimized letters Ab are under an existential quantifier, and thus “projected” from the models of the formula Circ(⋯). We can, modulo auxiliary letters, eliminate existential quantifiers as follows:

1. Rename every quantifier ∃Ab in σ(T ) such that every quantified variable is different from any other variable.

2. In every circumscriptive subformula Circ(φ; P; Z) of the renamed formula, add to the floating atoms all variables which are quantified in φ (including subformulas).

3. Drop all quantifiers.

Let σ^{⋆}(T ) be the resulting formula. Note that its size is polynomial (quadratic) in the size of σ(T ).

Example 2 Let AB ={ab_{1}, ab_{2}} and T ={z : T_{1}, ab_{1} ↔z}, where T_{1} = {z : ab_{1} ↔ ¬ab_{2}, ab_{1} ↔ z}. Then,

σ(T ) = ∃ab_{1}, ab_{2}.Circ(σ(T_{1}) ∧ (ab_{1} ↔z); ab_{1}, ab_{2}; z),

where

σ(T_{1}) = ∃ab_{1}, ab_{2}.Circ({(ab_{1} ↔ ¬ab_{2}) ∧ (ab_{1} ↔ z); \atop ab_{1}, ab_{2}; z).}

In Step 1, we rename ab_{1} and ab_{2} in σ(T_{1}) to ab_{3} and ab_{4}, respectively, and add in Step 2 ab_{3}, ab_{4} to the floating letter z of T . After dropping quantifiers in Step 3, we obtain:

σ^{⋆}(T ) = Circ(σ^{⋆}(T_{1}) ∧ (ab_{1} ↔ z); ab_{1}, ab_{2}; z, ab_{3}, ab_{4}),
σ^{⋆}(T_{1}) = Circ((ab_{3} ↔ ¬ab_{4}) ∧ (ab_{3} ↔ z); ab_{3}, ab_{4}; z).

Let A^{∗}(T ) be the set of atoms from Step 3 of the embedding σ^{⋆}(T ). The following result, which can be proven by induction on the nesting depth of T , states the correctness of σ^{⋆}.

Proposition 3 For any NAT T , the formulas σ(T ) and σ^{⋆}(T ) are equivalent modulo A^{∗}(T ).

Corollary 2 Modulo auxiliary letters, NAT is (semantically) a fragment of L_{Circ}, and polynomial-time embedded via σ^{⋆}.

Notice that is not possible to add in Step 2 of the embedding σ^{⋆}(T ) the quantified variables in φ to the fixed atoms.

Example 3 Reconsider the NAT T in Ex. 2. Note that ∅ is the unique model of σ(T ). The formula σ^{⋆}(T_{1}) has, if we disregard ab_{1}, ab_{2} (which are fixed in it), the models M_{1} = {ab_{3}, z} and M_{2} = {ab_{4}}. They give rise to the two models N_{1} = {ab_{1}, z, ab_{3}} and N_{2} = {ab_{4}} of σ^{⋆}(T_{1}) ∧ (ab_{1} ↔ z), of which N_{2} is ab_{1}, ab_{2}; ab_{3}, ab_{4}, z-minimal.

However, if ab_{3}, ab_{4} were fixed in σ^{⋆}(T ), then both N_{1} and N_{2} would be models of σ^{⋆}(T ), as they are ab_{1}, ab_{2}; zminimal. Therefore, Proposition 3 would fail.

Eliminating fixed letters Every fixed letter q can be removed from a NAT T similarly as from a formula φ ∈ L_{Circ}. However, we must take into account that a fixed letter q may not be simply declared as a minimized letter in the rewriting, since there is a special set Ab of minimized letter which has restricted uses. We surpass this by introducing two special abnormality letters ab_{q} and \overline{ab_{q}} in Ab, and by adding the formula (q ↔ ab_{q}) ∧ (ab_{q} ↔ ¬\overline{ab_{q}}) as a new block to T , a well as ab_{q} ↔ ¬\overline{ab_{q}} in every other block of T . The letter q is declared floating in T .

4.1 Complexity of NATs

Ordinary circumscription can express a QBF sentence Φ = ∀X∃Y ψ (where ψ ∈ L) as follows. Let u be a fresh variable.

Lemma 1 (cf. [Eiter and Gottlob, 1993]) Φ is true if and only if Circ(φ; u; Y) ⊧ ¬u, where φ = ψ ∨ u.

This circumscription can be easily stated as a NAT. Set

T_{1} = {Y, u : φ, u ↔ ab}.

Then Lemma 1 implies that T_{1} ⊧ ¬u iff Φ is true. In fact, denote for any interpretation M and set of atoms S by t_{M}(S) the assignment to S as given by M. Then, every model M of T_{1} must be, if we fix the atoms in X to t_{M}(X), a model of φ such that M ⊧ u if and only if ψ[X/t_{M}(X)] is unsatisfiable.

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

Consider the case of a QBF Φ = ∀X∃Y ψ[V], where V are free variables in it, considered as “parameters”. We nest T_{1} into the following theory T_{2}:

T_{2} = {X ∪ Y, u : T_{1}, u ↔ ¬ab}

This amounts to the following circumscription:

σ(T_{2}) = ∃abCirc({∃abCirc(φ ∧ (u↔ab); ab; Y, u)∧ \atop (u↔¬ab); ab; X ∪ Y, u).}

The outer circumscription minimizes ab and thus maximizes u. σ(T_{2}) is, by Proposition 3, equivalent to the formula

σ^{⋆}(T_{2}) = Circ(σ^{⋆}(T_{1}) ∧ (u↔¬a_{2}); a_{2}; X ∪ Y, u, a_{1}),
σ^{⋆}(T_{1}) = Circ(φ ∧ (u↔a_{1}); a_{1}; Y, u)

modulo the atoms a_{1} and a_{2}. The following can be shown: Lemma 2 T_{2} ⊧ u if and only if for every assignment s(V), the QBF ∃X∀Y ¬ψ[V/s(V)] is true (i.e., Φ[V/s(V)] is false).

It follows from the lemma that deciding, given a NAT T_{2} of nesting depth 1 and ψ ∈ L, whether T_{2} ⊧ ψ is Π_{3}^{P} -hard. We generalize this pattern to encode the evaluation of a

QBF

Φ = Q_{n}X_{n}Q_{n−1}X_{n−1} ⋯ ∀X_{2}∃X_{1}ψ, n ≥ 1, (2)

where the quantifiers Q_{i} alternate, into inference T ⊧ ψ from a NAT theory T as follows.

Let φ = ψ ∨ u, where u is a fresh atom. Define inductively

T_{1} = {X_{1}, u : φ, u ↔ ab},
T_{2k} = {X_{1}, …, X_{2k}, u : T_{2k−1}, u ↔ ¬ab},
T_{2k+1} = {X_{1}, …, X_{2k+1}, u : T_{2k}, u ↔ ab},

for all 2k, 2k + 1 ∈ {2, …, n}, and let T_{0} = { : φ}. Note that T_{0} is equivalent to φ, and that nd(T_{i}) = i − 1, for all i ∈ {1, …, n} while nd(T_{0}) = 0. We obtain the following. Lemma 3 For every n ≥ 1, T_{n−1} has some model, and

• if n is odd, then T_{n−1} ⊧ u iff Φ is false, i.e., ¬Φ is true;

• if n is even, then T_{n−1} ⊧ ¬u iff Φ is true.

This statement can be proved by induction on n ≥ 1. Lemma 4 Model checking for NATs, i.e., deciding whether a given interpretation M is a model of a given NAT T , is in PSPACE. If nd(T ) ≤ k for constant k ≥ 0, then it is in Π_{k+1}^{P}. Proof: For k = 0, the problem amounts to model checking for ordinary circumscription, which is in coNP. For k > 0, we can test recursively for each block B of T whether M is a model of each block B_{1}, …, B_{n} in B = {C : B_{1}, …, B_{n}}, and that no model N of B_{1}, …, B_{n} exists such that N <_{Ab;C} M. The recursion depth is linear, and the procedure runs in quadratic space. Moreover, if nd(T ) is bounded by a constant k, then the check for M and the existence of N witnessing that M is not model of B, can be done in nondeterministic polynomial time with an oracle for Π_{k}^{P}. Thus, the problem is in PSPACE (resp., in Π_{k+1}^{P}). □

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 L_{Circ} formula. The following theorem highlights the consequences of such relations on complexity of inference wrt a NAT.

Theorem 3 Deciding, given a NAT theory T and a propositional formula φ, whether T ⊧ φ is PSPACE-complete. If nd(T ) ≤ k for constant k ≥ 0, then it is Π_{k+2}^{P}-complete.

Proof: The hardness part follows from Lemma 3 above. As for the membership part, a model M of T such that M |̸= φ can be guessed and verified in PSPACE (resp., with the help of a Π_{k+1}^{P}-oracle). Thus the problem is in co-NPSPACE = PSPACE (resp., Π_{k+2}^{P}). □

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 T and an interpretation M, deciding whether M ⊧ T is PSPACE-complete. If nd(T ) ≤ k for a constant k ≥ 0, then the problem is Π_{k+1}^{P}-complete.

Proof: (Sketch) By Lemma 4, it remains to show the hardness parts. Note that for k = 0, 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 T_{0}, …, T_{n} be as there, with the only difference that φ = ψ ∨ u is replaced by

φ′ = (ψ∨u∨(X_{n}∧v))∧((X_{n}∧v) → X_{1}∪⋯∪X_{n−1}∪ϵ_{n}),

where ϵ_{n} = {u} if n is odd and ϵ_{n} = {¬u} otherwise. Here v is a new letter, defined (i.e., floating) in T_{n} and fixed elsewhere; X_{n} resp. X_{1}∪⋯∪X_{n−1}∪ϵ_{n} is viewed as conjunction of its formulas. Let T′_{0}, …, T′_{n} be the resulting NATs.

Define M = ⋃_{i=1}^{n} X_{i} ∪ {v, u} if n is odd and M = ⋃_{i=1}^{n} X_{i} ∪ {v} if n is even. Note that M ⊧ φ′ and M is, modulo u, the only candidate for a model of T′_{n} in which X_{n} and v are true: any such model must satisfy φ′, and if X_{n} ∧ v are true, then all other atoms have a unique truth value.

It holds that M is a model of T′_{n} iff the QBF Φ is false (resp., true). It follows that model checking is PSPACEhard and Π_{k+1}^{P}-hard if nd(T ) ≤ k for constant k; note that nd(T′_{n}) = n − 1. □

4.2 A polynomial-time fragment

We call a block {C : B_{1}, …, B_{n}} Horn, if each B_{i} is a Horn CNF if B_{i} ∈ L, and recursively B_{i} is Horn otherwise. A NAT T is Horn, if each of its blocks is Horn.

In [Cadoli and Lenzerini, 1994], it was shown that deciding Circ(φ; P; ∅) ⊧ ¬u, where φ is a propositional Horn CNF and u is an atom, is coNP-complete. That is, already for Horn NATs T without nesting (i.e., nd(T ) = 0) 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 q is possible via auxiliary atoms ab_{q} ∈ Ab and Horn axioms q → ab_{q}, ab_{q} → q in T .

Call any P; Z-minimal model of a NAT T such that P = At \ Ab and Z = ∅ a minimal model of T .

Theorem 5 Let T be a Horn NAT without fixed letters. Then,

(1) T has a least (i.e., a unique minimal) model, and (2) T is equivalent to a Horn CNF φ(T ). Furthermore, both φ(T ) and M(T ) are computable in polynomial time.

Proof: (Sketch) Let, for any Horn CNF ψ and model M ⊆ At, be ψ^{M} the Horn CNF resulting from ψ after substituting each ab_{j} ∈ Ab by ⊤ (true) if M ⊧ ab_{j} and by ⊥ (false) if M ⊧ ¬ab_{j} and subsequent standard simplifications.

Let T be a single block B = {Z : B_{1}, …, B_{n}}, where Z = At \ Ab. Define the Horn CNF φ(B) recursively by

φ(B) := ⋀_{B_{i}∈L} B_{i}^{M_{0}} ∧ ⋀_{B_{i}∉L} φ(B_{i}),

where M_{0} = M_{0}(B) is the least model of the Horn CNF

ψ(B) := ⋀_{B_{i}∈L} B_{i} ∧ ⋀_{B_{i}∉L} φ(B_{i}),

and

M(B) := M_{0}[At \ Ab] (= M_{0}[Z]).

Then, by induction on nd(B)≥0, we can show that (1) M(B) is the least model of B, and (2) φ(B) is equivalent to B.

Let, for any formula α, block B, NAT T etc denote ∥α∥, ∥B∥, ∥T ∥ etc the representation size of the respective object. Obviously, we can compute φ(B) inductively. For the Horn CNFs ψ(B) and φ(B), we have ∥ψ(B)∥ ≤ ∥B∥ and ∥φ(B)∥ ≤ ∥B∥. Of the model M_{0}, we only need its restriction M_{0}[A] to the atoms A occurring in B (all other atoms are irrelevant for computing φ(B)). We can compute M_{0}[A] from ψ(B) in O(∥B∥) time (recall that the least model of a Horn CNF α is computable in O(∥α∥) time), and ⋀_{B_{i}∈L} B_{i}^{M_{0}} from M_{0}[A] in O(∥B∥) time. Overall, it follows that for T = B, we can compute both φ(T ) and its least model M(T ) in time O(#b(T )∥T ∥), where #b(T ) is the number of (recursive) blocks in T , thus in polynomial time. By Prop. 2, we can replace a multiple block T = B_{1}, …, B_{n} by T′ = {At \ Ab : B_{1}, …, B_{n}}, which is Horn and without fixed letters, and obtain analogous results. □

Using sophisticated data structures, the (relevant parts of) models M_{0}(B) above can be computed incrementally, where each clause in φ(B) is fired at most once. Overall, φ(T ) and M(T ) are computable in O(∥T ∥) time. We thus have:

Theorem 6 (Flat Normal Form) Every Horn NAT T without fixed letters can be rewritten to an equivalent Horn NAT {Z : φ} without fixed letters, where φ ∈ L is a Horn CNF, in O(∥T ∥) 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 T without fixed letters is polynomial.

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

For the inference problem, we obtain the following result.

Theorem 7 Given a Horn NAT T without fixed letters and φ ∈ L, deciding T ⊧ φ is coNP-complete. If φ is a CNF, then the problem is polynomial.

Proof: Since model checking is polynomial, the problem is clearly in coNP. The coNP-hardness part follows from coNP-completeness of validity checking for a given φ ∈ L (ask whether {Z : ⊤} ⊧ φ, where Z contains all letters).

We can reduce T ⊧ ψ to φ(T ) ⊧ ψ in O(∥T ∥) time, where φ(T ) is a Horn CNF. If ψ = ⋀_{i=1}^{m} α_{i} is a CNF of clauses α_{i}, the latter can be checked in O(m∥φ(T )∥ + ∥ψ∥) time, thus in O(m∥T ∥+∥ψ∥) time (check φ(T ) ⊧ α_{i}, which is O(∥φ(T )∥ + ∥α_{i}∥) time, for all i ∈ {1, ….m}). □

5 Other Generalizations of Circumscription

As we have discussed above, fixed letters can be removed from L_{Circ} 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 Circ(φ; P; Z) by partitioning the letters P into priority levels P_{1} >P_{2} > ⋯ > P_{n}, and informally pruning all models of φ which are not minimal on P_{i}, while Z ∪P_{i+1} ∪⋯∪P_{n} floats and P_{1} ∪ ⋯ ∪ P_{i−1} is fixed, for i = 1, …, n (cf. [Lifschitz, 1994]). This can be readily expressed as the nested circumscription Circ(⋯ Circ(Circ(φ; P_{1}; Z∪P_{2}∪⋯∪P_{n}); P_{2}; Z∪ P_{3}∪⋯∪P_{n}) ⋯). This generalization differs from L_{Circ} and NATs: The complexity does not increase, as inference and model checking remain Π_{2}^{P} -complete and coNP-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, Curb(φ; P; Z) for a formula φ ∈ L is the smallest set M ⊆ mod(φ) which contains all models of Circ(φ; P; Z) and is closed under minimal upper bounds in mod(φ). A minimal upper bound (mub) of a set M′ of models in mod(φ) is a model M ∈ mod(φ) such that (1) M′ ≤_{P;Z} M, for every M′ ∈ M′, and (2) there exists no N ∈ mod(φ) satisfying item 1 such that N <_{P;Z} M′.

For example, φ = a ∨ b has two minimal models, if all letters are minimized (P = At = {a, b}): {a} and {b}. The model {a, b} is not a minimal model of φ, but is a curb model of φ. Thus, Curb(a ∨ b) ≡ a ∨ b. On the other hand, if At = {a, b, c}, then Curb(a ∨ b) ≡ (a ∨ b) ∧ ¬c is different from a ∨ b; the unsupported letter c is set to false. Note that Circ(a ∨ b) ≡ (a ↔ ¬b) ∧ c is different from Curb(a ∨ b).

Like for L_{Circ} and NATs, inference and model checking for Curb(φ; P; Z) 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 L_{Circ} and NATs can not. We can, e.g., write a (fixed) interpreter T_{I} in this language for curbing varying propositional 3CNF formulas φ, input as ground facts F (φ), such that the curb models of T_{I} ∪ F (φ) 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 L_{Circ} or NAT theory (unless PH=PSPACE). Further relationships between L_{Circ} 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.

References

[Baral et al., 1998] C. Baral, A. Gabaldon, and A. Provetti. Formalizing narratives using nested circumscription. Artificial Intelligence, 104(1-2):107–164, 1998.

[Baral et al., 2000] C. Baral, V. Kreinovich, and R. Trejo. Computational complexity of planning and approximate planning in the presence of incompleteness. Artificial Intelligence, 122(1/2):241–267, 2000.

[Cadoli and Lenzerini, 1994] M. Cadoli and M. Lenzerini. The complexity of propositional closed world reasoning and circumscription. JCSS, 43:165–211, 1994.

[de Kleer and Konolige, 1989] J. de Kleer and K. Konolige. Eliminating the fixed predicates from a circumscription. Artificial Intelligence, 39:391–398, 1989.

[Eiter and Gottlob, 1993] T. Eiter and G. Gottlob. Propositional circumscription and extended closed world reasoning are Π_{2}^{p}-complete. Theoretical Computer Science, 114(2):231–245, 1993.

[Eiter and Gottlob, 2000] T. Eiter and G. Gottlob. On the complexity of theory curbing. In Proc. LPAR-2000, LNCS 1955, 1–19. 2000.

[Eiter et al., 1993] T. Eiter, G. Gottlob, and Y. Gurevich. Curb your theory! A circumscriptive approach for inclusive interpretation of disjunctive information. In Proc. IJCAI-93, 634–639. Morgan Kaufman, 1993.

[Gogic et al., 1995] G. Gogic, H.A. Kautz, Ch.H. Papadimitriou, and B. Selman. The Comparative Linguistics of Knowledge Representation. In Proc. IJCAI-95, 862–869. [Lifschitz, 1985] V. Lifschitz. Computing circumscription.

In Proc. IJCAI-85, 121–127, 1985. [Lifschitz, 1994] V. Lifschitz. Circumscription. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, eds, Handbook of Logic in AI and Logic Programming, III, 297-352. 1994. [Lifschitz, 1995] V. Lifschitz. Nested abnormality theories.

Artificial Intelligence, 74(2):351–365, 1995. [McCarthy, 1980] J. McCarthy. Circumscription – A form of non-monotonic reasoning. Artif. Intell., 13:27–39, 1980. [Pollett and Remmel, 1997] C. Pollett and J. Remmel. Nonmonotonic reasoning with quantified boolean constraints. In Proc. LPNMR’97, 18–39, LNCS 1265. Springer, 1997. [Rintanen, 1999] J. Rintanen. Improvements to the evaluation of quantified boolean formulae. In Proc. IJCAI ’99, 1192–1197. AAAI Press, 1999.

[Wagner, 1990] K. Wagner. Bounded query classes. SIAM Journal of Computing, 19(5):833–846, 1990.