Pushing the EL Envelope

1 Introduction

The quest for tractable (i.e., polynomial-time decidable) description logics (DLs), which started in the 1980s after the first intractability results for DLs were shown [Brachman and Levesque, 1984; Nebel, 1988], was until recently restricted to DLs extending the basic language FL0, which allows for conjunction (⊓) and value restrictions (∀r.C). The main reason was that, when clarifying the logical status of property arcs in semantic networks and slots in frames, the decision was taken that arcs/slots should be read as value restrictions rather than existential restrictions (∃r.C).

For subsumption between concept descriptions, the tractability barrier was investigated in detail in the early 1990s [Donini et al., 1991]. However, as soon as terminologies (TBoxes) were taken into consideration, tractability turned out to be unattainable: even with the simplest form of acyclic TBoxes, subsumption in FL0 (and thus in all languages extending it) is coNP-hard [Nebel, 1990]. Subsumption in FL0 is PSPACE-complete w.r.t. cyclic TBoxes [Baader, 1996; Kazakov and de Nivelle, 2003], and we show in this paper that it becomes even EXPTIME-complete in the presence of general concept inclusion axioms (GCIs), which are supported by all modern DL systems.

For these reasons, and also because of the need for expressive DLs supporting GCIs in applications, from the mid 1990s on the DL community has mainly given up on the quest of finding tractable DLs. Instead, it investigated more and more expressive DLs, for which reasoning is worst-case intractable. The goal was then to find practical subsumption algorithms, i.e., algorithms that are easy to implement and optimize, and which-though worst-case exponential or even worsebehave well in practice (see, e.g., [Horrocks et al., 2000]). This line of research has resulted in the availability of highly optimized DL systems for expressive DLs [Horrocks, 1998; Haarslev and M¨ oller, 2001], and successful applications: most notably the recommendation by the W3C of the DLbased language OWL [Horrocks et al., 2003] as the ontology language for the Semantic Web.

Recently, the choice of value restrictions as a sine qua non of DLs has been reconsidered. On the one hand, it was shown that the DL EL, which allows for conjunction and existential restrictions, has better algorithmic properties than FL0. Subsumption in EL stays tractable w.r.t. both acyclic and cyclic TBoxes [Baader, 2003b], and even in the presence of GCIs [Brandt, 2004]. On the other hand, there are applications where value restrictions are not needed, and where the expressive power of EL or small extensions thereof appear to be sufficient. In fact, SNOMED, the Systematized Nomenclature of Medicine, employs EL [Spackman, 2000] with an acyclic TBox. Large parts of the Galen medical knowledge base can also be expressed in EL with GCIs and transitive roles [Rector and Horrocks, 1997]. Finally, the Gene Ontology [Consortium, 2000] can be seen as an acyclic EL TBox with one transitive role.

Motivated by the positive complexity results cited above and the use of extensions of EL in applications, we start with the DL EL with GCIs, and investigate the effect on the complexity of the subsumption problem that is caused by the addition of standard DL constructors available in ontology languages like OWL. We prove that the subsumption problem remains tractable when adding the bottom concept (and thus disjointness statements), nominals (i.e., singleton concepts), a restricted form of concrete domains (e.g., references to numbers and strings), and a restricted form 1 of role-value maps

1 Adding arbitrary role-value maps to EL is known to cause undecidability [Baader, 2003a].

(which can express transitivity and the right-identity rule required in medical applications [Spackman, 2000]). We then prove that, basically, all other additions of standard DL constructors lead to intractability of the subsumption problem, and in most cases even to EXPTIME-hardness. Proofs and further technical details can by found in the accompanying technical report [Baader et al., 2005].

2 The Description Logic EL++

In DLs, concept descriptions are inductively defined with the help of 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. In this section, we introduce the extension EL++ of EL, whose concept descriptions are formed using the constructors shown in the upper part of Table 1. There and in general, we use a and b to denote individual names, r and s to denote role names, and C,D to denote concept descriptions.

