Defeasible Inclusions in Low-Complexity DLs: Preliminary Notes

1 Introduction

The ample literature on nonmonotonic extensions of description logics (DLs) witnesses a long-standing interest for this topic (for some early approaches see [Brewka, 1987; Straccia, 1993; Baader and Hollunder, 1995]). Recently, fresh motivations came from the construction of ontologies for biomedical domains (cf. [Rector, 2004; Stevens et al., 2007]) and from the use of description logics as policy languages [Uszok et al., 2004; Kagal et al., 2003; Tonti et al., 2003] where nonmonotonic reasoning is needed to properly encode default policies and authorization inheritance (cf. [Bonatti and Samarati, 2003]). Several recent works [Donini et al., 1998; 1997; 2002; Bonatti et al., 2006; Giordano et al., 2008] improved our understanding of the complexity of nonmonotonic description logics based on default logic, autoepistemic logic, and circumscription. Unfortunately, nonmonotonic DLs are typically very complex. For example, reasoning with circumscribed ALC knowledge bases is NExpNP-hard [Bonatti et al., 2006], and a tableaux calculus for reasoning with autoepistemic knowledge bases is in 3-ExpTime [Donini et al., 2002]. Besides such complexity results, it turns out that some theoretical properties that are very important for the implementation of reasoning in "classical" DLs-such as the tree model property for example- do not carry over to nonmonotonic DLs.

Independently from the works on nonmonotonic DLs, lowcomplexity (monotonic) DLs of practical interest have been recently studied. Here we will focus on DL-liteR [Calvanese et al., 2005] and the EL family [Baader, 2003; Baader et al., 2005], whose inferences are in PTIME. The former is motivated by efficient query processing over large

L. Sauro

sauro@na.infn.it

bodies of semantic web knowledge. The latter is interesting because it is spontaneously adopted in major biomedical ontologies. It is interesting to investigate whether the syntactic restrictions obeyed by such logics decrease the complexity of reasoning also in a nonmonotonic context.

In this paper, we identify less complex circumscribed DLs by (i) using the constructs supported by DL-liteR and by the EL family, and (ii) restricting the use of abnormality predicates by hiding them into "defeasible" inclusion axioms, similar to those adopted by [Straccia, 1993]. The latter restriction is also expected to make the formalism easier to use. Under such restrictions, we prove that (i) satisfiability checking for circumscribed knowledge bases (KB) is equivalent to classical KB satisfiability, and hence in P (sometimes even trivial) for the logics we consider here: DL-liteR, EL, and EL⊥; (ii) concept satisfiability, instance checking, and subsumption over circumscribed DL-liteR and left local EL⊥ KBs remain within the second level of the polynomial hierarchy; (iii) the same reasoning tasks for circumscribed EL⊥ KBs, unfortunately, remain ExpTime-hard.

Further related approaches are [Cadoli et al., 1990; Straccia, 1993]. In [Cadoli et al., 1990], a fragment of ALE under minimal entailment (an instance of circumscription where all predicates are minimized with the same priority) is proved to belong to Πp2 . Our approach adopts different DLs and more general forms of circumscription, supporting priorities as well as fixed and variable predicates. In [Straccia, 1993] the underlying nonmonotonic logic is a prioritized version of default logic. The paper contains NP-hardness results for extremely simplified DLs.

The rest of the paper is organized as follows: In Section 2, we recall the basics of DLs. Section 3 introduces the specialized circumscription framework we adopt here. After some auxiliary results (Section 4), sections 5 and 6 illustrate the results on DL-liteR and the EL family, respectively. Section 7 concludes the paper with a summary of the results and some directions for future work.

2 Preliminaries

In DLs, concepts are inductively defined with a set of constructors, starting with a set NC of concept names, a set NR of role names, and (possibly) a set NI of individual names (all countably infinite). We use the term predicates to refer to elements of NC ∪NR. Hereafter, letters A and B will range over NC, P will range over NR, and a, b, c will range over NI. The concepts of the DLs dealt with in this paper are formed using the constructors shown in Figure 1. There, the inverse role constructor is the only role constructor, whereas the remaining constructors are concept constructors. Letters C,D will range over concepts and letters R, S over (possibly inverse) roles.

