On the Complexity of EL with Defeasible Inclusions

1 Introduction

Literature shows a recurrent interest in extending description logics with nonmonotonic reasoning. Early approaches date back to [Brewka, 1987; Straccia, 1993; Baader and Hollunder, 1995a]). Some of the latest motivations originate from the ontologies for biomedical domains and the need of modelling prototypical entities (cf. [Rector, 2004; Stevens et al., 2007]); others arise from the policy languages based on description logics [Uszok et al., 2004; Kagal et al., 2003; Tonti et al., 2003] where nonmonotonic reasoning is needed to express default policies and exceptions [Bonatti et al., 2009a]. So far practical solutions have not been found mainly because of high asymptotic complexity coupled with the absence of effective optimization methods.

Circumscription is particularly interesting in this context. It supports in a natural way specificity-based overriding of inherited properties [Bonatti et al., 2009a], that is, the crucial feature needed to address the aforementioned application requirements. 1 In general, reasoning with circumscribed description logics is very complex, e.g. NExpNP-hard for circumscribed ALC knowledge bases [Bonatti et al., 2009b]. For this reason, in [Bonatti et al., 2009a] we investigated circumscribed low-complexity description logics of practical interest, such as DL-liteR [Calvanese et al., 2005] and the EL family [Baader, 2003; Baader et al., 2005], proving that complexity can be reduced within the second level of the polynomial hierarchy. However, no matching lower complexity bounds were provided.