The concrete domain constructor provides an interface to so-called concrete domains, which permits reference to, e.g., strings and integers. Formally, a concrete domain D is a pair (∆D ,P D ) with ∆D a set and P D a set of predicate names. Each p ∈ P is associated with an arity n > 0 and an extension pD ⊆ (∆D )n . To provide a link between the DL and the concrete domain, we introduce a set of feature names NF. In Table 1, p denotes a predicate of some concrete domain D and f1, . . . , fk are feature names. The DL EL++ may be equipped with a number of concrete domains D1, . . . , Dn such that ∆Di ∩∆Dj = ∅ for 1 ≤ i < j ≤ n. If we want to stress the use of particular concrete domains D1, . . . , Dn, we write EL++(D1, . . . ,Dn) instead of EL++.

The semantics of EL++(D1, . . . ,Dn)-concept descriptions is defined in terms of an interpretation 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 subset AI of ∆I , each role name r ∈ NR to a binary relation rI on ∆I , each individual name a ∈ NI to an individual aI ∈ ∆I , and each feature name f ∈ NF to a partial function f I from∆I to ⋃1≤i≤n ∆Di . The extension of ·I to arbitrary concept descriptions is inductively defined as shown in the third column of Table 1.

An EL++ constraint box (CBox) is a finite set of general concept inclusions (GCIs) and role inclusions (RIs), whose syntax can be found in the lower part of Table 1. Note that a finite set of GCIs would commonly be called a general TBox. We use the term CBox due to the presence of RIs. An interpretation I is a model of a CBox C if, for each GCI and RI in C, the conditions given in the third column of Table 1 are satisfied. In the definition of the semantics of RIs, the symbol "◦" denotes composition of binary relations.

The main inference problem considered in this paper is subsumption. Given two EL++-concept descriptions C,D we say that C is subsumed by D w.r.t. the CBox C (C ⊑C D) iff CI ⊆ DI for all models I of C.

Some remarks regarding the expressivity of EL++ are in order. First, though we restrict the attention to subsumption, EL++ is expressive enough to reduce all other standard reasoning tasks (concept satisfiability, ABox consistency, instance problem) to the subsumption problem and vice versa [Baader et al., 2005]. Second, our RIs generalize three means of expressivity important in ontology applications: role hierarchies r ⊑ s; transitive roles, which can be expressed by writing r ◦ r ⊑ r; and so-called right-identity rules r ◦ s ⊑ s, which are important in medical applications [Spackman, 2000; Horrocks and Sattler, 2003]. Third, the bottom concept in combination with GCIs can be used to express disjointness of complex concept descriptions: C ⊓ D ⊑ ⊥ says that C, D are disjoint. Finally, the unique name assumption for individual names can be enforced by writing {a} ⊓ {b} ⊑ ⊥ for all relevant individual names a and b.

3 Tractability of EL++

Before we can describe a polynomial-time subsumption algorithm for EL++, we must introduce an appropriate normal form for CBoxes. Given a CBox C, we use BCC to denote the smallest set of concept descriptions that contains the top concept ⊤, all concept names used in C, and all concept descriptions of the form {a} or p(f1, . . . , fk) appearing in C. Then, C is in normal form if

1. all GCIs have one of the following forms, where C1, C2 ∈ BCC and D ∈ BCC ∪ {⊥}:

1. all role inclusions are of the form r ⊑ s or r1 ◦ r2 ⊑ s.

By introducing new concept and role names, any CBox C can be turned into a normalized CBox C ′ that is a conservative extension of C, i.e., every model of C ′ is also a model of C, and every model of C can be extended to a model of C ′ by appropriately choosing the interpretations of the additional concept and role names. In [Baader et al., 2005] it shown that this transformation can actually be done in linear time, yielding a normalized CBox C ′ whose size is linear in the size of C.

Lemma 1 Subsumption w.r.t. CBoxes in EL++ can be reduced in linear time to subsumption w.r.t. normalized CBoxes in EL++.

In the following, all CBoxes are assumed to be normalized. When developing the subsumption algorithm for normalized EL++ CBoxes, we can restrict our attention to subsumption