The semantics of the above concepts is defined in terms of interpretations I = (ΔI , ·I ). The domain ΔI is a non-empty set of individuals and the interpretation function ·I maps each concept name A ∈ NC to a set AI ⊆ ΔI , each role name r ∈ NR to a binary relation rI on ΔI , and each individual name a ∈ NI to an individual aI ∈ ΔI . The extension of ·I to inverse roles and arbitrary concepts is inductively defined as shown in the third column of Figure 1. An interpretation I is called a model of a concept C if CI ̸= ∅. If I is a model of C, we also say that C is satisfied by I.

A (strong) knowledge base is a finite set of (i) concept inclusions (CIs) C ⊑ D where C and D are concepts, (ii) concept assertions A(a) and role assertions P(a, b), where a, b are individual names, P ∈ NR, and A ∈ NC, (iii) role inclusions (RIs) R ⊑ R′ . An interpretation I satisfies (i) a CI C ⊑ D if CI ⊆ DI , (ii) an assertion C(a) if aI ∈ CI , (iii) an assertion R(a, b) if (aI , bI ) ∈ rI , and (iv) a RI R ⊑ R′ iff RI ⊆ R′I . Then, I is a model of a strong knowledge base S iff I satisfies all the elements of S.

We write C ⊑S D iff for all models I of S, I satisfies C ⊑ D.

The logic DL-lightR [Calvanese et al., 2005] restricts concept inclusions to expressions CL ⊑ CR, where

(as usual, ∃R abbreviates ∃R.⊤).

The logic EL [Baader, 2003; Baader et al., 2005] restricts knowledge bases to assertions and concept inclusions built from the following constructs:

(note that inverse roles are not supported). The extension of EL with ⊥, role hierarchies, and nominals (respectively) are denoted by EL⊥, ELH, and ELO. Combinations are allowed: for example ELHO denotes the extension of EL supporting role hierarchies and nominals. Finally, EL¬A denotes the extension where negation can be applied to concept names.

3 Defeasible knowledge

A defeasible inclusion (DI) is an expression A ⊑n C whose intended meaning is: A's elements are normally in C.

A defeasible knowledge base (DKB) in a logic DL is a pair (S,D) where S is a strong DL knowledge base, and D is a set of DIs A ⊑n C such that C is a DL concepts.

Example 3.1 The sentences: "in humans, the heart is usually located on the left-hand side of the body; in humans with situs inversus, the heart is located on the right-hand side of the body" [Rector, 2004; Stevens et al., 2007] can be formulated with the following EL⊥ inclusions

Human ⊑n ∃has heart.∃has position.Left ; Situs Inversus ⊑ ∃has heart.∃has position.Right ; ∃has heart.∃has position.Left ⊓ ∃has heart.∃has position.Right ⊑ ⊥ .

Intuitively, a model of (S,D) is a model of S that maximizes the set of individuals satisfying the defeasible inclusions in D, resolving conflicts by means of specificity whenever possible.

In order to formalize this idea, we first have to specify how DIs are prioritized. We determine specificity based on classically valid inclusions. For all DIs δ1 = (A1 ⊑n C1) and δ2 = (A2 ⊑n C2), we write

For the sake of readability, the subscript S will be omitted when clear from context.

Second, we have to specify how to deal with the predicates occurring in the knowledge base: is their extension allowed to vary in order to satisfy defeasible inclusions? A discussion of the effects of letting predicates vary vs. fixing their extension can be found in [Bonatti et al., 2006]; they conclude that the appropriate choice is application dependent. Here we let roles vary to avoid undecidability problems (cf. [Bonatti et al., 2006]). The set of concept names NC, on the contrary, can be arbitrarily partitioned into two sets F and V containing fixed and varying predicates, respectively; we denote this semantics with CircF .

The set F, the DIs D, and their ordering ≺ induce a strict partial order over interpretations, defined below. As we move down the ordering we find interpretations that are more and more normal w.r.t. D. For all δ = (A ⊑n C) and all interpretations I let the set of individuals satisfying δ be:

Definition 3.2 For all interpretations I and J , and all F ⊆ NC, let I <D,F J iff:

1. ΔI =ΔJ ;
2. aI = aJ , for all a ∈ NI;
3. AI = AJ , for all A ∈ F;
4. for all δ ∈ D, if satI(δ) ̸⊇ satJ (δ) then there exists δ′ ∈ D such that δ′ ≺ δ and satI(δ′ ) ⊃ satJ (δ′ ) ;
5. there exists a δ ∈ D such that satI(δ) ⊃ satJ (δ).

