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, o ers exponential speed-up in the existentialdisjunctive fragment U L of ALC.
One of the key reasoning tasks in the application of DL formalisms is the
subsumption 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 nally (iii) the
semantic interpretation of the logical operators. E.g., to deal with cyclic TBoxes
the standard extensional (so-called `descriptive') semantics which considers all
xed points of TBoxes has been made more intensional by restricting to greatest
xed points and least xed points [
Regarding the full language ALC [
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 sacri ce 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 F L and E L represent only two of the
four corners of the Aristotelian classi cation square: F L0 with f8; ug permits
us to make general statements of the form \all S are P" while E L with f9; ug
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 f8; tg
and f9; tg. Are these also useful as a basis in speci c applications and if so what
are their complexities? On the other hand, there is the semantics issue: The
standard 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 xed or greatest xed point view for cyclic TBoxes introduced
by Nebel [
The aim of this paper is to show that the choice of semantics can play a
decisive role for the complexity of the subsumption problem in certain fragments
of ALC. Speci cally, we will show that for the f9; tg fragment, here named U L,
there is an exponential gap between the classical descriptive semantics which
gives ExpTime-complete subsumption checking while for the constructive
semantics [
Concept descriptions are built from role names NR and concept names NC as follows
C; D ::= A j > j ? j :C j C u D j C t D j C v D j 9R:C j 8R:C;
where A 2 NC and R 2 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:
De nition 1 ([
I is lifted from constant ? and concept names A to arbitrary concepts as seen below, where cI =df I n ?I is the set of non-fallible elements in I: >I =df I (:C)I =df fx j 8y 2 (C u D)I =df CI \ DI (C t D)I =df CI [ DI (C v D)I =df fx j 8y 2 (9R:C)I =df fx j 8y 2 (8R:C)I =df fx j 8y 2 cI : x
I y ) y 62 CI g cI : (x cI : x cI : x
I y & y 2 CI ) ) y 2 DI g I y ) 9z 2 I : (y; z) 2 RI & z 2 CI g
I y ) 8z 2 I : (y; z) 2 RI ) z 2 CI g:
Entities in I are partial descriptions representing incomplete information about individuals. Read a b as saying that b \is a re nement of " a. The di erence to the classical descriptive semantics is the re nement dimension I and the universal quanti cation 8y 2 cI : x I y ) : : : in the clauses of De nition 1.
If I trivialises to the identity relation, i.e., each entity re nes 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
related to the constructive modal logic CK (Constructive K) [
Before we can embark on the main technical developments we need to introduce some pieces of notation. First, it will be convenient (to save indices) to use a semantic validity relation j= as follows: Write I; x j= C to abbreviate x 2 CI in which case we say that entity x satis es concept C in the interpretation I. Further, I is a model of C, written I j= C i 8x 2 I : I; x j= C. All uses of j= are extended to sets of concepts, I; x j= , I j= in the usual universal fashion. Let be a set of TBox axioms, and a set of concept descriptions. We write ; j= C if for all models I of it is the case that every entity x 2 I which satis es all axioms in must also satisfy concept C. Formally, 8I:8x 2 I : (I j= & I; x j= ) ) I; x j= C. The reasoning task which we are interested in here is subsumption in the presence of TBox axioms: The statement ; fCg j= D expresses that concept C is subsumed by concept D in the presence of terminology , i.e., for all models I j= we have CI DI ; Unlike in the classical semantics of ALC, we cannot reduce subsumption to non-satis ability since ; fC; :Dg j= ? is not the same as ; fCg j= D. For convenience, the latter will be written ; C j= D saving the braces. Note that subsumption is de ned relative to all constructive models. If we wish to restrict to the classical models we write ; C j=cl D, meaning that for all classical models I j= we have CI DI .
In the following we will consider TBoxes which consist entirely of subsumptions 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 U L. This is the class of Constructive UL is PTIME concept descriptions formed as
C; D :: = > j ? j A j C t D j 9R:C with A 2 NC and R 2 NR. Notice that in this fragment we can have unconditional 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 U L. 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 quanti ers. A general U L TBox is called (existentially) guarded if in every C v D 2 the conclusion D is guarded. 3
We reduce subsumption in the language F L0 consisting of operators f8; ug to subsumption in U L under classical descriptive semantics. In fact, we will reduce subsumption in F L0 to the fragment U L0, which is U L without the constants >; ?, and relative to guarded U L0 TBoxes. Let be a general TBox in F L0 and C, D two F L0 concept descriptions. For simplicity we assume that NC contains exactly the concept names appearing in or C; D. The rst step in our reduction dualises the problem under the classical descriptive semantics, replacing u 7! t and 8 7! 9 and swapping left and right-hand sides of subsumptions. Formally, de ne the dual d (C) of a F L0 concept description recursively as follows: d (A) =df A, d (C u D) =df d (C) t d (D), d (8R:C) =df 9R:d (C). Further, the dual of the TBox is d ( ) =df fd (D) v d (C) j C v D 2 g. Then, one shows ; C j=cl D () d ( ); d (D) j=cl d (C): Obviously, the dualised F L0 concepts d (D); d (C) are now U L0 expressions and d ( ) is a general TBox of U L0. d ( ) need not be existentially guarded, though. However, this can be xed.We introduce a new role to guard the TBox inclusions making sure that the e ect of can be compensated for by choosing the right classical interpretations. Given an U L0 TBox we de ne its expansion exp( ) =df fC v 9 :D j C v D 2 g [ f 9R:X v 9 :9R:X; 9 :9R:X v 9R:X j 9R:X 2 Sf( )g
[ fA v 9 :A; 9 :A v A j A 2 NC g; 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 j=cl D i exp( ); C j=cl D, classical subsumption checking for in F L0 is now reduced to exp( ) in guarded U L0: Lemma 1. Let C; D be F L0 concept descriptions and Then, ; C j=cl D i exp(d ( )); d (D) j=cl d (C). a general TBox of F L0.
Lemma 1 gives a linear-time reduction of the F L0 problem to that in U L0,
where the simulating TBox exp(d ( )) is existentially guarded. Since
subsumption checking in F L0 for general TBoxes and classical descriptive semantics 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
existential distribution j=cl 9R:(C t D) (9R:C t 9R:D). As has been pointed out
by Hofmann [
In the following we will show that subsumption checking in U L under the constructive semantics and relative to existentially guarded TBoxes is in PTime. We obtain a PTime decision procedure for U L by the calculus presented in Fig. 1. The calculus is formulated in the style of Gentzen with left introduction rules tL, vL, 9LR, ?L and right introduction rules tR1, tR2, 9LR, >R for each logical connective of U L. We will show that the calculus is sound and complete for U L under the constructive semantics.
Let I be a constructive interpretation and a 2 I an entity in I. We say that the pair (I; a) satis es a sequent ; C ` D if I is a model of , i.e., I j= , and I; a j= C as well as I; a 6j= D. A sequent ; C ` D is (constructively) satis able, i there exists (I; a) which satis es the sequent. This is equivalent to non-subsumption ; C 6j= 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 satis able. Soundness means that whenever ; C ` D is derivable then ; C j= 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.
De nition 2. A concept description P is called (constructively) prime in a TBox if for all D1; D2 2 Sf( ) [ Sf(P ), whenever ; P j= D1 t D2 then ; P j= D1 or ; P j= 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 su ciently 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
?L ; E ` D ; E ` C t D tR2 ; C ` >
>R ; C ` F ; D ` F ; C t D ` F tL ; E ` C ; D ` F ; C v D; E ` F vL
; C ` D ; 9R:C ` 9R:D 9LR 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 U L concept description C is constructively prime for the empty TBox.
Proof. By induction on the structure of C and the de nition of j= for the constructive semantics (see page 4). tu
Proposition 1 is the reason why for existentially guarded U L the constructive
calculus for ALC [
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 induction on the derivations and the cut formula D. ; C ` E by tu 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, 9LR 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 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 derivation 20 for ; F ` Di for some i = 1; 2, from which we get
The next observation we need to make is that all concept descriptions in a U L TBox can be decomposed and fully covered by the guarded elements of Sf( ). De ne a relation C D P i 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 U L and Then, a TBox. (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 i 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. tu
From now on we will assume that the U L 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 nite map associating with each role R 2 NR a set C (R) Sf( ) of concept descriptions such that the formal (intensional) consistency requirement ; C 6` C holds. This consistency condition is an abbreviation for ; C 6` 9R: FX2 C(R) X for all R 2 NR such that C (R) 6= ;. The guarded concept description C in a pair (C; C ) records the extensional information characterising the entity represented by (C; C ) while the second component C encodes additional intensional information. Each entry X 2 C (R) speci es the R- llers in the sense that every entity consistent with the concepts in C (R) will be an R- ller 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 2 NR or for exactly one R 2 NR we have C (R) = fXg, respectively. Note that the pair (C; ;) is always consistent regardless of C and that (C; [R 7! X]) is consistent i ; C 6` 9R:X.
The canonical model I is given by an interpretation of concept names, ller and re nement relations RI and I on I, respectively, as follows: (C; C ) 2 AI
() (C; C ) 2 ?I
() (C; C ) RI (D; D) () 8X 2 ; C ` A ; C ` ? (C; C )
I (D; D) () ; D ` C:
C (R): ; D 6` X Observe that the constructive semantics distinguishes between two kinds of consistencies, viz. extensional consistency, if (C; C ) 62 ?I and intensional consistency, if ; C 6` C . Our canonical I contains only intensionally consistent objects, though they may be extensionally inconsistent. In such an entity (C; C ) 2 ?I we must necessarily have C (R) = ; for all R 2 NR. For if C (R) = fXg for some R and X then ; ? ` 9R:X by rule ?L which by the assumption ; C ` ? and cut admissibility would yield ; C ` 9R:X in contradiction to intensional consistency of (C; C ). But C (R) = ; means the entity (C; C ) does not exclude any R- llers, 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 re exive because of rule Ax and transitive because of cut admissibility Prop. 2. It is not antisymmetric, though, due to the slack in the second component D which has no in uence 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 inconsistent objects ?I partake in all U L concept descriptions, i.e., for all U L concepts, ?I CI . Thus, I is a constructive model according to Def. 12. Lemma 3. Let be an existentially guarded TBox and E an arbitrary U L concept description. Then, for every (C; C ) 2 I, we have I; (C; C ) j= E i ; C ` E.
Proof. We proceed by induction on E. For concept names and ? the statement follows directly from the de nition of AI . For > we need to use rule >R. The interesting cases are existentials and disjunction:
Let (C; C ) 2 I and suppose ; C 6` 9R: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` 9R: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]) 2 cI = I n ?I . Consider any R- ller (C; [R 7! E]) RI (D; D) which must satisfy ; D 6` E by de nition. Now we use the induction hypothesis to infer I; (D; D) 6j= E which proves I; (C; C ) 6j= 9R:E according to Def. 1, all in all. Vice versa, suppose that ; C ` 9R:E and let (C; C ) I (D; D) 2 cI be given arbitrarily, which means ; D ` C and by 2 To be fully compatible also with the constructive semantics of :, 8R we should also make sure that all R- llers of objects in ?I are themselves extensionally inconsistent.
This is not needed for the existential-disjunctive fragment at hand. cut admissibility ; D ` 9R:E. We claim that there exists a guarded component P of E such that (P; ;) is an R- ller of (D; D). If D(R) = ; we can take any guarded E D P and have (D; D) RI (P; ;) for trivial reasons. Otherwise, if D(R) = fXg we must nd 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 9LR gives ; 9R:E ` 9R:X and further cut admissibility ; D ` 9R: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; ;) j= E which completes the proof that I; (C; C ) j= 9R:E according to Def. 1.
Now assume I; (C; C ) j= E1 tE2, i.e., I; (C; C ) j= 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 ) j= Ei from which I; (C; C ) j= E1 t E2 follows as required. tu
Lemma 3 means that I is a constructive model of the TBox . To see this let F v E 2 and (C; C ) I (D; D) such that I; (D; D) j= 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) j= E by Lem. 3. Hence, overall, I; (C; C ) j= F v E.
Proposition 4. The rules in Fig. 1 are sound for constructive subsumption in U L and complete relative to existentially guarded (general) TBoxes . Proof. Soundness, viz. that ; C ` D implies ; C j= D, is proved by induction on derivations. Regarding completeness, let a subsumption ; C j= D be constructively valid. Consider the canonical model I constructed above which satis es I j= . Take any guarded component C D P of C. By Lem. 2 (i) and rule Ax we have ; P ` C. Hence, I; (P; ;) j= C because of Lem. 3. But then the assumption ; C j= D implies I; (P; ;) j= 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).
Theorem 2. Subsumption checking in U L 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 U L. We want to decide the subsumption C v D relative to . Due to Prop. 4 we can decide ; C j= 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( [ fC; Dg). 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 ) 2 Sf( [ fC; Dg)2 such that ; X ` Y using dynamic programming memorisation techniques and thus decide any xed subsumption in polynomial time. tu
This paper highlights the dramatic e ect that the choice of semantic
interpretation can have on the complexity of reasoning in DL. Arguably, as long as there
is no application domain identi able for the U L fragment these results may only
have theoretical interest. Perhaps our results can be extended to more
expressive 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 U L is
somewhat unexpected. However, as discussed in [
We can see some immediate ways to generalise our results. The main results carry over to all TBoxes in which every C 2 Sf( ) has a non-empty prime cover Cov(C) Sf( ) satisfying the conditions of Prop. 3 and Lem. 2. We have exploited this here for guarded TBoxes in the U L language where every concept has a prime cover. We conjecture that the PTime result extends directly to U L which is U L plus limited universal quanti cation 8R:?. 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 combinatorics does not spill over quanti ers (exploiting that in constructive logic 8: is not the same as :9, etc.). One of our referees has pointed out that if we remove the guardedness restriction then we could express Disjunctive Distribution 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 F L0 to U L0
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
E L (see, e.g., [
Acknowledgements This work has been funded by the German Research Council (DFG) under ME 1427/4-1. The authors would like to thank the anonymous reviewers for their suggestions to improve the presentation of this paper.