• CR1 If C′ ∈ S(C), C′ ⊑D ∈ C, and D ̸∈ S(C) then S(C) := S(C) ∪ {D}
• CR2 If C1,C2 ∈ S(C), C1 ⊓C2 ⊑D ∈ C, and D ̸∈ S(C) then S(C) := S(C) ∪ {D}
• CR3 If C′ ∈ S(C), C′ ⊑ ∃r.D ∈ C, and (C,D) /∈ R(r) then R(r) := R(r) ∪ {(C, D)}
• CR4 If (C,D) ∈ R(r), D′ ∈ S(D), ∃r.D′ ⊑ E ∈ C, and E /∈ S(C) then S(C) := S(C) ∪ {E}
• CR5 If (C,D) ∈ R(r), ⊥ ∈ S(D), and ⊥ /∈ S(C), then S(C) := S(C) ∪ {⊥}
• CR6 If {a} ∈ S(C) ∩S(D), C ⇝R D, and S(D) ̸⊆ S(C) then S(C) := S(C) ∪ S(D)
• CR7 If conj(S(C)) is unsatisfiable in Dj and ⊥ /∈ S(C), then S(C) := S(C) ∪ {⊥}
• CR8 If conj(S(C)) implies p(f1, . . . , fk) ∈ BCC in Dj and p(f1, . . . , fk) /∈ S(C), then S(C) := S(C) ∪ {p(f1, . . . , fk)}
• CR9 If p(f1, . . . , fk), p′ (f ′1, . . . , f ′k′) ∈ S(C), p ∈ P Dj , p′ ∈ P Dℓ , j ̸= ℓ, fs = f ′ t for some s, t, and ⊥ /∈ S(C), then S(C) := S(C) ∪ {⊥}
• CR10 If (C, D) ∈ R(r), r ⊑ s ∈ C, and (C, D) /∈ R(s) then R(s) := R(s) ∪ {(C, D)}
• CR11 If (C, D) ∈ R(r1), (D, E) ∈ R(r2), r1 ◦ r2 ⊑ r3 ∈ C, and (C,E) /∈ R(r3) then R(r3) := Ri(r3) ∪ {(C, E)}

Table 2: Completion Rules

between concept names. In fact, C ⊑C D iff A ⊑C′ B, where C ′ = C∪{A ⊑ C, D ⊑ B} with A and B new concept names. Our subsumption algorithm not only computes subsumption between two given concept names w.r.t. the normalized input CBox C; it rather classifies C, i.e., it simultaneously computes the subsumption relationships between all pairs of concept names occurring in C.

Now, let C be a CBox in normal form that is to be classified. We use RC to denote the set of all role names used in C. The algorithm computes

• a mapping S from BCC to a subset of BCC ∪{⊤, ⊥}, and
• a mapping R from RC to a binary relation on BCC.

The intuition is that these mappings make implicit subsumption relationships explicit in the following sense:

• (I1) D ∈ S(C) implies that C ⊑C D,
• (I2) (C,D) ∈ R(r) implies that C ⊑C ∃r.D.

In the algorithm, these mappings are initialized as follows:

• S(C) := {C,⊤} for each C ∈ BCC,
• R(r) := ∅ for each r ∈ RC.

Then the sets S(C) and R(r) are extended by applying the completion rules shown in Table 2 until no more rule applies.

Some of the rules use abbreviations that still need to be introduced. First, CR6 uses the relation ⇝R ⊆ BCC ×

BCC, which is defined as follows: C ⇝R D iff there are C1, . . . , Ck ∈ BCC such that

• C1 = C or C1 = {b} for some individual name b,
• (Cj, Cj+1) ∈ R(rj) for some rj ∈ RC (1 ≤ j < k),
• Ck =D.