The subscript D will be omitted when clear from context.

Definition 3.3 [Model] Let KB = (S,D) and F ⊆ NC. An interpretation I is a model of CircF (KB) iff I is a (classical) model of S and for all models J of S, J ̸<F I.

Remark 3.4 This semantics is a special case of the circumscribed DLs of [Bonatti et al., 2006]. The correspondence can be seen by (i) introducing for each DI A ⊑n C a fresh atomic concept Ab, playing the role of an abnormality predicate; (ii) replacing A ⊑n C with A ⊓ ¬Ab ⊑ C; (iii) minimizing the predicates Ab introduced above according to the priorities over defeasible inclusions.

In order to enhance readability, we will use the following notation for the special cases in which all concept names are varying and the case in which they are all fixed: <var and Circvar stand for <∅ and Circ∅, respectively; <fix and Circfix stand respectively for <NC and CircNC .

In this paper, we consider the following standard reasoning tasks over defeasible DLs:

Knowledge base consistency Given a DKB KB, decide whether CircF (KB) has a model.

Concept consistency Given a concept C and a DKB KB, check whether C is satisfiable w.r.t. KB , that is, there exists a model I of CircF (KB) such that CI ̸= ∅.

Subsumption Given two concepts C, D and a DKB KB, check whether CircF (KB) |= C ⊑ D, that is, for all models I of CircF (KB), CI ⊆ DI .

Instance checking Given a ∈ NI, a concept C, and a DKB KB, check whether CircF (KB) |= C(a), that is, for all models I of CircF (KB), aI ∈ CI .

We conclude this section with an example taken from [Bonatti et al., 2006].

Example 3.5 The following inclusions model a policy with authorization inheritance and multiple overridings:

User ⊑n ¬∃hasAccessTo.ConfidentialFile Staff ⊑ User Staff ⊑n ∃hasAccessTo.ConfidentialFile BlacklistedStaff ⊑ Staff⊓ ¬∃hasAccessTo.ConfidentialFile .

Let S contain the second and fourth inclusions plus the assertion Staff(John), and let D consist of the first and third inclusions. Let KB = (S,D). Due to the second inclusion, the DI for Staff has greater priority than the DI for User. In all models of Circvar(KB), John belongs to ∃hasAccessTo.ConfidentialFile and not to BlacklistedStaff. On the contrary, there exist models of Circfix(KB) where John does not belong to ∃hasAccessTo.ConfidentialFile because John belongs to BlacklistedStaff and Circfix does not allow to change the extension of BlacklistedStaff to satisfy the DI for Staff.

4 Auxiliary results

The logics we deal with enjoy the finite model property.

Lemma 4.1 Let KB = (S,D) be a DKB in DL-liteR or ELHO⊥,¬. For all F ⊆ NC, CircF (KB) has a model only if CircF (KB) has a finite model whose size is exponential in the size of KB.

Proof. A simple adaptation of a result for ALCIO [Bonatti et al., 2006], taking role hierarchies into account.

As a consequence, these logics preserve classical consistency (because all <D,F -descending chains of models originating from a finite model must be finite):

Theorem 4.2 Let KB = (S, D) be a DKB in in DL-liteR or ELHO⊥,¬. For all F ⊆ NC, S is (classically) consistent iff CircF (KB) has a model.

Under very mild assumptions, CircF and Circfix (which is a special case of the former) are equally expressive.

Theorem 4.3 If DL is a description logic supporting unqualified existential restrictions (∃R), then concept consistency, subsumption, and instance checking in CircF (DL) can be reduced in polynomial time to concept consistency, subsumption, and instance checking (respectively) in Circfix(DL).

The idea behind the proof is simple: Let KB be any given DKB. Introduce a new role name RA for each (variable) concept name A ̸∈ F. Then replace each occurrence of any A ̸∈ F with ∃RA. The details of the proof are omitted here for space limitations.

5 Complexity of circumscribed DL-liteR

