Keys, Nominals, and Concrete Domains

1 Introduction

Description Logics (DLs) are a family of popular knowledge representation formalisms. Many expressive DLs combine powerful logical languages with an interface to concrete do­ mains (e.g., integers, reals, strings) and built-in predicates (e.g., <, sub-string-of) [Lutz, 2002b]. These can be used to form descriptions such as "employee working for the govern­ ment and earning more than her boss" that combine "abstract" logical components (e.g. , working for the government) with components using concrete domains and predicates (e.g., a numerical comparison of earnings).

DLs with concrete domains have turned out to be useful for reasoning about conceptual (database) models [Lutz, 2002e], and as the basis for expressive ontology languages [Horrocks et al., 2002]. So far, however, they have not been able to ex­ press key constraints, i.e., constraints expressing the fact that certain "concrete features" uniquely determine the identity of the instances of a certain class. E.g., the concrete feature "so­ cial security number (SSN)" might serve as a key for citizens of the US, and the combination of identification number and manufacturer might serve as a key for vehicles. Such con­ straints are important both in databases and in realistic on­ tology applications. In a DL context, key constraints have so far only been considered on logical, "non-concrete" do­ mains [Borgida and Weddell, 1997; Calvanese et al., 2000; Khizder et al., 2001; Toman and Weddell, 2002].

It is easy to see that concrete keys can express nominals, i.e. , concepts to be interpreted as singleton sets (closely re­ lated to the "one-of" operator): e.g., if SSN is a key for Hu­ man (SSN keyfor Human), then the concept "Human with SSN 1234" (Humann :lSSN. = 1234 ) has at most one instance.

In this paper, we extend the well-known DLs with concrete domains A.CC(V) and S'HOQ(V) [Baader and Hanschke, 1991; Horrocks and Sattler, 2001] with key constraints and analyse the complexity of reasoning with the resulting log­ ics A.CCOJC(V) and S'HOQJC(V). We show that allowing complex concepts to occur in key constraints dramatically increases the complexity of A.CC(V) (which is PSPACE­ complete): it becomes undecidable. Restricting key con­ straints to atomic concepts (such as "Human" in the above example) still yields a NEXPTIME-hard formalism, even for rather simple (PTrME) concrete domains. We show several variants of this result that depend on other characteristics of key constraints, such as the number of concrete features and the "path length". This effect is consistent with the observa­ tion that the PSPACE upper bound for A.CC(V) is not robust [Lutz, 2003].

Additionally, we prove the NEXPTIME bounds to be tight by presenting tableau algorithms for A.CCOJC(V) and S'HOQJC(V) with key admissible concrete domains that are in NP, where key admissibility is a simple and natural prop­ erty. We have chosen to devise tableau algorithms since they have the potential to be implemented in efficient reasoners and have been shown to behave well in practise [Horrocks et al., 2000]. Due to space restrictions, we can only sketch proofs and refer to [Lutz et al., 2002] for more details.

2 Preliminaries

First, we formally introduce the description logic A.CCOJC(V).

Definition 1. A concrete domain V is a pair (.6.v , <I>v) , where .6.v is a set and <I>v a set of predicate names. Each predicate name P E <I>v is associated with an arity n and an n-ary predicate pD ~ .6.7J.

Let Nc, No, NR, NcF be pairwise disjoint and countably in­ finite sets of concept names, nominals, role names, and con­ crete features. We assume that NR has a countably infinite subset NaF of abstract features . A path u is a composition h · · · fng of n abstract features h, ... , fn (n 2: 0) and a concrete feature g. Let V be a concrete domain. The set of A.CCOJC(V)-concepts is the smallest set such that (i) every concept name and every nominal is a concept, and (ii) if C and D are concepts, R is a role name, g is a concrete feature, u1 , ... , Un are paths, and P E <I>v is a predicate of arity n, then the following expressions are also concepts:

A key definiton is an expression ( u1 , ... , uk keyfor C) for u1, ... , Uk (k 2: 1) paths and C a concept. A finite set of key definitions is called a key box. 0