Second, rules CR7 and CR8 use the notion conj(Si(C)), and satisfiability and implication in a concrete domain. If p is a predicate of the concrete domain Dj , then the EL++-concept description p(f1, . . . , fn) can be viewed as an atomic firstorder formula with variables f1, . . . , fn. Thus, it makes sense to consider Boolean combinations of such atomic formulae, and to talk about whether such a formula is satisfiable in (the first-order interpretation) Dj, or whether in Dj one such formula implies another one. For a set Γ of EL++(D1, . . . , Dn)- concept descriptions and 1 ≤ j ≤ n, we define

For the rules CR7 and CR8 to be executable in polynomial time, satisfiability and implication in the concrete domains D1, . . . ,Dn must be decidable in polynominal time. However, for our algorithm to be complete, we must impose an additional condition on the concrete domains. The concrete domain D is p-admissible iff

1. satisfiability and implication in D are decidable in polynominal time;
2. D is convex: if a conjunction of atoms of the form p(f1, . . . , fk) implies a disjunction of such atoms, then it also implies one of its disjuncts.

Let us now show that the rules of Table 2 indeed yield a polynomial algorithm for subsumption in EL++(D1, . . . ,Dn) provided that the concrete domains D1, . . . ,Dn are padmissible.

The following lemma is an easy consequence of the facts that (i) each rule application adds an element to one of the sets S(C) ⊆ BCC ∪ {⊤,⊥} or R(C,D) ⊆ BCC × BCC, (ii) the cardinality of BCC is polynomial in the size of C, and (iii) the relation ⇝R can be computed using (polytime) graph reachability, and (iv) the concrete domains are p-admissible.

Lemma 2 For a normalized CBox C, the rules of Table 2 can only be applied a polynomial number of times, and each rule application is polynomial.

The next lemma shows how all subsumption relationships between concept names occurring in C can be determined once the completion algorithm has terminated.

Lemma 3 Let S be the mapping obtained after the application of the rules of Table 2 for the normalized CBox C has terminated, and let A,B be concept names occurring in C. Then A ⊑C B iff one of the following two conditions holds:

• S(A) ∩ {B,⊥} ̸= ∅,
• there is an {a} ∈ BCC such that ⊥ ∈ S({a}).

The if-direction of this lemma (soundness) immediately follows from the fact that (I1) and (I2) are satisfied for the initial definition of S,R, and that application of the rules preserves (I1) and (I2). This is trivial for most of the rules. We consider CR6 in more detail. If {a} ∈ S(C) ∩ S(D), then C,D ⊑C {a}. Now, C ⇝R D implies that C ⊑C ∃r1. · · · ∃rk-1.D or {b} ⊑C ∃r1. · · · ∃rk-1.D for some individual name b. In the second case, this implies that D cannot be empty in any model of C, and in the first case it implies that D is non-empty in any model of C for which C is non-empty. Together with C,D ⊑C {a}, this implies that C ⊑C D, which shows that the rule CR6 is sound since it preserves (I1).

To show the only-if-direction of the lemma, we assume that the two conditions do not hold, and then use the computed mappings S,R to construct a model I of C such that AI ̸⊆ BI . Basically, the domain ∆I of this model consists of all elements C ∈ BCC such that A ⇝R C. However, we identify elements C,D of BCC if there is an individual name a such that {a} ∈ S(C) ∩ S(D). The interpretation of concept and role names is determined by S,R: if D ∈ BCC is a concept name, then DI = {C ∈ BCC | D ∈ S(C)}, and if r is a role name, then (C,D) ∈ rI iff (C,D) ∈ R(r). Finally, the interpretation of the feature names is determined by the the assignments satisfying the conjunctions conj(S(C)) (see [Baader et al., 2005] for a more detailed description of this construction, and a proof that it indeed yields a countermodel to the subsumption relationship A ⊑C B).

To sum up, we have shown the following tractability result:

Theorem 4 Let D1, . . . ,Dn be p-admissible concrete domains. Then subsumption in EL++(D1, . . . ,Dn) w.r.t. CBoxes can be decided in polynomial time.

P-admissibile and non-admissible concrete domains

In order to obtain concrete DLs of the form EL++(D1, . . . ,Dn) for n > 0 to which Theorem 4 applies, we need concrete domains that are p-admissible. In the following, we introduce two concrete domains that are p-admissible, and show that small extensions of them are no longer p-admissible.

