Introduction

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 finally (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 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 exploring 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 languages 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 FL 0 consisting of {∀, } and the EL-type languages which build on the operator set {∃, }. Among these, the latter tend to be much better behaved (e.g., more efficient and less sensitive to extensions) than the former. For instance, it is known that subsumption checking in FL 0 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 semantics [1] and it becomes ExpTime complete for general TBoxes (descriptive 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 , 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: FL 0 with {∀, } permits us to make general statements of the form "all S are P" while EL with {∃, } corresponds 1 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 {∀, } and {∃, }. 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 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 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 decisive role for the complexity of the subsumption problem in certain fragments of ALC. Specifically, we will show that for the {∃, } fragment, here named UL, there is an exponential gap between the classical descriptive semantics which gives ExpTime-complete subsumption checking while for the constructive semantics [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 relation for concept abstraction and refinement. The idea behind the constructive 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 potentially 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 | | ⊥ | ¬C | C D | C D | C D | ∃R.C | ∀R.C,

where A ∈ N C and R ∈ N R . This syntax is more general than standard ALC in that it includes subsumption as a concept-forming operator. The fact that can be nested will be irrelevant for the purposes of this paper. Still, we present the constructive semantics for the full system: I is lifted from constant ⊥ and concept names A to arbitrary concepts as seen below, where

∆ I c = df ∆ I \ ⊥ I is the set of non-fallible elements in I: I = df ∆ I (¬C) I = df {x | ∀y ∈ ∆ I c . x I y ⇒ y ∈ C I } (C D) I = df C I ∩ D I (C D) I = df C I ∪ D I (C D) I = df {x | ∀y ∈ ∆ I c . (x I y & y ∈ C I ) ⇒ y ∈ D I } (∃R.C) I = df {x | ∀y ∈ ∆ I c . x I y ⇒ ∃z ∈ ∆ I . (y, z) ∈ R I & z ∈ C I } (∀R.C) I = df {x | ∀y ∈ ∆ I c . x I y ⇒ ∀z ∈ ∆ I . (y, z) ∈ R I ⇒ z ∈ C I }.

Entities in ∆ I are partial descriptions representing incomplete information about individuals. Read a b as saying that b "is a refinement of " a. The difference to the classical descriptive semantics is the refinement dimension I and the universal quantification ∀y ∈ ∆ I c . 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 related 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 ¬C ≡ , Double Negation ¬¬C ≡ C, the dualities ∃R.C ≡ ¬∀R.¬C, ∀R.C ≡ ¬∃R.¬C and Disjunctive Distribution ∃R.(C D) ≡ ∃R.C ∃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 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 D), yet it would be rather strong to assume it also satisfies ∃R.C ∃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 introduce some pieces of notation. First, it will be convenient In the following we will consider TBoxes Θ which consist entirely of subsumptions C D such that both C, D are -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 concept descriptions formed as 3 Guarded U L 0 is ExpTime hard for Classical Descriptive Semantics

C, D :: = | ⊥ | A | C D | ∃R.C with A ∈ N C and R ∈ N R .

We reduce subsumption in the language FL 0 consisting of operators {∀, } to subsumption in UL under classical descriptive semantics. In fact, we will reduce subsumption in FL 0 to the fragment UL 0 , which is UL without the constants , ⊥, and relative to guarded UL 0 TBoxes. Let Θ be a general TBox in FL 0 and C, D two FL 0 concept descriptions. For simplicity we assume that N C contains exactly the concept names appearing in Θ or C, D. The first step in our reduction dualises the problem under the classical descriptive semantics, replacing → and ∀ → ∃ and swapping left and right-hand sides of subsumptions. Formally, define the dual d (C) of a FL 0 concept description recursively as follows: need not be existentially guarded, though. However, this can be fixed.We introduce 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 UL 0 TBox Θ we define its expansion

d (A) = df A, d (C D) = df d (C) d (D), d (∀R.C) = df ∃R.d (C).exp(Θ) = df {C ∃τ.D | C D ∈ Θ} ∪ { ∃R.X ∃τ.∃R.X, ∃τ.∃R.X ∃R.X | ∃R.X ∈ Sf(Θ)} ∪ {A ∃τ.A, ∃τ.A A | A ∈ N C },

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 Lemma 1 gives a linear-time reduction of the FL 0 problem to that in UL 0 , where the simulating TBox exp(d (Θ)) is existentially guarded. Since subsumption checking in FL 0 for general TBoxes and classical descriptive semantics is ExpTime hard [12,4] we have the following theorem: Theorem 1. UL 0 subsumption checking under the classical semantics and relative 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 existential distribution |= cl ∃R.(C D) ≡ (∃R.C ∃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 FL 0 the operators { , ∀} distribute while in the PTime fragment { , ∃} [2, 12] they do not.

Guarded U L is in PTime for Constructive Descriptive Semantics

In the following we will show that subsumption checking in UL under the constructive 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 L, L, ∃LR, ⊥L and right introduction rules R 1 , R 2 , ∃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 |= D. A sequent Θ; C D is (constructively) satisfiable, iff there exists (I, a) which satisfies the sequent. This is equivalent to non-subsumption Θ; C |= 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 D 1 , D 2 ∈ Sf(Θ) ∪ Sf(P ), whenever Θ; P |= D 1 D 2 then Θ; P |= D 1 or Θ; P |= D 2 .

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 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.

Ax Θ; C C ⊥L Θ; ⊥ C R Θ; C Θ; E C R 1 Θ; E C D Θ; E D R 2 Θ; E C D Θ; C F Θ; D F L Θ; C D F Θ; E C Θ; D F L Θ, C D; E F Θ; C D ∃LR Θ; ∃R.C ∃R.D

Proposition 1. Every existentially guarded UL concept description C is constructively prime for the empty TBox.

Proof. By induction on the structure of C and the definition of |= for the constructive semantics (see page 4).

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 Proof. We proceed by induction on the derivation for Θ; P D 1 D 2 . Since P is not a disjunction, the last rule in this derivation cannot be Ax , L, ∃LR or R. If the last rule is ⊥L or one of R 1 , R 2 the claim follows immediately. The only interesting case is when the derivation ends in an application of L, i.e., it looks like . . .

π 1 Θ; P E . . . π 2 Θ; F D 1 D 2 L Θ, E F ; P D 1 D 2

By assumption on our TBox from which E F is drawn, F is guarded. Hence we may invoke the induction hypothesis on the sub-derivation π 2 . This gives a

The canonical model I is given by an interpretation of concept names, filler and refinement relations R I and I on I, respectively, as follows:

(C, Ψ C ) ∈ A I ⇐⇒ Θ; C A (C, Ψ C ) ∈ ⊥ I ⇐⇒ Θ; C ⊥ (C, Ψ C ) R I (D, Ψ D ) ⇐⇒ ∀X ∈ Ψ C (R). Θ; D X (C, Ψ C ) I (D, Ψ D ) ⇐⇒ Θ; D C.

Observe that the constructive semantics distinguishes between two kinds of consistencies, viz. extensional consistency, if (C, Ψ C ) ∈ ⊥ I and intensional consistency, if Θ; C Ψ C . Our canonical I contains only intensionally consistent objects, though they may be extensionally inconsistent. In such an entity (C, Ψ C ) ∈ ⊥ I we must necessarily have Ψ C (R) = ∅ for all R ∈ N R . 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 exclude any R-fillers, i.e. (C, Ψ C ) R I (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 admissibility 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 A I are closed under I due to cut admissibility. Extensionally inconsistent 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. We claim that there exists a guarded component P of E such that (P, ∅) is an R-filler of (D, Ψ D ). If Ψ D (R) = ∅ we can take any guarded E P and have (D, Ψ D ) R I (P, ∅) for trivial reasons. Otherwise, if Ψ D (R) = {X} we must find a guarded component P of E such that Θ; P X. We proceed by contradiction. Suppose, Θ; P X for every P with E 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 ) R I (P, ∅) for some guarded component P of E. By Lem. 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.

Conclusion and Future Work

This paper highlights the dramatic effect that the choice of semantic interpretation 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 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 UL is somewhat 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 exploited 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 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 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 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 FL 0 to UL 0 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 {∀, } under the classical semantics. Similarly, coNP-hardness for FL 0 in acyclic TBoxes should imply coNP-hardness for UL 0 , PSpace-hardness of FL 0 should give PSpace-hardness of UL 0 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.