In this section we focus on DL-liteR DKBs (S,D) that consist in a DL-liteR KB S and a set D of inclusions A ⊑n C such that A ⊑ C is a (classical) DL-liteR CI. Our complexity results for DL-liteR rely on the possibility of extracting a small (polynomial-size) model from any model of a circumscribed DKB. We start with Circvar :

Lemma 5.1 Let KB be a DL-liteR knowledge base. For all models I of Circvar(KB) and all x ∈ ΔI there exists a model J of Circvar(KB) such that (i) ΔJ ⊆ ΔI , (ii) x ∈ ΔJ , (iii) for all DL-liteR concepts C, x ∈ CI iff x ∈ CJ , and (iv) |ΔJ | is polynomial in the size of KB.

Proof. Assume that KB = (S,D), I is a model of Circvar(KB), and x ∈ ΔI . Let cl(KB) be the set of all concepts and individual names occurring in KB. Choose a minimal set Δ ⊆ ΔI containing: (i) x, (ii) all aI such that a ∈ NI ∩cl(KB), (iii) for each concept ∃R in cl(KB) satisfied in I, a node yR such that for some z ∈ ∃RI , (z, yR) ∈ RI .

Now define J as follows: (i) ΔJ = Δ, (ii) aJ = aI (for a ∈ NI ∩ cl(KB)), (iii) AJ = AI ∩ Δ (A ∈ NC ∩ cl(KB)), and (iv) P J = {(z, yP ) | z ∈ Δ and z ∈ ∃P I } ∪ {(yP , z) | z ∈ Δ and z ∈ ∃P -I } (P ∈ NR).

Note that by construction, for all z ∈ ΔJ and for all C ∈ cl(KB), z ∈ CJ iff z ∈ CI ; consequently, J is a classical model of S. Moreover, the cardinality of ΔJ is linear in the size of KB (by construction). So we are only left to show that J is a <D,var-minimal model of KB.

Suppose not, and consider any J ′ <D,var J . Define I ′ as follows: (i) ΔI′ = ΔI , (ii) aI′ = aI , (iii) AI′ = AJ ′ , (iv) P I′ = P J ′ . Note that the elements in ΔI \ΔJ ′ satisfy no left-hand side of any DL-liteR inclusion (be it classical or defeasible), therefore all inclusions are vacuously satisfied. Moreover, the restriction of I ′ to ΔJ ′ is <D,var-smaller than the corresponding restriction of I in the interpretation ordering. It follows that I ′ <D,var I, and hence I cannot be a model of Circvar(KB) (a contradiction).

The above proof can be refined and adapted to Circfix.

Lemma 5.2 Let KB be a DL-liteR knowledge base. For all models I of Circfix(KB) and all x ∈ ΔI there exists a model J of Circfix(KB) such that (i) ΔJ ⊆ ΔI , (ii) x ∈ ΔJ , (iii) for all DL-liteR concepts C, x ∈ CI iff x ∈ CJ (iv) |ΔJ | is polynomial in the size of KB.

Proof. We will employ a refined definition of Δ. It should be a ⊆-minimal set containing: (i) x, (ii) all aI such that a ∈ NI ∩cl(KB), (iii) for each concept ∃R in cl(KB) satisfied in I, a node yR such that yR ∈ (∃R-)I , and finally (iv) for all inclusions C ⊑ ∃R or C ⊑n ∃R in KB such that (C ⊓ ∃R)I ̸= ∅, a node z ∈ (C ⊓ ∃R)I .

Define J as in the previous lemma, using the above Δ. Recall that for all z ∈ ΔJ and for all C ∈ cl(KB), z ∈ CJ iff z ∈ CI ; consequently, J is a classical model of S. Moreover, the cardinality of ΔJ is linear in the size of KB (by construction). So we are only left to show that J is a <D,fix-minimal model of KB.

Suppose not, and consider any J ′ <D,fix J . Define I ′ as follows: (a)ΔI′ = ΔI , (b) aI′ = aI , (c) AI′ = AI , (d) each RI′ is a minimal set such that (d1) RI′ ⊇ RJ ′ , (d2) for all z ∈ ΔI \ΔJ , and for all inclusions C ⊑ ∃R or C ⊑n ∃R in KB such that z ∈ (C ⊓ ∃R)I , if RJ ′ contains a pair (v,w), then (z,w) ∈ RI′ ; finally, (d3) each P I′ is closed under the role inclusion axioms of KB. Note that, by construction,