The concrete domain Q = (◗, P Q) has as its domain the set ◗ of rational numbers, and its set of predicates P Q consists of the following predicates:

• a unary predicate ⊤Q with (⊤Q)Q = ◗;
• unary predicates =q and >q for each q ∈ ◗;
• a binary predicate =;
• a binary predicate +q, for each q ∈ ◗, with (+q)Q = {(q′ , q′′ ) ∈ ◗2 | q′ + q = q′′ }.

The concrete domain S is defined as (Σ∗ , P S ), where Σ is the ISO 8859-1 (Latin-1) character set and P S consistes of the following predicates:

• a unary predicate ⊤S with (⊤S)S = Σ∗ ;
• a unary predicate =w, for each w ∈ Σ∗ ;
• a binary predicate =;
• a binary predicate concw, for each w ∈ Σ∗ , with conc Qw = {(w′ , w′′ ) | w′′ = w′w}.

Polynomiality of reasoning in Q can be shown by a reduction to linear programming, and polynomiality of reasoning in S

has been proved in [Lutz, 2003]. Moreover, we can show [Baader et al., 2005] that both Q and S are convex.

Proposition 5 Q and S are p-admissible.

Both Q and S are interesting concrete domains since they allow us to refer to concrete numbers and strings in concepts, and use the properties of the concrete predicates when reasoning. However, the predicates available in these concrete domains are rather restricted. Unfortunately, p-admissibility is a fragile property, i.e., we cannot extend Q and S by other interesting predicates without losing p-admissibility. As an illustration, we consider one extension of Q and one of S.

The concrete domain Q≤q,>q extends Q by the additional unary predicates (≤q)q∈◗. Then the Q≤q,>q -conjunction >0(f ′ ) implies the disjunction ≤0(f) ∨ >0(f) without implying one of its disjuncts. Thus, Q≤q,>q is not convex.

Next, consider any concrete domain S∗ with domain Σ∗ for some finite alphabet Σ and, for every s ∈ Σ∗ , the unary predicates prefs and suffs with the semantics

Let Σ = {a1, . . . , an}. Then the S∗ -conjunction suffa1 (f) implies the disjunction prefa1 (f) ∨ . . . ∨ prefan (f) without implying any of its disjuncts.

4 Intractable extensions of EL with GCIs

In this section we consider the sublanguage EL of EL++ and restrict the attention to general TBoxes, i.e., finite sets of GCIs. Recall that EL is obtained from EL++ by dropping all concept constructors except conjunction, existential restriction, and top. We will show that the extension of EL with basically any typical DL constructor not present in EL++ results in intractability of subsumption w.r.t. general TBoxes. Syntax and semantics of the additional constructors used in this section can be found in Table 3, where #S denotes the cardinality of a set S.

In addition to the subsumption problem, we will sometimes also consider the satisfiability problem: the concept description C is satisfiable w.r.t. the general TBox T iff there exists a model I of T with CI ̸= ∅. As in the previous section, we can restrict the attention to satisfiability/subsumption of concept names w.r.t. general TBoxes.

Atomic negation

Let EL¬ be the extension of EL with negation, and let EL(¬) be obtained from EL¬ by restricting the applicability of negation to concept names (atomic negation). Since EL¬ is a notational variant of the DL ALC, EXPTIME-completeness of satisfiability and subsumption in ALC w.r.t. general TBoxes [Schild, 1991] carries over to EL¬. EXPTIME-completeness even carries over to EL(¬) since ¬C with C complex can be replaced with ¬A for a new concept name A if we add the two GCIs A ⊑ C and C ⊑ A.

Theorem 6 In EL(¬) , satisfiability and subsumption w.r.t. general TBoxes is EXPTIME-complete.

Disjunction

