Exponential Speedup in U L Subsumption Checking Relative to General TBoxes for the Constructive Semantics Michael Mendler and Stephan Scheele Informatics Theory Group University of Bamberg, Germany {michael.mendler,stephan.scheele}@uni-bamberg.de Abstract. The complexity of the subsumption problem in description logics can vary widely with the choice of the syntactic fragment and the semantic interpretation. In this paper we show that the constructive semantics of concept descriptions, which includes the classical descriptive semantics as a special case, offers exponential speed-up in the existential- disjunctive fragment UL of ALC. 1 Introduction One of the key reasoning tasks in the application of DL formalisms is the sub- sumption problem relative to a set of terminological axioms, called a TBox. The complexity of the decision procedure depends on (i) the language fragment used for concept descriptions, (ii) the structure of the TBox, i.e., whether it is acyclic, cyclic or even permits general concept inclusions (GCIs) and finally (iii) the se- mantic interpretation of the logical operators. E.g., to deal with cyclic TBoxes the standard extensional (so-called ‘descriptive’) semantics which considers all fixed points of TBoxes has been made more intensional by restricting to greatest fixed points and least fixed points [17]. Many result have been obtained in ex- ploring the options in all these dimensions, discovering complexities all the way from PTime to NExpTime completeness. Regarding the full language ALC [5] it has been shown for the descriptive semantics that subsumption without TBox as well as with acyclic TBoxes is PSpace complete, while it is ExpTime complete for general TBoxes (see [5]). Since many applications do not need all the operators of ALC, restricted lan- guages have been considered for which lower complexity levels can be derived, even down to PTime. There seem to be two main strands among these so-called sub-boolean formalisms, the FL-type languages starting from the fragment FL0 consisting of {∀, u} and the EL-type languages which build on the operator set {∃, u}. Among these, the latter tend to be much better behaved (e.g., more effi- cient and less sensitive to extensions) than the former. For instance, it is known that subsumption checking in FL0 is PTime for empty TBoxes [14], coNP complete for acyclic TBoxes [17], while for cyclic TBoxes it is PSpace complete under the descriptive semantics [13] as well as greatest and least fixed point 2 M. Mendler, S. Scheele semantics [1] and it becomes ExpTime complete for general TBoxes (descrip- tive semantics) [12, 4]. On the other side, subsumption in EL remains in PTime for cyclic and acyclic TBoxes under all three semantics [3] and even for general descriptive TBoxes [8, 12]. There are several extensions to the EL language one can make without losing tractability, such as adding ⊥, >, nominals, concrete domains and more [6]. The addition of disjunction t, which brings back Boolean expressiveness, results in coNP hardness [8] for empty TBoxes, PSpace for acyclic and ExpTime completeness for cyclic and general TBoxes [4]. See [11] for an overview on the EL family. Presumably it is fair to assume that applications of logic-based knowledge engineering, in particular those involving mass data or real-time interaction, will tend to sacrifice expressiveness for higher performance of reasoning services. The search for tractable fragments below ALC is not only expedient from a practical perspective, it still appears there is quite some playground left to be explored. On the one hand, the existing fragments FL and EL represent only two of the four corners of the Aristotelian classification square: FL0 with {∀, u} permits us to make general statements of the form “all S are P” while EL with {∃, u} corresponds1 to “some S are P”. Less attention has been given to the so-called contraries “no S is P” and “not all S are P” which correspond to fragments {∀, t} and {∃, t}. Are these also useful as a basis in specific applications and if so what are their complexities? On the other hand, there is the semantics issue: The stan- dard descriptive semantics which follows a classical Tarskian model-theory is not the only reasonable way of interpreting concept description languages. There is the Scottian least fixed or greatest fixed point view for cyclic TBoxes introduced by Nebel [18] or the automata-theoretic interpretation of Baader [1]. Also, the concept algebras introduced by Dionne et al. [19, 10] provide alternative ways of giving intensional semantics to concept descriptions and TBoxes. Depending on application and language fragment some of these may be more appropriate than the classical descriptive semantics. The semantics issue, too, leaves room for further systematical investigations. The aim of this paper is to show that the choice of semantics can play a de- cisive role for the complexity of the subsumption problem in certain fragments of ALC. Specifically, we will show that for the {∃, t} fragment, here named UL, there is an exponential gap between the classical descriptive semantics which gives ExpTime-complete subsumption checking while for the constructive se- mantics [16] the problem lies in PTime. Like Dionne et al.’s concept algebras, the constructive interpretation is intensional but is based on a modal extension of Heyting algebras which are more general and also cover full ALC. They admit an elementary presentation using Kripke models which enrich the traditional descriptive interpretation naturally by a reflexive and transitive refinement re- lation for concept abstraction and refinement. The idea behind the constructive 1 To see this consider conjunction u as representing generic affirmative statements with > as nullary case and disjunction t as a generic refutative statement with ⊥ as the degenerated case. Of course, the refutation about t consists in giving choices, thus avoiding commitment. Constructive UL is PTIME 3 semantics [16] is that concepts must not be taken as absolute references for clearly delineated sets of object instances but as intensional descriptions that are subject to context and negotiation. This is important for situations in which knowledge is incomplete or evolving such as business auditing, where the data populating the concepts are produced in continuous streams which are poten- tially infinite. In this case role filling may involve actions that brings data into existence only at auditing time. There, the open world assumption of classical descriptions is too weak, since it is not dynamic, while the constructive semantics is robust. In [16] a number of examples are given to illustrate the issue. Showing that it turns the classically intractable problem for UL tractable further justifies the interest in the constructive semantics. 2 Constructive Semantics for ALC Concept descriptions are built from role names NR and concept names NC as follows C, D ::= A | > | ⊥ | ¬C | C u D | C t D | C v D | ∃R.C | ∀R.C, where A ∈ NC and R ∈ NR . This syntax is more general than standard ALC in that it includes subsumption v as a concept–forming operator. The fact that v can be nested will be irrelevant for the purposes of this paper. Still, we present the constructive semantics for the full system: Definition 1 ([16]). A constructive interpretation of ALC is a structure I = (∆I , I , ⊥I , ·I ) consisting of – a non-empty set ∆I of entities; – a refinement pre-ordering I on ∆I (reflexive and transitive); – a subset ⊥I ⊆ ∆I of fallible entities closed under refinement and role filling, i.e., x ∈ ⊥I and x I y or xRI y implies y ∈ ⊥I for all R ∈ NR ; also x ∈ ⊥I means that for all R ∈ NR there exists y ∈ ∆I such that xRI y; – finally an interpretation function ·I mapping each role name R ∈ NR to a binary relation RI ⊆ ∆I × ∆I and each concept name A ∈ NC to a set ⊥I ⊆ AI ⊆ ∆I which is closed under refinement, i.e., x ∈ AI and x I y implies y ∈ AI . I is lifted from constant ⊥ and concept names A to arbitrary concepts as seen below, where ∆Ic =df ∆I \ ⊥I is the set of non-fallible elements in I: >I =df ∆I (¬C)I =df {x | ∀y ∈ ∆Ic . x I y ⇒ y 6∈ C I } (C u D)I =df C I ∩ DI (C t D)I =df C I ∪ DI (C v D)I =df {x | ∀y ∈ ∆Ic . (x I y & y ∈ C I ) ⇒ y ∈ DI } (∃R.C)I =df {x | ∀y ∈ ∆Ic . x I y ⇒ ∃z ∈ ∆I . (y, z) ∈ RI & z ∈ C I } (∀R.C)I =df {x | ∀y ∈ ∆Ic . x I y ⇒ ∀z ∈ ∆I . (y, z) ∈ RI ⇒ z ∈ C I }. 4 M. Mendler, S. Scheele Entities in ∆I are partial descriptions representing incomplete information about individuals. Read a  b as saying that b “is a refinement of ” a. The differ- ence to the classical descriptive semantics is the refinement dimension I and the universal quantification ∀y ∈ ∆Ic . x I y ⇒ . . . in the clauses of Definition 1. If I trivialises to the identity relation, i.e., each entity refines only itself, and if ⊥I = ∅, then the constructive semantics coincides with the classical descriptive semantics of ALC. Therefore, the constructive semantics includes the classical one. Let cALC be ALC under the constructive interpretation. Then cALC is re- lated to the constructive modal logic CK (Constructive K) [20, 7, 15] as ALC is related to the classical modal system K [9]. In cALC the classical principles of the Excluded Middle C t ¬C ≡ >, Double Negation ¬¬C ≡ C, the dualities ∃R.C ≡ ¬∀R.¬C, ∀R.C ≡ ¬∃R.¬C and Disjunctive Distribution ∃R.(C t D) ≡ ∃R.C t∃R.D are no longer tautologies but non-trivial TBox statements (cf. [16]). In particular, consider Disjunctive Distribution: Imagine a dynamic data model so that role filling for R is a process which involves accessing a remote data base. Then role filling is a computation which interacts with the environment to access/generate the data. In this case the disjunctive decision C t D can only be made once the (R-filler) context to access the data has been established. This means that the data model may well guarantee ∃R.(C t D), yet it would be rather strong to assume it also satisfies ∃R.C t ∃R.D where the decision is outside the scope of R and thus available before the R-filler is even requested. Before we can embark on the main technical developments we need to intro- duce some pieces of notation. First, it will be convenient (to save indices) to use a semantic validity relation |= as follows: Write I; x |= C to abbreviate x ∈ C I in which case we say that entity x satisfies concept C in the interpretation I. Further, I is a model of C, written I |= C iff ∀x ∈ ∆I . I; x |= C. All uses of |= are extended to sets Φ of concepts, I; x |= Φ, I |= Φ in the usual universal fashion. Let Θ be a set of TBox axioms, and Γ a set of concept descriptions. We write Θ; Γ |= C if for all models I of Θ it is the case that every entity x ∈ ∆I which satisfies all axioms in Γ must also satisfy concept C. Formally, ∀I.∀x ∈ ∆I . (I |= Θ & I; x |= Γ ) ⇒ I; x |= C. The reasoning task which we are interested in here is subsumption in the presence of TBox axioms: The statement Θ; {C} |= D expresses that concept C is subsumed by concept D in the presence of terminology Θ, i.e., for all models I |= Θ we have C I ⊆ DI ; Unlike in the classical semantics of ALC, we cannot reduce subsumption to non-satisfiability since Θ; {C, ¬D} |= ⊥ is not the same as Θ; {C} |= D. For convenience, the latter will be written Θ; C |= D saving the braces. Note that subsumption is defined relative to all constructive models. If we wish to restrict to the classical models we write Θ; C |=cl D, meaning that for all classical models I |= Θ we have C I ⊆ DI . In the following we will consider TBoxes Θ which consist entirely of subsump- tions C v D such that both C, D are v-free. These are usually called general TBoxes. We will investigate subsumption checking relative to general TBoxes for the existential-disjunctive fragment of ALC, called UL. This is the class of Constructive UL is PTIME 5 concept descriptions formed as C, D :: = > | ⊥ | A | C t D | ∃R.C with A ∈ NC and R ∈ NR . Notice that in this fragment we can have uncon- ditional negative and positive axioms C and ¬C included in TBoxes, viz. as subsumptions C v ⊥ and > v C. The PTime result will hold for the guarded fragment of UL. A concept description C is (existentially) guarded if it is not a disjunction, or equivalently, if all disjunctions appearing in C are guarded behind existential quantifiers. A general UL TBox Θ is called (existentially) guarded if in every C v D ∈ Θ the conclusion D is guarded. 3 Guarded U L0 is ExpTime hard for Classical Descriptive Semantics We reduce subsumption in the language FL0 consisting of operators {∀, u} to subsumption in UL under classical descriptive semantics. In fact, we will reduce subsumption in FL0 to the fragment UL0 , which is UL without the constants >, ⊥, and relative to guarded UL0 TBoxes. Let Θ be a general TBox in FL0 and C, D two FL0 concept descriptions. For simplicity we assume that NC contains exactly the concept names appearing in Θ or C, D. The first step in our re- duction dualises the problem under the classical descriptive semantics, replacing u 7→ t and ∀ 7→ ∃ and swapping left and right-hand sides of subsumptions. For- mally, define the dual d (C) of a FL0 concept description recursively as follows: d (A) =df A, d (C u D) =df d (C) t d (D), d (∀R.C) =df ∃R.d (C). Further, the dual of the TBox is d (Θ) =df {d (D) v d (C) | C v D ∈ Θ}. Then, one shows Θ; C |=cl D ⇐⇒ d (Θ); d (D) |=cl d (C). Obviously, the dualised FL0 concepts d (D), d (C) are now UL0 expressions and d (Θ) is a general TBox of UL0 . d (Θ) need not be existentially guarded, though. However, this can be fixed.We intro- duce a new role τ to guard the TBox inclusions making sure that the effect of τ can be compensated for by choosing the right classical interpretations. Given an UL0 TBox Θ we define its expansion exp(Θ) =df {C v ∃τ.D | C v D ∈ Θ} ∪ { ∃R.X v ∃τ.∃R.X, ∃τ.∃R.X v ∃R.X | ∃R.X ∈ Sf(Θ)} ∪ {A v ∃τ.A, ∃τ.A v A | A ∈ NC }, where Sf(Θ) denotes the set of sub-concepts of Θ. Clearly, all subsumptions in exp(Θ) are guarded. Because of the additional axioms, the new role τ is semantically “silent” and does not add any information. Observing Θ; C |=cl D iff exp(Θ); C |=cl D, classical subsumption checking for Θ in FL0 is now reduced to exp(Θ) in guarded UL0 : Lemma 1. Let C, D be FL0 concept descriptions and Θ a general TBox of FL0 . Then, Θ; C |=cl D iff exp(d (Θ)); d (D) |=cl d (C). 6 M. Mendler, S. Scheele Lemma 1 gives a linear-time reduction of the FL0 problem to that in UL0 , where the simulating TBox exp(d (Θ)) is existentially guarded. Since subsump- tion checking in FL0 for general TBoxes and classical descriptive semantics is ExpTime hard [12, 4] we have the following theorem: Theorem 1. UL0 subsumption checking under the classical semantics and rel- ative to existentially guarded (general) TBoxes is ExpTime hard. It is important to realise that the reduction behind Thm. 1 depends crucially on the classical nature of the semantics, the DeMorgan dualities and the exis- tential distribution |=cl ∃R.(C t D) ≡ (∃R.C t ∃R.D). As has been pointed out by Hofmann [12] the presence and absence of such distributive laws can make the difference between ExpTime and PTime complexity. In ExpTime FL0 the operators {u, ∀} distribute while in the PTime fragment {u, ∃} [2, 12] they do not. 4 Guarded U L is in PTime for Constructive Descriptive Semantics In the following we will show that subsumption checking in UL under the con- structive semantics and relative to existentially guarded TBoxes is in PTime. We obtain a PTime decision procedure for UL by the calculus presented in Fig. 1. The calculus is formulated in the style of Gentzen with left introduction rules tL, vL, ∃LR, ⊥L and right introduction rules tR1 , tR2 , ∃LR, >R for each logical connective of UL. We will show that the calculus is sound and complete for UL under the constructive semantics. Let I be a constructive interpretation and a ∈ ∆I an entity in I. We say that the pair (I, a) satisfies a sequent Θ; C ` D if I is a model of Θ, i.e., I |= Θ, and I; a |= C as well as I; a 6|= D. A sequent Θ; C ` D is (constructively) satisfiable, iff there exists (I, a) which satisfies the sequent. This is equivalent to non-subsumption Θ; C 6|= D (see page 4). Completeness of the calculus of Fig. 1 means that if no proof can be found for Θ; C ` D then the sequent is satisfiable. Soundness means that whenever Θ; C ` D is derivable then Θ; C |= D, i.e. C is subsumed by D. While soundness is easy to establish completeness requires a number of auxiliary tools which we introduce next. Definition 2. A concept description P is called (constructively) prime in a TBox Θ if for all D1 , D2 ∈ Sf(Θ) ∪ Sf(P ), whenever Θ; P |= D1 t D2 then Θ; P |= D1 or Θ; P |= D2 . The trouble for the classical semantics is that TBoxes have only very few if any prime concepts. Instead, the TBox must be saturated by adding and manipulating instances in terms of sets of concepts. Such sets of concepts are needed to pin down a hypothetical individual sufficiently for going through all the case analyses needed to decide a given subsumption in the context of Θ. On the other hand, constructive TBoxes have more prime elements, i.e., single concept Constructive UL is PTIME 7 Ax ⊥L >R Θ; C ` C Θ; ⊥ ` C Θ; C ` > Θ; E ` C Θ; E ` D Θ; C ` F Θ; D ` F tR1 tR2 tL Θ; E ` C t D Θ; E ` C t D Θ; C t D ` F Θ; E ` C Θ; D ` F Θ; C ` D vL ∃LR Θ, C v D; E ` F Θ; ∃R.C ` ∃R.D Fig. 1. Gentzen sequent rules for UL. descriptions which are able to capture a whole set of individuals completely. The striking feature of constructive ALC is that existential concepts are always constructively prime for the empty TBox. Proposition 1. Every existentially guarded UL concept description C is con- structively prime for the empty TBox. Proof. By induction on the structure of C and the definition of |= for the con- structive semantics (see page 4). t u Proposition 1 is the reason why for existentially guarded UL the constructive calculus for ALC [16] can be restricted to the simple form of sequents Θ; C ` D manipulated in Fig. 1 without losing completeness. The following Props. 2 and 3 will be instrumental for proving this. Proposition 2 (Cut Admissibility). In the proof system of Fig. 1 the cut rule is admissible, i.e., if Θ; C ` D and Θ; D ` E then Θ; C ` E. Proof. Given derivations for Θ; C ` D and for Θ; D ` E we show Θ; C ` E by induction on the derivations and the cut formula D. t u Proposition 3 (Provable Primes). Let Θ be an existentially guarded TBox and P, C1 , C2 concept descriptions. If P is existentially guarded then Θ; P ` C1 t C2 implies Θ; P ` C1 or Θ; P ` C2 . Proof. We proceed by induction on the derivation for Θ; P ` D1 t D2 . Since P is not a disjunction, the last rule in this derivation cannot be Ax , tL, ∃LR or >R. If the last rule is ⊥L or one of tR1 , tR2 the claim follows immediately. The only interesting case is when the derivation ends in an application of vL, i.e., it looks like .. .. . π1 . π2 Θ; P ` E Θ; F ` D1 t D2 vL Θ, E v F ; P ` D1 t D2 By assumption on our TBox from which E v F is drawn, F is guarded. Hence we may invoke the induction hypothesis on the sub-derivation π2 . This gives a 8 M. Mendler, S. Scheele derivation π20 for Θ; F ` Di for some i = 1, 2, from which we get .. .. 0 . π1 . π2 Θ; P ` E Θ; F ` Di vL Θ, E v F ; P ` Di as desired. t u The next observation we need to make is that all concept descriptions in a UL TBox Θ can be decomposed and fully covered by the guarded elements of Sf(Θ). Define a relation C D P iff P is a (maximal) guarded sub-expression of C. If C is guarded then C D C. Otherwise, C = C1 t C2 is a disjunction and one of Ci must contain the guarded sub-expression P . Lemma 2 (Coverings). Let C be a concept description in UL and Θ a TBox. Then, (i) If C D P and Θ; C ` E then Θ; P ` E (ii) If Θ; P ` E for all C D P then Θ; C ` E. Proof. (i) The proof depends on cut admissibility and the fact that if C D P then Θ; P ` C. This can be proved easily by induction on C. (ii) Again, this is by induction on the structure of C. For constants >, ⊥, concept names and existentials the statement is trivial, since for these C D C. For disjunctions we notice that C1 t C2 D P iff C1 D P or C2 D P . Hence, if Θ; P ` E for all C1 t C2 D P we have Θ; Ci ` E for both i = 1, 2 by induction hypothesis and thus Θ; C1 t C2 ` E by way of rule tL. t u From now on we will assume that the UL TBox Θ is existentially guarded. We build a constructive interpretation I based on guarded concept descriptions by letting ∆I consist of the set of pairs (C, ΨC ) where C is guarded and ΨC is a finite map associating with each role R ∈ NR a set ΨC (R) ⊆ Sf(Θ) of concept de- scriptions such that the formal (intensional) consistency requirementF Θ; C 6` ΨC holds. This consistency condition is an abbreviation for Θ; C 6` ∃R. X∈ΨC (R) X for all R ∈ NR such that ΨC (R) 6= ∅. The guarded concept description C in a pair (C, ΨC ) records the extensional information characterising the entity repre- sented by (C, ΨC ) while the second component ΨC encodes additional intensional information. Each entry X ∈ ΨC (R) specifies the R-fillers in the sense that every entity consistent with the concepts in ΨC (R) will be an R-filler of (C, ΨC ). In our case we can further restrict the structure to ΨC = ∅ or ΨC = [R 7→ X], i.e. ΨC (R) = ∅ for all R ∈ NR or for exactly one R ∈ NR we have ΨC (R) = {X}, respectively. Note that the pair (C, ∅) is always consistent regardless of C and that (C, [R 7→ X]) is consistent iff Θ; C 6` ∃R.X. Constructive UL is PTIME 9 The canonical model I is given by an interpretation of concept names, filler and refinement relations RI and I on I, respectively, as follows: (C, ΨC ) ∈ AI ⇐⇒ Θ; C ` A (C, ΨC ) ∈ ⊥I ⇐⇒ Θ; C ` ⊥ (C, ΨC ) RI (D, ΨD ) ⇐⇒ ∀X ∈ ΨC (R). Θ; D 6` X (C, ΨC ) I (D, ΨD ) ⇐⇒ Θ; D ` C. Observe that the constructive semantics distinguishes between two kinds of con- sistencies, viz. extensional consistency, if (C, ΨC ) 6∈ ⊥I and intensional consis- tency, if Θ; C 6` ΨC . Our canonical I contains only intensionally consistent ob- jects, though they may be extensionally inconsistent. In such an entity (C, ΨC ) ∈ ⊥I we must necessarily have ΨC (R) = ∅ for all R ∈ NR . For if ΨC (R) = {X} for some R and X then Θ; ⊥ ` ∃R.X by rule ⊥L which by the assumption Θ; C ` ⊥ and cut admissibility would yield Θ; C ` ∃R.X in contradiction to intensional consistency of (C, ΨC ). But ΨC (R) = ∅ means the entity (C, ΨC ) does not ex- clude any R-fillers, i.e. (C, ΨC ) RI (D, ΨD ) for every intensionally consistent pair (D, ΨD ). Notice again that every pair (C, ∅) is intensionally consistent and thus an object in I. Clearly, I is reflexive because of rule Ax and transitive because of cut ad- missibility Prop. 2. It is not antisymmetric, though, due to the slack in the second component ΨD which has no influence on I . In fact, it contains cycles since, e.g., (C, ΨC ) I (C, ∅) and also (C, ∅) I (C, ΨC ) for all ΨC . Truth valuations ⊥I and AI are closed under I due to cut admissibility. Extensionally inconsis- tent objects ⊥I partake in all UL concept descriptions, i.e., for all UL concepts, ⊥I ⊆ C I . Thus, I is a constructive model according to Def. 12 . Lemma 3. Let Θ be an existentially guarded TBox and E an arbitrary UL concept description. Then, for every (C, ΨC ) ∈ I, we have I; (C, ΨC ) |= E iff Θ; C ` E. Proof. We proceed by induction on E. For concept names and ⊥ the statement follows directly from the definition of AI . For > we need to use rule >R. The interesting cases are existentials and disjunction: Let (C, ΨC ) ∈ I and suppose Θ; C 6` ∃R.E, which in particular implies Θ; C 6` ⊥ by cut admissibility and ⊥L. Then the pair (C, [R 7→ E]) is intensionally and extensionally consistent. The latter follows from Θ; C 6` ⊥ and the former from Θ; C 6` ∃R.E. Thus, (C, [R 7→ E]) is an entity in I and also (C, [R 7→ E]) I (C, [R 7→ E]) with (C, [R 7→ E]) ∈ ∆Ic = ∆I \⊥I . Consider any R-filler (C, [R 7→ E]) RI (D, ΨD ) which must satisfy Θ; D 6` E by definition. Now we use the in- duction hypothesis to infer I; (D, ΨD ) 6|= E which proves I; (C, ΨC ) 6|= ∃R.E according to Def. 1, all in all. Vice versa, suppose that Θ; C ` ∃R.E and let (C, ΨC ) I (D, ΨD ) ∈ ∆Ic be given arbitrarily, which means Θ; D ` C and by 2 To be fully compatible also with the constructive semantics of ¬, ∀R we should also make sure that all R-fillers of objects in ⊥I are themselves extensionally inconsistent. This is not needed for the existential-disjunctive fragment at hand. 10 M. Mendler, S. Scheele cut admissibility Θ; D ` ∃R.E. We claim that there exists a guarded compo- nent P of E such that (P, ∅) is an R-filler of (D, ΨD ). If ΨD (R) = ∅ we can take any guarded E D P and have (D, ΨD ) RI (P, ∅) for trivial reasons. Oth- erwise, if ΨD (R) = {X} we must find a guarded component P of E such that Θ; P 6` X. We proceed by contradiction. Suppose, Θ; P ` X for every P with E D P . By Lem. 2 (ii) this implies Θ; E ` X. From there, an application of ∃LR gives Θ; ∃R.E ` ∃R.X and further cut admissibility Θ; D ` ∃R.X which would contradict consistency of (D, ΨD ). Thus, as claimed, (D, ΨD ) RI (P, ∅) for some guarded component P of E. By Lem. 2 (i) we have Θ; P ` E from which the induction hypothesis tells us that I; (P, ∅) |= E which completes the proof that I; (C, ΨC ) |= ∃R.E according to Def. 1. Now assume I; (C, ΨC ) |= E1 tE2 , i.e., I; (C, ΨC ) |= Ei for some i = 1, 2. The induction hypothesis obtains Θ; C ` Ei and thus Θ; C ` E1 t E2 by virtue of rule tR1 (for i = 1) or tR2 (for i = 2). In the other direction, given Θ; C ` E1 t E2 , we get Θ; C ` E1 or Θ; C ` E2 based on the fact that C is guarded (Prop. 3). In either case we can use the induction hypothesis to conclude I; (C, ΨC ) |= Ei from which I; (C, ΨC ) |= E1 t E2 follows as required. t u Lemma 3 means that I is a constructive model of the TBox Θ. To see this let F v E ∈ Θ and (C, ΨC ) I (D, ΨD ) such that I; (D, ΨD ) |= F . Therefore, Θ; D ` F because of Lem. 3. From here we get Θ; D ` E by way of rules vL and Ax , which implies I; (D, ΨD ) |= E by Lem. 3. Hence, overall, I; (C, ΨC ) |= F v E. Proposition 4. The rules in Fig. 1 are sound for constructive subsumption in UL and complete relative to existentially guarded (general) TBoxes Θ. Proof. Soundness, viz. that Θ; C ` D implies Θ; C |= D, is proved by induc- tion on derivations. Regarding completeness, let a subsumption Θ; C |= D be constructively valid. Consider the canonical model I constructed above which satisfies I |= Θ. Take any guarded component C D P of C. By Lem. 2 (i) and rule Ax we have Θ; P ` C. Hence, I; (P, ∅) |= C because of Lem. 3. But then the assumption Θ; C |= D implies I; (P, ∅) |= D which means Θ; P ` D again by Lem. 3. Since P with C D P was arbitrary we have shown that Θ; C ` D by virtue of Lem. 2 (ii). t u Theorem 2. Subsumption checking in UL under the constructive semantics and relative to existentially guarded (general) TBoxes is in PTime. Proof. Let Θ be an existential TBox and C and D concept descriptions in UL. We want to decide the subsumption C v D relative to Θ. Due to Prop. 4 we can decide Θ; C |= D by proof search in the calculus of Fig. 1. Because of the sub-formula property each possible node in a derivation tree is determined by a pair of concept descriptions in Sf(Θ ∪ {C, D}). Thus the number of possible nodes in a tree is at worst quadratic in the size of Θ. We may systematically tabulate all pairs (X, Y ) ∈ Sf(Θ ∪ {C, D})2 such that Θ; X ` Y using dynamic programming memorisation techniques and thus decide any fixed subsumption in polynomial time. t u Constructive UL is PTIME 11 5 Conclusion and Future Work This paper highlights the dramatic effect that the choice of semantic interpreta- tion can have on the complexity of reasoning in DL. Arguably, as long as there is no application domain identifiable for the UL fragment these results may only have theoretical interest. Perhaps our results can be extended to more expres- sive DLs that may eventually support practical applications. Note that from the expressiveness point of view the constructive semantics genuinely enriches the classical descriptive interpretation, so that the low complexity of UL is some- what unexpected. However, as discussed in [16], the constructive semantics has useful applications which are independent of this complexity result. We can see some immediate ways to generalise our results. The main results carry over to all TBoxes in which every C ∈ Sf(Θ) has a non-empty prime cover Cov(C) ⊆ Sf(Θ) satisfying the conditions of Prop. 3 and Lem. 2. We have ex- ploited this here for guarded TBoxes in the UL language where every concept has a prime cover. We conjecture that the PTime result extends directly to UL− which is UL plus limited universal quantification ∀R.⊥. For other extensions like (i) permitting negated atoms ¬A, (ii) adding conjunctions u we expect coNP hardness, but hopefully not more since the Boolean reasoning should remain safely contained between the levels of existentials so that the Boolean combi- natorics does not spill over quantifiers (exploiting that in constructive logic ∀¬ is not the same as ¬∃, etc.). One of our referees has pointed out that if we remove the guardedness restriction then we could express Disjunctive Distribu- tion in the TBox which suggests that complexity might rise to ExpTime. Since we apply constructive rather than classical semantics it is not clear whether such Disjunctive Distribution in TBoxes necessarily lead to exponentially large TBoxes/derivations or they can be eliminated in terms of an exponential number of polynomially sized TBoxes. We leave these investigations to future work. Finally, it is worthwhile to add that the dualising reduction from FL0 to UL0 used in Section 3 can also be applied to axiomatic (cyclic or non-cyclic) TBoxes so that several other complexity results for the classical descriptive semantics should follow in a similar fashion. E.g., all the hardness/completeness results for EL (see, e.g., [11]) should carry over to the “no S is P” fragment {∀, t} under the classical semantics. Similarly, coNP-hardness for FL0 in acyclic TBoxes should imply coNP-hardness for UL0 , PSpace-hardness of FL0 should give PSpace-hardness of UL0 in cyclic TBoxes. Of course, this applies to the classical descriptive semantics. For the constructive semantics the situation is open since DeMorgan-style dualisation does not work. Acknowledgements This work has been funded by the German Research Council (DFG) under ME 1427/4-1. The authors would like to thank the anony- mous reviewers for their suggestions to improve the presentation of this paper. 12 M. Mendler, S. Scheele References 1. F. Baader. Using automata theory for characterizing the semantics of terminolog- ical cycles. Annals of Math. and Artificial Intelligence, pages 175–219, 1996. 2. F. Baader. Computing the least common subsumer in the description logic EL w.r.t. terminological cycles with descriptive semantics. In Proc. Int’l Conf. on Conceptual Structures (ICCS2003), pages 117–130. Springer LNAI 2746, 2003. 3. F. Baader. Terminological cycles in a description logic with existential restrictions. In Proc. 18th Int’l Joint Conf. on Artificial Intelligence, pages 325–330. Morgan Kaufmann, 2003. 4. F. Baader, S. Brandt, and C. Lutz. Pushing the EL-envelope. In Proc. 19th Joint Conf. on Artificial Intelligence (IJCAI 2005), pages 364–369, 2005. 5. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. Patel-Schneider, edi- tors. The Description Logic Handbook: Theory, Implementations and Applications. Cambridge University Press, 2003. 6. Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope further. In Kendall Clark and Peter F. Patel-Schneider, editors, In Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions, 2008. 7. G. Bellin, V. de Paiva, and E. Ritter. Extended Curry-Howard correspondence for a basic constructive modal logic. In Methods for Modalities II, November 2001. 8. S. Brandt. Polynomial time reasoning in a description logic with existential re- strictions, GCI axioms, and – what else? In R. López de Mantáras and L. Saitta, editors, Proc. Eur. Conf. on Artificial Intelligence (ECAI-2004), pages 298–302, 2004. 9. V. de Paiva. Constructive description logics: what, why and how. In Context Representation and Reasoning, Riva del Garda, August 2006. 10. R. Dionne, E. Mays, and F. J. Oles. The equivalence of model-theoretic and structural subsumption in description logics. In Proc. 13th Int’l Joint Conf. on Artificial Intelligence (IJCAI’93), pages 710–718, 1993. 11. Ch. Haase and C. Lutz. Complexity of subsumption in the EL family of description logics: acyclic and cyclic TBoxes. In Proc. Europ. Conf. on Artificial Intelligence ECAI 2008, 2008. 12. M. Hofmann. Proof-theoretic approach to description-logic. In Proc. Logic in Computer Science LICS 2005, 2005. 13. Y. Kazakov and H. de Nivelle. Subsumption of concepts in FL0 for (cyclic) termi- nologies with respect to descriptive semantics is PSPACE complete. In Proc. Int’l Workshop Description Logics (DL 2003), volume 81 of CEUR Electronic workshop proceedings, 2003. 14. H. J. Levesque and R. J. Brachman. Expressiveness and tractability in knowledge representation and reasoning. Computational Intelligence, 3:78–93, 1897. 15. M. Mendler and V. de Paiva. Constructive CK for contexts. In L. Serafini and P. Bouquet, editors, Context Representation and Reasoning (CRR-2005), vol- ume 13 of CEUR Proceedings, July 2005. Also presented at the Association for Symbolic Logic Annual Meeting, Stanford University, USA, 22nd March 2005. 16. M. Mendler and S. Scheele. Towards constructive description logics for abstraction and refinement. In 21st Int’l Workshop on Description Logics (DL2008). CEUR Workshop proceedings 353, May 2008. 17. B. Nebel. Terminological reasoning is inherently intractable. Artificial Intelligence, pages 235–249, 1990. Constructive UL is PTIME 13 18. B. Nebel. Terminological cycles: Semantics and computational properties. In J. F. Sowa, editor, Principles of Semantic Networks. Morgan Kaufmann, 1991. 19. F. J. Oles R. Dionne, E. Mays. A non-well-founded approach to terminological cycles. In Proc. 10th Nat’l Conf. of the Americ. Assoc. for Artificial Intelligence (AAAI’92), 1992. 20. D. Wijesekera. Constructive modal logic I. Annals of Pure and Applied Logic, 50:271–301, 1990.