Now we prove that I ′ is a model of the CIs of KB. By construction, the edges (z,w) introduced in (d2) do not change the set of existential restrictions satisfied by the members of ΔJ ′ ; as a consequence-and since J ′ is a model of KB-the members of ΔJ ′ satisfy all the CIs of KB.

Now consider an arbitrary element z ∈ ΔI′ \ΔJ ′ and any CI γ of KB. If γ is ∃-free, then I and I ′ give the same interpretation to γ by definition, therefore z satisfies γ. If γ is ∃R ⊑ A, ∃R ⊑ ¬A, ∃R ⊑ ¬∃S, or A ⊑ ¬∃R (and considering that I satisfies γ) z fails to satisfy γ only if for some R′ ∈ {R, S}, z ̸∈ (∃R′ )I and z ∈ (∃R′ )I′ ; this is impossible by (*). Next, suppose γ is ∃R ⊑ ∃S. If z ∈ (∃R)I′ , then by (**) there exists a v ∈ ΔJ ′ satisfying (∃R)J ′ and hence (∃S)J ′ (as J ′ is a model of KB), therefore z ∈ (∃S)I′ (by d2). We are only left to consider γ = A ⊑ ∃R: If z ∈ AI′ = AI , then there exists wA ∈ AJ ′ (by construction of Δ). Then z ∈ (∃R)I′ (by d2). Therefore, in all possible cases, z satisfies γ.

This proves that I ′ satisfies all the CIs of KB. It is not hard to verify that I ′ satisfies also all role inclusions of KB. Therefore, in order to derive a contradiction, we are left to prove that I ′ <D,fix I (which implies that I is not a model of Circfix(KB)).

Claim: For all δ ∈ D, if satJ (δ) ⊆ satJ ′(δ), then satI(δ) ⊆ satI′ (δ).

Suppose satJ (δ) ⊆ satJ ′(δ). It suffices to prove that for all z ∈ ΔI′ \ΔJ ′ , if z ∈ satI(δ) then z ∈ satI′(δ).

In all cases but those in which the right-hand side of δ is ∃R, the proof is similar to the proof for CIs (it exploits (*) and the fact that all atomic concepts are fixed).

Finally, let δ be A ⊑n ∃R and consider an arbitrary z ∈ ΔI′ \ ΔJ ′ such that z ∈ satI(δ) and z ∈ (A ⊓ ∃R)I . By (iv), Δ contains a v ∈ (A ⊓ ∃R)I , and hence ΔJ ′ contains a v ∈ (A ⊓ ∃R)J ′ ; consequently, by (d2), z ∈ (∃R)I′ and hence z ∈ satI′ (δ). This completes the proof of the claim.

Now, I ′ <D,fix I follows as a straightforward consequence of the Claim.

Theorem 5.3 Concept consistency over circumscribed DLliteR DKBs is in Σp2 . Subsumption and instance checking over circumscribed DL-liteR DKBs are in Πp2 .

Proof. (Sketch) By the above lemmas, it suffices to guess a polynomial model I of the KB that proves consistency or disproves subsumption/instance checking. Then, with an NP oracle, one can check that I is minimal w.r.t. <var or <fix.

6 Circumscribing the EL family

In ELHO, that cannot express any contradictions, defeasible inclusions cannot be possibly blocked under Circvar, and circumscription collapses to classical reasoning:

Theorem 6.1 Let KB = (S, D) be an ELHO DKB. Then I is a model of Circvar(KB) iff I is a model of S ∪ ˆD, where ˆD = {A ⊑ C | (A ⊑n C) ∈ D}.

By the results of [Baader et al., 2005], it follows that in Circvar(ELHO), concept satisfiability is trivial, subsumption and instance checking are in P.

If we make EL more interesting by adding ⊥ as a source of inconsistency, then complexity increases significantly.

Theorem 6.2 In Circvar(EL⊥), concept satisfiability, instance checking, and subsumption are ExpTime-hard. These results still holds if knowledge bases contain no assertion. 1