∗This work is very partially supported by the Italian national project LoDeN ( http://loden.fisica.unina.it ).

1 This feature is known also as defeasible inheritance and is analogous to the inheritance mechanism of object-oriented languages.

In this paper we extend our previous results on EL⊥ in several ways. First, the characterization of complexity for the old framework is completed by providing matching hardness results and tightening some upper complexity bounds. Then we extend the framework to support more general queries, general defeasible inclusions (whose left-hand side can be a compound concept), and explicit priorities over defeasible inclusions (that generalize the specificity-based priorities adopted in [Bonatti et al., 2009a]). Finally, we relax the LL restriction adopted in our previous paper (that forbids qualified existentials in the left-hand side of inclusions) by supporting a more liberal use of existential quantification and terminologies (that is, acyclic sets of definitions of the form A ≡ C, where C may depend on qualified existential restrictions). This extension covers axioms commonly used by important knowledge bases such as GALEN and SNOMED. Some restrictions on acyclic definitions are still needed to confine complexity within the second level of the polynomial hierarchy. Further contributions will be discussed later.

The rest of the paper is organized as follows: In Section 2, we recall the basics of circumscribed DLs. Sections 3 and 4 deal with the characterization of complexity for variable and fixed concept names, respectively. Section 5 proves thatin some contexts-extensions such as arbitrary partitions in fixed and variable concepts, general defeasible inclusions, and arbitrary priorities do not increase the complexity of reasoning. Section 6 studies the complexity of LL with acyclic terminologies. Two sections on related work and conclusions complete the paper.

2 Syntax and Semantics of Circumscribed EL

We assume the reader to be familiar with the syntax and semantics of monotonic Description Logics. We refer to [Baader et al., 2003, Chap. 2] for details and notation. The sets of concept names, role names, and individual names are denoted by NC, NR, and NI, respectively. By predicate we mean any member of NC ∪ NR. Hereafter, letters A and B range over NC, P and R range over NR, and a, b, c range over NI. Letters C,D range over concepts.

A (strong) knowledge base is a finite set of (i) concept inclusions (CIs) C ⊑ D, (ii) concept assertions A(a), and (iii) role assertions P(a, b). Recall that an interpretation I satisfies (i) a CI C ⊑ D if CI ⊆ DI , (ii) an assertion C(a) if aI ∈ C I , (iii) an assertion R(a, b) if (aI , bI ) ∈ rI . 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 EL [Baader, 2003; Baader et al., 2005] restricts the language to the following constructs:

The extension of EL with ⊥ is denoted by EL⊥.

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

Example 2.1 [Bonatti et al., 2009a] 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 formalized with the EL⊥ axioms and GDIs:

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

A defeasible knowledge base (DKB) in a logic DL is a pair 〈K, ≺〉, where K = KS ∪ KD, KS is a strong DL KB, KD is a set of GDIs C ⊑n D such that C ⊑ D is a DL inclusion, and ≺ is a strict partial order (a priority relation) over KD.

The priority relation ≺K adopted in [Bonatti et al., 2009a] is based on specificity: For all GDIs δ1 = (C1 ⊑n D1) and δ2 = (C2 ⊑n D2), let

Example 2.2 The access control policy: "Normally users cannot read project files; staff can read project files; blacklisted staff is not granted any access" can be encoded with:

Staff ⊑ User

Blacklisted ⊑ Staff UserRequest ≡ ∃subj.User ⊓ ∃target.Proj ⊓ ∃op.Read StaffRequest ≡ ∃subj.Staff ⊓ ∃target.Proj ⊓ ∃op.Read UserRequest ⊑n ∃decision.Deny StaffRequest ⊑n ∃decision.Grant ∃subject.Blacklisted ⊑ ∃decision.Deny ∃decision.Grant ⊓ ∃decision.Deny ⊑ ⊥ .

Staff members cannot simultaneously satisfy the two defeasible inclusions (due to the last inclusion above). With specificity, the second defeasible inclusion overrides the first one and yields the intuitive inference that non-blacklisted staff members are indeed allowed to access project files.

The semantics of DKBs depends on which predicates are allowed to vary in order to maximize the set of individuals satisfying the GDIs. In [Bonatti et al., 2009a], roles are always allowed to vary, to avoid undecidability problems. 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. Fixed predicates retain their classical semantics, while varying predicates can be affected by nonmonotonic inferences.

The set F, the GDIs KD, and their ordering ≺ induce a strict preference ordering over interpretations, defined below. Roughly speaking, I is preferred to J if some GDIs are satisfied by more individuals in I than in J , possibly at the cost of satisfying less lower-priority GDIs. Formally, for all δ = (C ⊑n D) and all interpretations I let the set of individuals satisfying δ be:

Definition 2.3 Let KB = 〈K, ≺〉 be a DKB. For all interpretations I and J , and all F ⊆ NC, let I <KB,F J iff:

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

The subscript KB will be omitted when clear from context. Now a model of a DKB can be defined as a maximally preferred model of its strong (i.e. classical) part.

Definition 2.4 [Model] Let KB = 〈K,≺〉 and F ⊆ NC. An interpretation I is a model of CircF (KB) iff I is a (classical) model of KS and for all models J of KS, J ̸<F I.

In order to enhance readability, <var and Circvar stand for <∅ and Circ∅, respectively; <fix and Circfix stand respectively for <NC and CircNC . The standard reasoning tasks are adapted to DKBs as follows: 2

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 .

It has been proved in [Bonatti et al., 2009a] that reasoning in circumscribed EL⊥ is ExpTime-hard, and that complexity decreases for left local EL⊥ knowledge bases (LL EL⊥, for short). This fragment consists of the following schemata:

where A can be either a concept name or ⊤, and B either a concept name or ⊥. A LL EL⊥ concept is any concept that can occur in the above inclusions. It has been proved that if KB is a LL EL⊥ knowledge base, then LL EL⊥ subsumption and instance checking 3 are in Πp2 , and LL EL⊥ concept consistency in Σp2 .

2 KB consistency is equivalent to its classical counterpart [Bonatti et al., 2009a], therefore it will not be dealt with in this paper.

3 Subsumption is LL EL⊥ if C and D are LL EL⊥ concepts; instance checking and concept consistency are LL EL⊥ if C is. Similar terminology applies to other fragments.

3 Complexity of Circvar(LL EL⊥)

Now we prove that reasoning in Circvar(LL EL⊥) is actually hard (and hence complete) for Σp2 and Πp2 . For this purpose, we provide a reduction of minimal entailment over positive, propositional disjunctive logic programs (PDLP for short), that was proved to be Πp2 hard in [Eiter and Gottlob, 1995, Theorem 5]. A PDLP over a set of propositional variables PV = {p1, . . . , pn} is a set of clauses S = {c1, . . . , cm} over PV where each cj contains at least one positive literal. The minimal-entailment problem can be then defined as follows: given a literal l, S |=min l if and only if every ⊆- minimal Herbrand model I of S satisfies l.

For each propositional variable pi, 1 ≤ i ≤ n, introduce two concept names Pi and ¯ Pi - where the latter encodes ¬pi. In the following we will denote by Lj , 1 ≤ j ≤ 2n, a generic Pi or ¯ Pi. For each clause cj ∈ S introduce a concept name Cj. Then, two other concept names True and False represent the set of true and false literals respectively. Finally, the concept names Lit and Min are used to model minimal propositional assignments; we need also an auxiliary role R.

First, literals are reified, i.e. modelled as individuals, with the axioms:

The first axiom makes all Li nonempty. Axioms (2) make them pairwise disjoint. Finally, axioms (3) minimize the Li and make them singletons. Then, we represent S by adding for each clause cj = lj1 ∨ · · · ∨ ljh, 1 ≤ j ≤ m, the axioms

By axioms (4) and (5), Cj equals the set of literals in cj. Axioms 6 make sure that each clause holds.

In order to model the concepts True and False and the correct meaning of complementary literals we add the axioms

The axioms defined so far encode the classical semantics of S. To minimize models, add the following axioms:

By (12) and (13), Min collects false positive literals and true negative literals. By (14) and (15), Lit contains all the (representations of) literals and clauses. The purpose of these axioms is giving defeasible inclusions (3) and (5) higher

(specificity-based) priority than (16), so that model minimization cannot cause any Li to be larger than a singleton, nor any Cj to be different from the set of literals of cj. Now (16) prefers those models where as many Pi as possible are in False.

In the following, given a PDLP S, let KBS be the Tbox defined above.

Lemma 3.1 Given a PDLP S, a literal l in S's language, and the encoding L of l, the following are equivalent:

(minimal entailment) S |=min l

(subs) Circvar(KBS) |= ⊤ ⊑ ∃R.(True ⊓L);

(co-sat) False ⊓ L is not satisfiable w.r.t Circvar(KBS);

(instance checking) Circvar(KBS) |= (∃R.(True ⊓L))(a).

The conjunctions (⊓) nested in ∃ can be easily replaced with a new atom A by adding the equivalence A ≡ True ⊓ L, that can itself be encoded in LL EL⊥, so we have:

Theorem 3.2 Subsumption and instance checking over Circvar(LL EL⊥) are Πp2 -hard; concept satisfiability is Σp2 - hard. These results hold even if queries are restricted to LL EL⊥ concepts, and priorities are specificity-based.

4 Complexity of Circfix(EL⊥)

When concept names are all fixed, reasoning in LL EL⊥ is tractable:

Theorem 4.1 LL EL⊥ subsumption, instance checking, and concept consistency over Circfix(LL EL⊥) DKBs are in P.

The proof is based on a deterministic version of Algorithm 1 (see below), and exploits the fact that defeasible inclusions cannot interfere with each other in LL EL⊥, regardless of ≺ (details are omitted due to space limitations).

Complexity is low under Circfix because in this context LL axioms are not general enough to simulate quantifier nesting nor conjunctions of existential restrictions. In Circvar these features can be simulated by abbreviating compound concepts C with concept names A using equivalences A ≡ C such that C does not depend on qualified existentials (hence the LL restriction is preserved). With Circfix, such equivalences change the semantics of C whenever C is (or contains) an existential restriction, because A is fixed and prevents C from varying freely. As we reintroduce the missing features, complexity increases again.

Let LL2EL⊥ support the schemata:

The reader may easily verify that LL2EL⊥ is equivalent to LL EL⊥ plus schema ∃P1 ⊓ ∃P2 ⊑ ∃P3.B. The missing axioms can be reformulated using fresh roles R and suitable equivalences ∃R ≡ C (that preserve C's semantics because R is a varying predicate).

Theorem 4.2 Subsumption and instance checking over Circfix(LL2EL⊥) are coNP-hard; concept satisfiability is NP-hard. These results hold even if queries are restricted to LL2EL⊥ concepts, and priorities are specificity-based.

Proof. By reduction of SAT. For each propositional variable pi introduce the concept names Ai, ¯ Ai, and role Ui, representing pi's truth value (resp. true, false, and undefined). These alternatives are made mutually inconsistent with:

For each given clause cj = lj,1∨· · ·∨lj,n, introduce a concept name ¯ Cj representing cj's falsity. Add ¯Lj,1⊓· · ·⊓ ¯Lj,n ⊑ ¯ Cj , where ¯Lj,k represents the complement of lj,k (k = 1, . . . , n).

¯

Define a concept name F representing the falsity of the given set of clauses, and a disjoint concept F with:

Now, with a defeasible inclusion, ∃Ui is forced to be true for all individuals that satisfy neither Ai nor ¯ Ai; moreover, a role U detects undefined literals:

Let K be the set of above inclusions and KB = 〈K,≺K〉. It can be proved that the given set of clauses S is unsatisfiable iff Circfix(KB) |= F ⊑ ∃U, therefore subsumption checking is coNP-hard.

Similarly, it can be proved that S is unsatisfiable iff Circfix(KB′ ) |= (∃U)(a), where KB′ = 〈K′ ,≺K′〉 and K′ = K∪{F(a)}; therefore instance checking is coNP-hard.

Finally, it can be proved that S is satisfiable iff F ⊓ ∃OK is satisfiable w.r.t. Circfix(KB′′ ), where KB′′ = 〈K′′ ,≺K′′〉 and K′′ = K ∪ {∃U ⊓ ∃OK ⊑ ⊥}; therefore satisfiability checking is NP-hard. We are only left to remark that K can be easily encoded in LL2EL⊥.

We prove that this bound is tight using Algorithm 1. There, we assume without loss of generality that C = AC ⊓ bigsqcapni=1 ∃Pi.Bi. The algorithm nondeterministically looks for an individual x (in some model) that satisfies C and not D. S1 guesses any additional fixed concept names satisfied by x; S2 guesses the concept names that are satisfied somewhere in the model (not necessarily by x) and finally ≺′ guesses a total extension of ≺ that determines the application order of GDIs.

The algorithm selects, according to ≺′ , the defeasible inclusions that are active in x and accumulates the rhs of those that are not blocked. A defeasible inclusion A ⊑n ∃R.B is blocked only if ∃R.B (i) entails locally ⊥ or a concept name not satisfied by x, or (ii) entails globally the non-emptyness of a concept name that should be empty. The rationale behind blocking is that concept names are fixed and circumscription cannot change their extension as the application of A ⊑n ∃R.B would instead require in cases (i) and (ii). Conditions (i)-(ii) are checked, respectively, by means of the sets of concepts SupCls(X) (the set of atomic concepts that subsume X) and NonEmpty(X,KS) (the set of concept names that must be nonempty if X is).

Note that the variable part of C (i.e. bigsqcapni=1 ∃Pi.Bi) is introduced in X only in line 8, after all defeasible inclusions have been applied, because defeasible inclusions can influence the variable part (e.g. by forcing it to be empty).

Theorem 4.3 LL2EL⊥ subsumption and instance checking over Circfix(LL2EL⊥) are in coNP; LL2EL⊥ concept satisfiability is in NP.

Algorithm 1:

• Data: C = AC ⊓ bigsqcapn1 ∃Pi.Bi, D, KB = 〈K, ≺〉. 1 Guess S1, S2 ⊆ NC, where ⊓S1 |= AC and S1 ⊆ S2, and a linearization ≺′ of ≺; 2 A := {A ⊑n ∃P.B | ⊓S1 |= A}; 3 X := bigsqcap S1; 4 while A ̸= ∅ do 5 remove from A the ≺′ -minimal inclusion A ⊑n ∃P.B; 6 if SupCls(X ⊓ ∃P.B) ⊆ S1 and NonEmpty(X ⊓ ∃P.B, KS) ⊆ S2 then 7 X := X ⊓ ∃P.B; 8 X := X⊓ bigsqcapn1 ∃Pi.Bi; 9 return SupCls(X) ̸⊆ S1 or NonEmpty(X,KS) ̸⊆ S2 or X ⊑KS D;

Proof. (Sketch) Assume without loss of generality that C = AC ⊓ bigsqcapni=1 ∃Pi.Bi. It can be proved that Algorithm 1 returns true iff the subsumption C ⊑ D is valid. Moreover, SupCls(·) and NonEmpty(·, ·) can be computed in polynomial time using standard EL reasoning. The theorem for subsumption immediately follows. Concept consistency can be solved by setting D = ⊥. An instance checking problem D(a) can be solved by collecting in C all the properties of a classically entailed by KS.

It can be verified that the LL2 fragment does not support quantifier nesting.

Let full LL EL⊥ (in symbols, LLfEL⊥) support all the inclusions A ⊑n D and C ⊑ D such that A ∈ NC ∪ {⊤}, C and D are EL⊥ concepts, and no qualified existentials occur in C. The reader may easily verify that full LL EL⊥ is equivalent to LL2EL⊥ plus quantifier nesting. The exact complexity of Circfix(LLfEL⊥) is still unknown. A lower bound is provided in the next section.

5 Complexity of CircF(EL⊥) and Extensions

The circuscribed EL⊥ introduced in Section 2 generalizes the definitions of [Bonatti et al., 2009a] in two ways: First, GDIs can be freely prioritized through ≺, and are not restricted to ≺K (specificity-based priority). Second, in a GDI C ⊑n D, C is not restricted to concept names. These extensions do not increase complexity. We first show how to encode extended DKBs in the old framework using additional fixed concepts.

Let KB = 〈K,≺〉 be any given DKB in EL⊥. First we need to define a new fixed concept AΔ that encodes the domain without being equivalent to ⊤. This requires the following transformation:

Obtain K∗ from K by transforming all inclusions in K and by adding a nonemptiness axiom ⊤ ⊑ ∃aux.AΔ (aux a fresh role) plus an assertion AΔ(a) for each a ∈ NI occurring in K. It is not hard to see that the restrictions to AΔ of the models of K∗ correspond to the classical models of K. Now we have to remove the new features. For all GDIs δ = (C ⊑n D) ∈

K∗D , add two fresh predicates Aδ,Rδ and replace δ with the following axiom schemata:

Call the newDKBKB′ = 〈K′ , ≺K′ 〉. By (17), the specificitybased relation ≺K′ prioritizes the new GDIs according to the original priorities. It is not difficult to verify that all the reasoning tasks such that none of the new predicates Aδ and Rδ occur in the query yield the same answer in 〈K∗ ,≺∗ 〉 and KB′ . Note that the above transformations preserve the LLfEL⊥ format. As a consequence of the above discussion, by combining the transformation ·∗ and (17), (18), we have:

Theorem 5.1 Let DL be either EL⊥ or LLfEL⊥. Reasoning in Circfix(DL) with explicit priorities and GDIs can be reduced in polynomial time to reasoning in Circfix(DL) with only specificity-based priority and defeasible inclusions of the form A ⊑n ∃R.

One of the applications of this theorem is proving that CircF (and hence Circvar) can be reduced to Circfix in full LL.

Theorem 5.2 Let DL be either EL⊥ or LLfEL⊥. Reasoning in CircF (DL) with explicit priorities and GDIs can be reduced in polynomial time to reasoning in Circfix(DL) with only specificity-based priority and defeasible inclusions of the form A ⊑n ∃R.

Proof. (Sketch) First remove all variable concepts by introducing a fresh role name RA for each A ̸∈ F, and uniformly replacing A with ∃RA. Then apply the reduction of Lemma 5.1 to remove explicit priorities and general defeasible inclusions (including those introduced by the elimination of variable predicates).

As a corollary of Theorem 5.2 and Theorem 3.2 we have: Corollary 5.3 Subsumption and instance checking over Circfix(LLfEL⊥) are Πp2 -hard; concept satisfiability is Σp2 - hard. These results hold even if queries are restricted to LL EL⊥ concepts, and priorities are specificity-based.

6 Supporting Acyclic Terminologies

In this section the expressive power of acyclic terminologies 4 is partially recovered.

Definition 6.1 An EL⊥ knowledge base KB = 〈K, ≺〉 is almost LL (aLL for short) iff (i) K = KLL ∪ Ka , (ii) KLL is in full LL, (iii) KBa is a classical acyclic terminology, and (iv) if a concept name A defined in Ka occurs in the left-hand side of an inclusion in KLL , then A does not depend (in Ka) on any qualified existential restriction.

Example 6.2 This DKB is in aLL. Ka consists of the first two equivalences:

Yes ≡ ∃decision.Grant No ≡ ∃decision.Deny UserRequest ⊑ ∃subj.User ⊓ ∃target.Proj ⊓ ∃op.Read StaffRequest ⊑ ∃subj.Staff ⊓ ∃target.Proj ⊓ ∃op.Read UserRequest ⊑n No StaffRequest ⊑n Yes .

4 A finite set of definitions A ≡ C is a terminology if no A occurs in the left-hand side of two different definitions. Given A ≡ C, if B occurs in C then A directly uses B; uses is the transitive closure of directly uses. A terminology is acyclic if no A uses itself.

In general, a concept name A occurring in a terminology T can be extended with default properties by means of an inclusion A ⊑n C in the following cases: A can be a primitive concept (with no definition in T , e.g. Grant), or a concept partially defined by a one-way inclusion (e.g. UserRequest), or even a concept with a definition A ≡ D in T , provided that A does not depend on any qualified existentials.

The small model property of LL [Bonatti et al., 2009a] can be extended to Circvar(aLLEL⊥) and more general queries. Let depth(D) be the maximum quantifier nesting level in D.

Lemma 6.3 Let KB = 〈K, ≺K〉 be an aLL EL⊥ knowledge base (where K = Ka ∪ KLL) and let C, D be EL⊥ concepts. For all models I ∈ Circvar(KB) and for all x ∈ C I \DI there exists a model J ∈ Circvar(KB) such that (i) ΔJ ⊆ ΔI , (ii) x ∈ C J \DJ , and (iii) |ΔJ | is O((|KB|+|C|)d ), where d = depth(D) + 1 + |Ka|2 .

Consequently, as in [Bonatti et al., 2009a], we can prove:

Theorem 6.4 In Circvar(aLL EL⊥) with specificity-based priorities concept satisfiability is in Σp2 . Moreover, deciding EL⊥ subsumptions C ⊑ D or instance checking problems D(a) with a constant bound on the quantifier depth of D's unfolding (w.r.t. the given DKB) is in Πp2 .

Currently, we do not know whether the bound on quantifier nesting depth is necessary to the above result. However, we can prove that the restriction to Circvar and <K is essential. By means of a reduction of quantified boolean formulae (QBF) satisfiability, it can be proved that:

Theorem 6.5 Subsumption checking in Circfix(aLL EL⊥) is PSPACE-hard, even if quantifier mesting depth is bounded by a constant.

It can be proved that the same holds for Circvar(aLL EL⊥) with general priorities, that can simulate fixed concepts.

7 RelatedWork

DLs have been extended with nonmonotonic constructs such as default rules [Straccia, 1993; Baader and Hollunder, 1995a; Baader and Hollunder, 1995b], autoepistemic operators [Donini et al., 1997; Donini et al., 2002], and circumscription [Cadoli et al., 1990; Bonatti et al., 2009b; Bonatti et al., 2009a; Bonatti et al., 2010]. The paper [Bonatti et al., 2009a] and this paper have the same goals and adopt essentially the same framework. Here the results of [Bonatti et al., 2009a] are refined and extended as summarized in the next section. The results of [Bonatti et al., 2009b] concern languages more expressive that those considered here; accordingly, complexity is much higher and may reach NEXPTIMENP. A hybrid of Circfix and closed world assumption has been proved to be in PTIME [Bonatti et al., 2010]. A recent approach based on rational closures and ALC can be found in [Casini and Straccia, 2010]; complexity ranges from PSPACE to EXPTIME. A nonmonotonic version of EL based on a modal typicality operator has been introduced in [Giordano et al., 2009b; Giordano et al., 2009a]. Reasoning is NP-hard; the exact complexity is still unknown.

Figure 1: Main complexity results for EL⊥

8 Conclusions and FurtherWork

We proved lower complexity bounds for Circvar and CircF , matching the Πp2 and Σp2 membership results of [Bonatti et al., 2009a], and extended those upper bounds to more general queries (partially supporting quantifier nesting), general defeasible inclusions, and acyclic definitions (as in aLL knowledge bases); these results are summarized in the upper part of Fig. 1. The lower part summarizes the analysis of Circfix, that we proved to be less complex than Circvar, in some cases, because under Circfix, LL is not a normal form for full LL (LLf ). The analysis shows the impact of reintroducing conjunctions of existential restrictions (LL2) and quantifier nesting (LLf ). In Theorem 5.2 we introduced a general method for eliminating variable concepts, GDIs, and general priorities for sufficiently expressive languages. The exact complexity of Circfix(LLfEL⊥) is still an open question, and so is the question on whether limiting quantifier depth is essential to the upper bounds. Another open question is whether the NP/coNP upper bounds for LL2 can be extended beyond LL2EL⊥ queries. Additional features, such as the constructs supported by EL++, will be the subject of further work.