Let ELU be the extension of EL with disjunction. Subsumption in ELU w.r.t. general TBoxes is in EXPTIME since ELU is a fragment of ALC. To obtain a matching EXPTIME lower bound, we reduce satisfiability in EL(¬) w.r.t. general TBoxes to subsumption in ELU w.r.t. general TBoxes. To this end, let A0 be a concept name and T a general EL(¬) TBox. For each concept name A occurring in T , we take a new concept name A′ (i.e., one not occurring in T ). Also fix an additional new concept name L. Then the general TBox T ∗ is obtained from T by replacing each subconcept ¬A with A′ , and then adding the following GCIs:

• ⊤ ⊑ A⊔A′ and A⊓A′ ⊑ L for each A ∈ NC in T ;
• ∃r.L ⊑ L.

Note that ∃r.L ⊑ L is equivalent to ¬L ⊑ ∀r.¬L. It thus ensures that L acts as the bottom concept in connected countermodels of A0 ⊑T ∗ L. Using this observation, it is not hard to verify that A0 is satisfiable w.r.t. T iff A0 ̸⊑T ∗ L.

Theorem 7 In ELU, subsumption w.r.t. general TBoxes is EXPTIME-complete.

At-least restrictions

Let EL≥2 be the extension of EL with at-least restrictions of the form (⩾ 2 r). Subsumption in EL≥2 w.r.t. general TBoxes is in EXPTIME since EL≥2 is a fragment of ALC extended with number restrictions [De Giacomo and Lenzerini, 1994]. We establish a matching lower bound by reducing subsumption in ELU w.r.t. general TBoxes. Let A0 and B0 be concept names and T a general ELU TBox. Without loss of generality, we may assume that all concept inclusions in T have one of the following forms:

where C, D, C1, and C2 are concept names or ⊤. Call the resulting TBox T ∗ . To convert T into an EL≥2 CBox, we simulate each GCI C ⊑ C1 ⊔ C2 by introducing two new concept names A and B and a new role name r, and putting

It is easy to see that A0 ⊑T B0 iff A0 ⊑T ∗ B0.

Theorem 8 In EL≥2 , subsumption w.r.t. general TBoxes is EXPTIME-complete.

The interested reader may note that similar reductions can be used to show EXPTIME-completeness for EL extended with one of the role constructors negation, union, and transitive closure.

Non-p-admissible concrete domains

P-admissibility of the concrete domains is not only a sufficient condition for polynomiality of reasoning in EL++, but also a necessary one: if D is a non-convex concrete domain, then subsumption in EL(D) is EXPTIME-hard, where EL(D) is the extension of EL with the concrete domain D. The proof uses a stronger version of Theorem 7: we can show that subsumption of concept names w.r.t. restricted ELU TBoxes is EXPTIME-complete, where a restricted ELU TBox is a general EL TBox extended with a single GCI of the form A ⊑ B1 ⊔ B2 [Baader et al., 2005].

The subsumption problem for such restricted ELU TBoxes can be reduced to subsumption in EL++(D) as follows. Let A0 and B0 be concept names and T a restricted ELU TBox. Since D is not convex, there is a satisfiable conjunction c of atoms of the form p(f1, . . . , fk) that implies a disjunction a1 ∨ . . . ∨ am of such atoms, but none of its disjuncts. If we assume that this is a minimal such counterexample (i.e., m is minimal), then we also know that c does not imply a2 ∨ . . . ∨ am, and that each of the ai is satifiable. Then we have (i) each assignment of values from D that satisfies c satisfies a1 or a2∨. . .∨am; (ii) there is an assignment satisfying c and a1, but not a2∨. . .∨am; (iii) there is an assignment satisfying c and a2 ∨ . . . ∨ am but not a1. Now, let T ∗ be obtained from T by replacing the single GCI A ⊑ B ⊔ B′ by A ⊑ c, a1 ⊑ B, and ai ⊑ B′ for i = 2, . . . ,m. It is easy to see that A0 ⊑T B0 iff A0 ⊑T ∗ B0.

Theorem 9 For any non-convex concrete domain D, subsumption in EL(D) w.r.t. general TBoxes is EXPTIME-hard. For example, this theorem applies to the non-convex concrete domains introduced in Section 3.

Inverse roles