Proof. (Sketch) We first reduce TBox satisfiability in EL¬A (which is known to be ExpTime-hard [Baader et al., 2005]) to the complement of subsumption in Circvar(EL⊥). Let T be a TBox (i.e., a set of CIs) in EL¬A. First introduce for each concept name A occurring in T a fresh concept name ¯ A whose intended meaning is ¬A. Obtain T ′ from T by replacing each literal ¬A with ¯ A. Let KB be the DKB obtained by extending T ′ with the following inclusions, where U and UA - for all A occurring in T - are fresh concept names (representing undefined truth values), and R is a fresh role name:

1 Equivalently, in DL's terminology: ABoxes are empty.

It can be verified that T is satisfiable iff in some model of Circvar(KB) all UA are empty, which holds iff Circvar(KB) ̸|= ⊤ ⊑ ∃R.U. Consequently, subsumption in Circvar(EL⊥) is ExpTime-hard.

Similarly, for any given a ∈ NI, T is satisfiable iff there exists a model I of Circvar(KB) such that aI ̸∈ (∃R.U)I . Therefore, instance checking in Circvar(EL⊥) is ExpTimehard as well.

Finally, add a fresh concept name B and all the inclusions B⊓∃R.UA ⊑ ⊥; call the newDKBKB′ . Note that T is satisfiable iff in some model of Circvar(KB) all UA are empty, which holds iff B is satisfiable w.r.t. Circvar(KB′ ). Consequently, concept satisfiability in Circvar(EL⊥) is ExpTimehard.

Since Circvar is a special case of CircF , and by Theorem 4.3, the above theorem applies to CircF and Circfix, too:

Corollary 6.3 For X = F, fix, concept satisfiability checking, instance checking, and subsumption in CircX(EL⊥) are ExpTime-hard. These results still hold if ABoxes are empty (i.e. assertions are not allowed).

The above proof can be adapted to CircF (EL). First we have to introduce a new concept name D representing ⊤ and translate each concept C into C∗ as follows:

• C∗ = C if C is a concept name;

¯

¯

• C∗ = A if C is ¬A (for all A, A is a new concept name);
• C∗ = D ⊓ ∃R.(C∗ 1 ⊓D) if C is ∃R.C1;
• C∗ = C∗ 1 ⊓C∗ 2 if C is C1 ⊓C2.

Each C1 ⊑ C2 in T is translated into C∗ 1 ⊑ C∗ 2 . Then we extend the translated TBox with the following inclusions, where Bot (representing ⊥), all UA, and Bad are new concept names and R is a new role name:

Let KB be the resulting DKB. Finally set F = {D, Bot}. Now (24) guarantees that D is nonempty; the translation (·)∗ , (10) and (11) make sure that by restricting to D any model I of CircF (KB) where all UA and Bot are empty one obtains a model of T . Inclusion (19) gives (20) and (21) lowest priority. These two DIs and (22)-(23) include D′ into Bad whenever the intended meaning of the atoms ¯ A is violated. Then T is satisfiable iff for some model I of CircF (KB), Bad I = ∅. In turn, this happens iff CircF (KB) ̸|= D ⊑ Bad, and iff aI ̸∈ Bad I . Then we have the desired reduction from EL¬A TBox satisfiability to the complement of subsumption and instance checking in CircF (EL). As a consequence, and by Theorem 4.3:

Theorem 6.4 Instance checking and subsumption are ExpTime-hard both in CircF (EL) and in Circfix(EL). The same holds in the restriction of EL not supporting ⊤.

Concept consistency is simpler, instead. Call an interpretation I maximal iff for all A ∈ NC, AI = ΔI , and for all P ∈ NR, P I = ΔI × ΔI . It is not hard to verify that all ELHO concepts and all ELHO inclusions (both classical and defeasible) are satisfied by all x ∈ ΔI , therefore maximal models are always models of CircF (KB), for all DKBs KB and all F ⊆ NC. As a consequence we have that concept consistency is trivial:

Theorem 6.5 For all EL concepts C, DKBs KB, and F ⊆ NC, C is satisfied by some model of CircF (KB).

One of the causes of the complexity of instance checking and subsumption for Circfix(EL⊥) is the ability of inferring consequences from qualified existential restrictions ∃P.B. By limiting their occurrences, it is possible to reduce significantly the complexity of instance checking and subsumption for Circfix(EL⊥) knowledge bases.

Definition 6.6 An EL⊥ knowledge base is left local (LL) if its concepts inclusions are instances of the following

where A and B can be concept names or ⊥. A LL EL⊥ concept is any concept that can occur in the above inclusions.