As usual, we use T to denote an arbitrary propositional tau­ tology. Throughout this paper, we will consider several frag­ ments of the logic A.CCOK:(V): A.CCO(V) is obtained from A.CCOK:(V) by admitting only empty key boxes; by disal­ lowing the use of nominals, we obtain the fragment A.CC (V) of A.CCO('D) and A.CCK:(V) of A.CCOK:(V).

The description logic A.CCOK:(V) is equipped with a Tarski-style set-theoretic semantics. Along with the seman­ tics, we introduce the standard inference problems: concept satisfiability and concept subsumption.

Definition 2. An interpretation I is a pair ( .6.:r, · 7 ), where .6.:r is a non-empty set, called the domain, and .:r is the in­ terpretation function. The interfretation function maps each concept name C to a subset C of .6.:r, each nominal N to a singleton subset N 7 of .6.:r, each role name R to a subset R 7 of .6.:r x .6.:r, each abstract feature f to a partial function ! 7 from .6.:r to .6.:r, and each concrete feature g to a partial function g 7 from .6.:r to .6.v.

If u = h · · · fng is a path and d E .6.7 , then u 7 (d) is de­ fined as g 7 (!'[( · · · (if (d)) · · · ) . The interpretation function is extended to arbitrary concepts as follows:

An interpretation I is a model of a concept C iff C 7 =f 0. Moreover, I satisfies a key definition ( u1 , . .. , Un keyfor C) if, for any a, bE C 7 , uf(a) = uf(b) for 1 ~ i ~ n implies a = b. I is a model of a key box K iff I satisfies all key definitions in K. A concept C is satisfiable w.r.t. a key box K iff C and K have a common model. C is subsumed by a concept D w.r.t. K (written c CK D) iff c:r c D 7 for all modelsiofK. - - 0

It is well-known that, in DLs providing for negation, sub­ sumption can be reduced to (un)satisfiability and vice versa: C ~K D iff C n ·D is unsatisfiable w.r.t. K and C is sat­ isfiable w.r.t. K iff C gK -, T. Thus we can concentrate on concept satisfiability when investigating the complexity of reasoning: the above reduction implies the corresponding bounds for subsumption and the complementary complexity class (usually co-NEXPTIME in this paper).

When devising decision procedures for DLs which are not tied to a particular concrete domain, admissibility of the con­ crete domain usually serves as a well-defined interface be­ tween the decision procedure and concrete domain reasoners [Baader and Hanschke, 1991; Lutz, 2002b]:

Definition 3. Let V be a concrete domain. A V-conjunction is a (finite) predicate conjunction of the form

where P; is an n;-ary predicate for i < k and the x(i) are variables. A 'D-conjunction c is satisfiable iff there e~ists a function b mapping the variables in c to elements of .6.v such that (b(xbi)), .. . , b(x~})) E PP for each i < k. We say that the concrete domain V is admissible iff (i) ci>v contains a name Tv for .6.v; (ii) ci>v is closed under negation, and (iii) satisfiability of 'D-conjunctions is decidable. We refer to the satisfiability of 'D-conjunctions as V-satisfiability. 0

As we shall see, it sometimes makes a considerable differ­ ence w.r.t. complexity and decidability to restrict key boxes in various ways. Because of this, it is convenient to introduce the following notions:

Definition 4. A key box K is called Boolean if all concepts appearing in (key definitions in) K are Boolean combinations of concept names; path-free if all key definitions in K are of the form (91, ... , 9n keyfor C) with 91, ... , 9n E NcF; sim­ ple if it is both path-free and Boolean; and a unary key box if all key definitions in K are of the form ( u keyfor C). A con­ cept C is called path-free if, in all its subconcepts of the form ~u1, ... , Un.P, u1, ... , Un are concrete features. 0

To emphasize that a key box must not necessarily be Boolean or path-free, we sometimes call such a key box general. Sim­ ilarly, to emphasize that a key box is not necessarily a unary key box, we sometimes call such a key box n-ary key box.

3 Lower Complexity Bounds

In this section, we present lower complexity bounds for DLs with concrete domains, key boxes and nominals. We start by showing that satisfiability of A.CCK('D)-concepts w.r.t. gen­ eral key boxes is undecidable for many interesting concrete domains. This discouraging result is relativized by the fact that, as shown in Section 4, the restriction to Boolean key boxes recovers decidability. Next, we prove that satisfiabil­ ity of path-free A.CCK('D)-concepts w.r.t. simple key boxes is NEXPTIME-hard for many concrete domains and that this holds even if we restrict ourselves to unary key boxes. Fi­ nally, we identify a concrete domain such that A.CCO('D)­ concept satisfiability (without key boxes) is already NEXP­ TIME-hard.

Undecidability of A.CCK:('D)-concept satisfiability w.r.t. general key boxes is proved by reduction of the undecidable Post Correspondence Problem (PCP) [Post, 1946].

Definition 5. An instance P of the PCP is given by a finite, non-empty list ( e 1 ' r1)' ... ' ( ek' r k) of pairs of words over some alphabet I:. A sequence of integers i1 , . . . , im, with m 2: 1, is called a solution for P iff t'; 1 · · · t';"' = r; 1 · · · r;"'. The problem is to decide whether a given instance P has a solution. 0

The reduction uses the admissible concrete domain W intro­ duced in [Lutz, 2003], whose domain is the set of words over L: and whose predicates express concatenation of words. For each PCP instance P = (t'1,r1), ... ,(ek,rk), we define a concept Cp and unary key box /Cp such that P has no solu­ tion iff Cp is satisfiable w.r.t. /C p. Intuitively, Cp and /Cp enforce an infinite, k-ary tree, where each node represents a sequences of integers, i.e. a potential solution. The role of the key box is to guarantee that the tree is of infinite depth; concrete features are used to store the left and right concate­ nations corresponding to the potential solutions; and concate­ nation predicates from the concrete domain W are used to compute them. Finally, an inequality predicate also provided by W is used to guarantee that none of the potential solutions is indeed a solution. Since it is known that W-satisfiability is in PTIME [Lutz, 2003], we obtain the following theorem.

Theorem 6. There exists a concrete domain V such that D-satisfiability is in PTIME and satisfiability of A.CCK(V)­ concepts w.r.t. (general) unary key boxes is undecidable.

As shown in [Lutz, 2003; Lutz et al., 2002], the reduction can easily be adapted to more natural concrete domains such as numerical ones based on the integers and providing predicates for equality to zero and one, binary equality, addition, and multiplication.

We now establish lower bounds for A.CCK(V) with Boolean key boxes and for A.CCO(V). These results are obtained using a NEXPTIME-complete variant of the well­ known, undecidable domino problem [Knuth, 1968].

Definition 7. A domino system 1> is a triple (T, H , V), where T C lN is a finite set of tile types and H, V ~ T x T repre­ sent the horizontal and vertical matching conditions. For 1> a domino system and a = ao, . . . , an-l E Tn an initial condi­ tion, a mapping T : {0, ... , 2n+1} x {0, . . . , 2n+1} --7 T is a solution for 1> and a iff, for all x, y < 2n+1, the following holds: (i) if T(x, y) = t and T(x+ 1 mod 2n+1 , y) = t', then (t,t') E H; (ii) ifT(x, y) = t andT(x, y + 1 mod 2n+l) = t', then (t, t') E V ; and (iii) T(i , 0) = ai fori < n. 0

This variant of the domino problem is NEXPTIME­ complete [Lutz, 2003]. The three NEXPTIME lower bounds are obtained by using suitable and admissible concrete do­ mains 0 1 , 0 2 , and 0 3 to reduce the above domino prob­ lem. More precisely, the simplest concrete domain 0 1 is used in the reduction to A.CCK(OI)-concept satisfiability w.r.t. Boolean (n-ary) key boxes, the slightly more complex 0 2 is used in the reduction to A.CCK(02 )-concept satisfiabil­ ity w.r.t. Boolean unary key boxes, and the most powerful concrete domain 0 3 is used in the reduction to A.CC0(03)­ concept satisfiability without key boxes.

The idea underlying all three reductions is to use concept names X 0 , .. . Xn, Y0 , . . . , Yn to represent positions in the 2n+I x 2n+1-torus: if a is a domain element representing the position (i,j), then a E Xf expresses that the £-th bit in the binary coding of i is 1, and a E Y/ expresses that the £-th bit of j is 1. We use standard methods to enforce that there exists a domain element for every position in the torus. The main difference between the three reductions is how it is en­ sured that no position is represented by two different domain elements-we call this uniqueness of positions.

The first reduction uses the very simple concrete do­ main 0 1 , which is based on the set {0, 1} and only pro­ vides unary predicates = 0 , = 1 , and their negations. Unique­ ness of positions is ensured by translating the position (i,j)

of a domain element a into concrete domain values: for xpose E NcF, we enforce that xposf (a) = 1 if a E Xf and 0 otherwise (analogously for ypose and Ye). Then the key def­ inition (xpos 0 , ... , xposn, ypos 0 , ... , yposn keyfor T) obvi­ ously ensures uniqueness of positions. Since the reduction concept is path-free and 0 1-satisfiability is easily seen to be in PTIME, we obtain the following:

Theorem 8. 0 1 -satisfiability is in PTIME and satisfiability of path-free A.CCK(OI) -concepts w.r.t. simple key boxes is NEXPTIME-hard.

The (somewhat artificial) concrete domain 0 1 can be replaced by many natural concrete domains V proposed in the litera­ ture [Baader and Hanschke, 1992; Haarslev and Moller, 2002; Lutz, 2002b; 2002d]: it suffices that V provides two unary predicates denoting disjoint singleton sets.

The second reduction uses the more complex concrete do­ main 0 2 , which "stores" whole bit vectors rather than only single bits. In 0 2 , we can translate the position (i,j) of an element a from concepts X e, Yk into a single bit vector of length 2(n + 1) that is then stored as a bv-successor of a, where bv is a concrete feature. Since we replaced the 2(n+ 1) concrete features used in the first reduction (one for each bit) by the single feature bv, it now suffices to use the simple unary key box (bv keyfor T) to ensure uniqueness of posi­ tions. As in 0 1 , the reduction concept is path-free. In [Lutz et al., 2002], it is shown that 0 2-satisfiability is in PTIME.

Theorem 9. 0 2 -satisfiability is in PTIME and satisfiability of path-free A£CK(02 )-concepts w.r.t. simple unary key boxes is NEXPT!ME-hard.

Again, the artificial concrete domain 0 2 can be replaced by more natural ones: we can simulate bit vectors using inte­ gers and the necessary operations on bit vectors by unary predicates =n for every interger n and a ternary addition predicate-for more details see [Lutz et al., 2002].

The last lower bound is concerned with the DL A.CC O(V). In the absence of key boxes, we need a different reduction strategy and the more complex concrete domain 0 3, which extends 0 2 with so-called domino arrays that allow us to store the tiling of the whole torus in a single concrete domain value. We can then ensure uniqueness of positions using a single nominal. Computationally, the concrete domain 0 3 is still very simple, namely in PTIME. However, it no longer suffices to use only path-free concepts.

Theorem 10. 0 3-satisfiability is in PT!ME and satisfiability of A.CC0(03)-concepts is NEXPTIME-hard.

4 Reasoning Procedures

We describe two tableau-based decision procedures for con­ cept satisfiability in DLs with concrete domains, nomi­ nals, and keys. The first is for A.CCOK(D)-concepts w.r.t. Boolean key boxes. This algorithm yields a NEXPTIME up­ per complexity bound matching the lower bounds established in Section 3. The second procedure is for SHOQK(V) w.r.t. path-free key boxes and also yields a tight NEXPTIME up­ per complexity bound. SHOQK(V) is an extension of the DL SHOQ(V) introduced in [Horrocks and Sattler, 2001;

Pan and Horrocks, 2002], which provides a wealth of ex­ pressive possibilities such as transitive roles, role hierar­ chies, nominals, qualifying number restrictions, and general TBoxes with a path-free concrete domain constructor and path-free key boxes. Path-freeness of SHOQK(V) 's con­ crete domain constructor is crucial for decidability. More­ over, it allows us to admit general rather than only Boolean key boxes.

Tableau algorithms decide the satisfiability of the input concept (in our case w.r.t. the input key box) by attempting to construct a model for it: starting with an initial data structure induced by the input concept, the algorithm repeatedly ap­ plies completion rules. Eventually, the algorithm either finds an obvious contradiction or it encounters a contradiction-free situation in which no more completion rules are applicable. In the former case the input concept is unsatisfiable, while in the latter case it is satisfiable.

Existing tableau algorithms for DLs with concrete do­ mains use admissibility as an "interface" between the tab­ leau algorithm and a concrete domain reasoner [Lutz, 2002b; Baader and Hanschke, 19911. In the presence of keys, this is not enough: besides knowing whether a given V­ conjunction is satisfiable, the concrete domain reasoner has to provide information on variables that must take the same value in solutions. As an example, consider the concrete domain N = (IN, { <nl n E IN}) and the N-conjunction c = <2(v1) 1\ <2(v2) 1\ <2(v3) . Obviously, every solution 8 for c identifies two of the variables v1 , v2 , v3 . This informa­ tion has to be passed from the concrete domain reasoner to the tableau algorithm since, in the presence of key boxes, it may have an impact on the satisfiability of the input concept. E.g., this information transfer reveals the unsatisfiability of 3R.An 3R.(-.AnB) n3R.(-.An-.B)n\IR.3g.<2 w.r.t. g keyfor T. To formalize this requirement, we strengthen the notion of ad­ missibility into key-admissibility.

Definition 11. A concrete domain V is key-admissible iff (i) <Pv contains a name Tv for ~v; (ii) <Pv is closed under negation, and (iii) there exists an algorithm that takes as input a V-conjunction c, returns clash if c is unsatisfiable, and oth­ erwise non-deterministically outputs an equivalence relation ""' on the set of variables V used in c such that there exists a solution 8 for c with the following property: for all v , v' E V 8 ( v) = 8 ( v') iff v ""' v'. Such an equivalence relation is henceforth called a concrete equivalence. We say that ex­ tended V-satisfiability is in NP if there exists an algorithm as above running in polynomial time. ()

It can easily be seen that any concrete domain that is ad­ missible and provides for an equality predicate is also key­ admissible [Lutz et al., 2002].

In the following, we assume that all concepts (the input concept and those occuring in key boxes) are in negation nor­ ma/form (NNF), i.e., negation occurs only in front of concept names and nominals; if the concrete domain V is admissi­ ble, then every A.CCOK(V)-concept can be converted into an equivalent one in NNF [Lutz et al., 2002]. We use .:., C to denote the result of converting the concept -.C into NNF, sub(C) to denote the set of subconcepts of C, and sub(K) to denote the set of subconcepts of all concepts occurring in key box K. Moreover, we use cl ( C, K) as abbreviation for the set sub( C) u sub(K) u { .:,n I D E sub(K) }.

Complexity of A£COK(V)

We start the presentation of the A.CCOK(V) tableau algo­ rithm by introducing the underlying data structure.

Definition 12. Let Oa and Oc be disjoint and countably in­ finite sets of abstract and concrete nodes. A completion tree for an A.CCOK(V)-concept C and a key box K is a finite, labeled tree (Va, Vc, E, .C) with a set of nodes Va U Vc such that Va ~ Oa, Vc ~ Oc, and all nodes from Vc are leaves. Each node a E Va of the tree is labeled with a subset .C(a) of cl ( C, K); each edge (a, b) E E with a, b E Va is labeled with a role name .C(a, b) occurring inC or K; and each edge (a, x ) E E with a E Va and x E Vc is labeled with a concrete feature .C(a, x ) occurring inC or K.

ForT= (Va, Vc,E,.C) and a E V.,, we use levT(a) to denote the depth at which a occurs in T (starting with the root node at depth 0). A completion system for an A.CCOK(V)­ concept C and a key box K is a tuple (T, P, -< , ""'), where T = (Va, Vc, E, .C) is a completion tree for C and K, P is a function mapping each P E <Pv with arity n appearing in C to a subset of v;;n, -< is a linear ordering of Va such that levT(a) :S levT(b) implies a -< b, and""' is an equivalence relation on Vc .

LetT = (Va, Vc, E, .C) be a completion tree. A node b E Va is an R-successor of a node a E Va if (a, b) E E and .C(a, b) = R. Similarly, a node x E Vc is a g-successor of a if (a, x) E E and .C(a,x) =g. For paths u, the notion u-successor is defined in the obvious way. ()

Intuitively, the relation ""' records equalities between concrete nodes that have been found during the model construction process. The relation ""' induces an equivalence relation ~a on abstract nodes which, in tum, yields the equivalence rela­ tion ~c 2 ""' on concrete nodes.

Definition 13. Let S = (T, P, -<, ""') be a completion system for a concept C and a key box K with T = (Va, Vc , E , .C) , and let ~ be an equivalence relation on Va. For each R E NR, a node b E Va is an R/~-neighbor of a node a E Va if there exists a node c E Va such that a ~ c and b is an R-successor of c. For paths u, the notion uf~-neighbor is defined analogously.

We define a sequence of equivalence relations ~~ ~ ~! ~ · · · on Va as follows :

Finally, set ~a = ui>O ~!. and define X ~, y if X "' y or there are a E Va andg E NcF such that x andy are g/~a­ neighbors of a. 0

Intuitively, if we have a ~a b, then a and b describe the same domain element of the constructed model (and similarly for the~, relation on concrete nodes).

Let V be a key-admissible concrete domain. To de­ cide the satisfiability of an A.CCOK(V)-concept Co w.r.t. a Boolean key box K (both in NNF), the tableau algo­ rithm is started with the initial completion system Sc 0 = (Tc 0 ,P0,0, 0), whereTc 0 = ({ao},0,0,{ao f-t {Co}}) and P0 maps each P E <Pv occurring in Co to 0. We now introduce an operation that is used by the completion rules to add new nodes to completion trees.

Definition 14. LetS = (T, P, -<,"')be a completion system with T = (Va, Vc, E, .C). An element of Oa or 0, is called fresh in T if it does not appear in T. We use the following notions:

S +aRb: Let a E Va, b E Oa fresh in T, and R E NR. We writeS+ aRb to denote the completion systemS' that can be obtained from S by adding (a, b) toE and setting .C(a, b) = Rand .C(b) = 0. Moreover, b is inserted into -< such that b-< c implies levT(b) :::; levT(c).

S + agx: Let a E Va, x E 0, fresh in T and g E NcF· We write S + agx to denote the completion system S' that can be obtained from S by adding (a, x) to E and setting .C(a, x) =g.

When nesting+, we omit brackets writing, e.g., S + aR1b + bR2c for (S + aR1b) + bR2c. Let u = h · · · fng be a path. With S + aux, where a E Va and x E 0, is fresh in T, we denote the completion system S' that can be obtained from S by taking fresh nodes b1 , . . . , bn E Oa and setting

0

The completion rules are given in Figure 1, where we assume that newly introduced nodes are always fresh. The RU and Rch rules are non-deterministic and the upper five rules are well-known from existing tableau algorithms for A.CC(V)­ concept satisfiability (c.f. for example [Lutz, 2002d]). Only R'v' deserves a comment: it considers R/~a-neighbors rather than R-successors since ~a relates nodes denoting the same domain element.

The last two rules are necessary for dealing with key boxes. The "choose rule" Rch (c.f. [Hollunder and Baader, 1991; Horrocks et al., 2000]) guesses whether an abstract node a satisfies C in case of C occurring in a key definition and a having neighbors for all paths ui in this key definition. The Rp rule deals with equalities between abstract nodes as recorded by the ~a relation: if a ~a b, then a and b describe the same element, and thus their node labels should be identi­ cal. We choose one representative for each equivalence class of ~a (the node that is minimal w.r.t. -<) and make sure that the representative's node label contains the labels of all the nodes it represents.

Definition 15. Let S = (T, P, -<, "') be a completion system for a concept C and a key box K with T = (Va, Vc, -< , "'). We

Rn ifC1 n C2 E £(a) and {C1 , C2} ~£(a) then L:(a) :=£(a) U {C1, C2} RU ifC1 U C2 E .C(a) and {C1,C2} n .C(a) = 0 then L:(a) :=£(a) U {C} for some C E {C1, C2} R3 if 3R. C E £ (a) and there is no R/ :::::a -neighbor b of a such that C E .C(b), then S := S +aRb and £(b):= {C} RV ifVR.C E .C(a), b is an R/:::::.-neighbor of a, and c ¢ L:(b) then £(b) := L:(b) U {C} R3c if 3ul, ... , Un .P E £(a) and there are no u;-successors x ; of a (for 1 ::; i ::; n) with (x1, . .. , Xn) E P(P) then S := (S + au1 x 1 + · · · + aunxn) and P(P) := P(P) U { (x1 , ... , Xn)} Rch if (u1, .. . , un keyfor C) E K, {C, .:.,c} n £(a)= 0, and there are u;/:::::3 -neighbors x; of a (for 1 ::; i ::; n) then £(a):= £(a) U {D} for some DE {C, .:.,c} Rp if L:(b) ~£(a) and a E Va is minimal w.r.t.-< such that a :::::. b then £(a) := L:(a) U .C(b)

say that the completion system S is concrete domain satisfi­ able iff the conjunction

is satisfiable. S contains a clash iff (i) there is an a E Va and an A E Nc such that {A, -,A} ~ .C(a); (ii) there are a E Va and x E Vc such that gt E .C(a) and xis g/~a-neighbor of a; or (iii) S is not concrete domain satisfiable. If S does not contain a clash, then S is called clash-free. S is complete if no completion rule is applicable to S. 0

We now give the tableau algorithm in pseudocode nota­ tion, where check denotes the algorithm computing concrete equivalences as described in Definition 11:

define procedure sat(S)

do if S contains a clash then return unsatisfiable ,...., :=check( (s) compute :::::. and then :::::c while ,...., =/= :::::c if S contains a clash then return unsatisfiable if Sis complete then return satisfiable apply a completion rule to S yielding S'

return sat(S')

The algorithm realizes a tight coupling between the con­ crete domain reasoner and the tableau algorithm: if the con­ crete domain reasoner finds that two concrete nodes are equal, the tableau algorithm may use this to deduce (via the com­ putation of ~a and ~c) even more equalities between con­ crete nodes. The concrete domain reasoner may then return in check( (s) further "equalities" "' and so forth.

A similar interplay takes place in the course of several re­ cursion steps: equalities of concrete nodes provided by the concrete domain reasoner may make new rules applicable (for example Rp and then R:Jc) which changes P and thus also (s. This may subsequently lead to the detection of more equali­ ties between concrete nodes by the concrete domain reasoner, and so forth. Note that, in the absence of keys boxes, there is much less interaction: it suffices to apply the concrete domain satisfiability check only once after the completion rules have been exhaustively applied [Baader and Hanschke, 1991].

In [Lutz et al., 2002], we prove that the algorithm runs in non-deterministic exponential time: there are exponential bounds on the number of abstract and concrete nodes in the completion system, on the number of while loop iterations in each recursion step, and on the size of (s. This yields the following upper bound, which is tight by Theorem 9.

Theorem 16. ForD a key-admissible concrete domain such that extended D-satisfiability is in NP, A.CCOJC(D) -concept satisfiability w.r.t. Boolean key boxes is in NEXPTIME.

Complexity of StlOQK(D)

We have designed a tableau algorithm for SHOQJC(D) as a combination of the one for SHOQ(D) in [Horrocks and Sat­ tler, 2001] and the one for A.CCOJC(D) presented above. It is restricted to path-free concepts and path-free key boxes, but can handle complex concepts in key boxes. The most impor­ tant difference from the A.CCOJC(D) algorithm is as follows: in the presence of non-Boolean key boxes, the Rch rule may add concepts of positive "role depth" to arbitrary nodes in the completion tree. Thus the role depth does not automatically decrease with the depth of nodes in the tree (as in the case of A.CCOJC(D)) and a naive tableau algorithm would con­ struct infinite trees. However, even for SHOQ(D) without key boxes, one has to enforce termination artificially by us­ ing a cycle detection mechanism called blocking-whereas the A.CCOJC(D) algorithm terminates "naturally". It can be shown that blocking can be used in the presence of key boxes without corrupting soundness or completeness. A detailed description of this algorithm and a correctness proof is given in [Lutz et al., 2002]. As a by-product of the SHOQJC(D) tableau algorithm, we obtain a small model property: every satisfiable SHOQJC(D)-concept has a model of size expo­ nential in the concept length. Thus we obtain the following upper bound, which is tight by Theorem 9.

Theorem 17. ForD a key-admissible concrete domain such that D-satisfiability is in NP, SHOQJC(D)-concept satisfia­ bility w.r.t. path-free key boxes is in NEXPTIME.

5 Summary

We have identified key boxes as an interesting extension of description logics with concrete domains, introduced a num­ ber of natural description logics, and provided a comprehen­ sive analysis of the decidability and complexity of reasoning. Moreover, we have proposed tableau algorithms for two such (NEXPTIME-complete) logics.

The main result of our investigations is that key constraints are rather powerful, since they dramatically increase the com­ plexity of reasoning: PSPACE A.CC (D) becomes undecidable with unrestricted key boxes, and NEXPTIME-complete with Boolean key boxes-provided that the concrete domain D is not too complex, i.e., extended D-satisfiability is in NP.