Let ELI be the extension of EL with inverse roles. We show that subsumption in ELI w.r.t. general TBoxes is PSPACEhard by reducing satisfiability in ALE w.r.t. primitive TBoxes: ALE extends EL with value restrictions and atomic negation; primitive TBoxes are finite sets of GCIs whose left-hand side is a concept name. This satisfiability problem is known to be PSPACE-complete [Calvanese, 1996].

Let A0 be a concept name and T a primitive ALE TBox. We assume without loss of generality that T contains only concept inclusions of the following forms:

where A, B, and B′ are concept names. We take a new concept name L and define the general ELI TBox T ∗ to consist of the following GCIs:

• A ⊑ D for all A ⊑ D ∈ T

if D is a concept name or of the form ∃r.B;

• ∃r-.A ⊑ B for all A ⊑ ∀r.B ∈ T ;
• A⊓B ⊑ L for all A ⊑ ¬B ∈ T ;
• ∃r.L ⊑ L.

As in the case of ELU, the concept inclusion ∃r.L ⊑ L is equivalent to ¬L ⊑ ∀r.¬L and ensures that L acts as the bottom concept in connected countermodels of A0 ⊑T ∗ L. Additionally, ∃r-.A ⊑ B is clearly equivalent to A ⊑ ∀r.B.

Thus, it is not hard to verify that A0 is satisfiable w.r.t. T iff A0 ̸⊑T ∗ L.

Theorem 10 Subsumption in ELI w.r.t. general TBoxes is PSPACE-hard.

The exact complexity of this problem is still open (the best upper bound we know of is EXPTIME, stemming from results for the DL ALCI [De Giacomo and Lenzerini, 1994]).

At-most restrictions/functional roles/FL0

Let EL≤1 be the extension of EL with at-most restrictions of the forn (⩽ 1 r). As in the case of EL≥2 , subsumption in EL≤1 w.r.t. general TBoxes is in EXPTIME since EL≤1 is a fragment of ALC with number restrictions. We prove a matching lower bound by reducing subsumption in the DL FLtf 0 w.r.t. general TBoxes. FLtf 0 offers only the concept constructors conjunction and value restriction and requires all roles to be interpreted as total functions. Subsumption in this DL w.r.t. general TBoxes was proved EXPTIME-complete in [Toman and Weddell, 2005].

Let A0 and B0 be concept names and T a general FLtf 0 TBox. We convert T into a general EL≤1 TBox T ∗ by replacing each subconcept ∀r.C with ∃r.C in GCI left-hand sides, and with (⩽ 1 r)⊓∃r.C in GCI right-hand sides. Then A0 ⊑T B0 in FLtf 0 iff A0 ⊑T ∗ B0 in EL≤1 .

Theorem 11 Subsumption in EL≤1 w.r.t. general TBoxes is EXPTIME-complete.

Interestingly, the result of Toman and Weddell can also be used to prove EXPTIME-completeness of subsumption in FL0 w.r.t. general TBoxes. Recall that FL0 is FLtf 0 without the restriction that roles be total functions. In [Baader et al., 2005] we show that A0 ⊑T B0 in FL0 iff A0 ⊑T B0 in FLtf 0 , i.e., subsumption in FL0 and FLtf 0 coincides.

Theorem 12 Subsumption in FL0 w.r.t. general TBoxes is EXPTIME-complete.

5 Conclusion

We believe that the results of this paper show that-in contrast to the negative conclusions drawn from early complexity results in the area-the quest for tractable DLs that are expressive enough to be useful in practice can be successful. Our DL EL++ is tractable even w.r.t. GCIs, and it offers many constructors that are important in ontology applications.

This is in strong contrast to its counterpart with value restrictions: FL0 is tractable without TBoxes [Brachman and Levesque, 1984], co-NP-complete for acyclic TBoxes [Nebel, 1990], PSPACE-complete for cyclic TBoxes [Baader, 1996; Kazakov and de Nivelle, 2003], and EXPTIMEcomplete for general TBoxes (as shown above, and, independently, in [Hofmann, 2005] ).