Note the similarity with the normal form of EL inclusions [Baader et al., 2005] that, however, would allow the more general inclusions ∃P.A ⊑ B and ∃P1.A ⊑ ∃P2.B .

Lemma 6.7 Let KB be an LL EL⊥ knowledge base. For all models I ∈ Circvar(KB) and x ∈ ΔI there exists a model J ∈ Circvar(KB) such that (i) ΔJ ⊆ ΔI , (ii) x ∈ ΔJ , (iii) |ΔJ | is polinomial in the size of KB.

Proof. The proof is analogous to the proof of Lemma 5.1. Here we start with a slightly different set Δ. Choose a minimal set Δ ⊆ ΔI containing: (i) x, (ii) all aI such that a ∈ NI ∩cl(KB), (iii) for each concept ∃P in cl(KB) satisfied in I, a node yP such that for some z ∈ ∃P I , (z, yP ) ∈ P I and (iv) for each concept ∃P.B in cl(KB) satisfied in I, a node yP,B such that for some z ∈ ∃P.BI , (z, yP,B) ∈ P I and yP,B ∈ BI .

Now define J as follows: (i) ΔJ = Δ, (ii) aJ = aI (for a ∈ NI ∩cl(KB)), (iii) AJ = AI ∩Δ (A ∈ NC∩cl(KB)), and (iv) P J = {(z, yP ) | z ∈ Δ and z ∈ ∃P I } ∪ {(z, yP,B) | z ∈ Δ and z ∈ ∃P.BI } (P ∈ NR).

The rest of the proof is similar to the proof of Lemma 5.1 and is omitted here for space limitations. We only remark that the restriction to LL KBs is needed to ensure that J is a classical model of the CIs in KB.

Lemma 6.8 Let KB be a LL EL⊥ knowledge base. For all models I ∈ Circfix(KB) and x ∈ ΔI there exists a model J ∈ Circfix(KB) such that (i) ΔJ ⊆ ΔI , (ii) x ∈ ΔJ , (iii) |ΔJ | is polinomial in the size of KB.

(*) Classical up to ELHO (by Theorem 6.1)

Table 1: Summary of complexity results

Proof. Similar to the proof of Lemma 5.2. Use a slightly modified, minimal set Δ ⊆ ΔI containing: (i) x, (ii) all aI such that a ∈ NI ∩ cl(KB), (iii) for each concept ∃P in cl(KB) satisfied in I, a node yP such that for some z ∈ ∃P I , (z, yP ) ∈ P I , (iv) for each concept ∃P.B in cl(KB) satisfied in I, a node yP,B such that for some z ∈ ∃P.BI , (z, yP,B) ∈ P I and yP,B ∈ BI and finally (v) for all inclusions C ⊑ ∃R.B or C ⊑n ∃R.B in KB such that (C ⊓ ∃R.B)I ̸= ∅, a node z ∈ (C ⊓ ∃R.B)I . The rest of the proof is similar to the proof of Lemma 5.2 and omitted here.

As a consequence of the above lemmata we get:

Theorem 6.9 Concept consistency over circumscribed LL EL⊥ DKBs is in Σp2 . Subsumption and instance checking over circumscribed LL EL⊥ DKBs are in Πp2 .

7 Conclusions and further work

The complexity of circumscribed description logics can be significantly reduced by (i) restricting the underlying DL to DL-liteR and to suitable members of the EL family, and (ii) restricting nonmonotonic constructs to defeasible inclusions A ⊑n C. KB satisfiability is equivalent to its classical version (by Theorem 4.2) and hence it is within P (sometimes even trivial) for the logics we investigated. The results for all the other reasoning tasks are summarized in Table 1. Surprisingly, fixed predicates in conjunction with qualified existential restrictions are powerful enough to keep the complexity of instance checking and subsumption ExpTime-hard even for a language like EL, which is not able to express any inconsistency. For DL-liteR and LL EL⊥, complexity drops to Σp2 and Πp2 , instead.

We are currently sharpening our complexity bounds, and extending them to more expressive logics, looking for alternatives to left-local KBs to confine complexity within the polynomial hierarchy. These theoretical results and the semantic properties emerging from their proofs will be exploited to design suitable calculi and algorithms for reasoning with circumscribed defeasible knowledge bases.