Abstract:
Many description logics (DLs) combine knowledge representation on an abstract, logical level with an interface to 'concrete' domains like numbers and strings with built-in predicates such as >, +, and prefix-of. These hybrid DLs have turned out to be useful in several application areas, such as reasoning about conceptual database models. We propose to further extend such DLs with key constraints that allow the expression of statements like 'US citizens are uniquely identified by their social security number'. Based on this idea, we introduce a number of natural description logics and perform a detailed analysis of their decidability and computational complexity. It turns out that naive extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.

---

Extracted Text

 


 
Journal of Artificial Intelligence Research 23 (2005) 667-726
Submitted 07/04; published 06/05
Keys, Nominals, and Concrete Domains
Carsten Lutz
lutz@tcs.inf.tu-dresden.de
Theoretical Computer Science, TU DresdenD-01062 Dresden, Germany
Carlos Areces
areces@loria.fr
INRIA Lorraine, Nancy54602 Villers les Nancy Cedex, France
Ian Horrocks
horrocks@cs.man.ac.uk
Department of Computer ScienceUniversity of ManchesterOxford Road, Manchester M13 9PL, UK
Ulrike Sattler
sattler@cs.man.ac.uk
Department of Computer Science
University of Manchester
Oxford Road, Manchester M13 9PL, UK
Abstract
Many description logics (DLs) combine knowledge representation on an abstract, logicallevel with an interface to “concrete” domains like numbers and strings with built-in predi-cates such as <, +, and prefix-of. These hybrid DLs have turned out to be useful in severalapplication areas, such as reasoning about conceptual database models. We propose tofurther extend such DLs with key constraints that allow the expression of statements like“US citizens are uniquely identified by their social security number”. Based on this idea,we introduce a number of natural description logics and perform a detailed analysis oftheir decidability and computational complexity. It turns out that naive extensions withkey constraints easily lead to undecidability, whereas more careful extensions yield NExp-Time-complete DLs for a variety of useful concrete domains.
1. Motivation
Description logics (DLs) are a family of formalisms that allow the representation of andreasoning about conceptual knowledge in a structured and semantically well-understoodmanner (Baader, Calvanese, McGuinness, Nardi, & Patel-Schneider, 2003). The centralentities for representing such knowledge are concepts, which are constructed from atomicconcept names (unary predicates) and role names (binary relations) by means of the conceptand role constructors offered by a particular DL. For example, in the basic propositionallyclosed description logic ALC (Schmidt-Schauß & Smolka, 1991), we can describe a companythat has part-time employees but only full-time managers using the concept
Company
∃employee.Parttime
∀employee.(¬Manager
¬Parttime).
In this example, all words beginning with uppercase letters denote concept names whileemployee denotes a role name.
c 2005 AI Access Foundation. All rights reserved.

 
Lutz, Areces, Horrocks, & Sattler
Rather than being viewed only as conceptual entities in a knowledge base, concepts
can, more generally, be understood as the central notion in various kinds of class-centeredformalisms. In the last decade, this observation has given rise to various new and challeng-ing applications of description logics such as reasoning about database conceptual modelsexpressed in entity-relationship diagrams or object-oriented schemas (Calvanese, Lenzerini,& Nardi, 1998; Calvanese, De Giacomo, & Lenzerini, 1998) and reasoning about ontologiesfor use in the semantic web (Baader, Horrocks, & Sattler, 2002a; Horrocks, 2002; Horrocks,Patel-Schneider, & van Harmelen, 2002). These new applications have, in turn, stimulatedresearch in description logics since the expressive power of existing DLs was insufficientfor the new tasks. One important extension is by providing expressive means that allowthe integration of numbers and other datatypes: suppose, for example, that we want toextend our earlier descriptions of companies and employees to include the founding year ofa company and the hiring year of an employee. Then, we may want to describe companiesthat were founded before 1970 and state that the hiring year of employees is not prior tothe founding year of the employing company. To do this, we obviously need a way to talkabout natural numbers (such as 1970) and comparisons between natural numbers.
Nowadays, the standard approach to integrate datatypes into description logics is to
extend DLs with concrete domains, as first proposed by Baader and Hanschke (1991a) andrecently surveyed by Lutz (2003). More precisely, a concrete domain D consists of a set(such as the natural numbers) and predicates which are associated with a fixed extensionover this set1 (such as the unary =0, the binary <, and the ternary +). The integration ofconcrete domains into, say, the description logic ALC is achieved by adding
1. abstract features, i.e. functional roles;
2. concrete features, i.e. (partial) functions associating values from the concrete domain
(e.g., natural numbers) with logical objects;
3. a concrete domain-based concept constructor.
The DL obtained by extending ALC in this way is called ALC(D), where D denotes aconcrete domain that can be viewed as a parameter to the logic. For example, using asuitable concrete domain D we can describe the constraints formulated above: the concept
Employee
∃employer.∃foundingyear.<1970
∃hiringyear, (employer foundingyear).≥
describes the set of employees who are employed by a company founded before 1970 andwho have a hiring year not prior to the company’s founding year. In this example, the term“∃foundingyear.<1970” is an instance of the concrete domain concept constructor (not to beconfused with the existential value restriction as in ∃employee.Parttime), and so is the thirdconjunct. While <1970 is a unary predicate and thus the former instance only takes oneconcrete feature foundingyear as argument, the second instance uses the binary predicate“≥” requiring two arguments: the concrete feature hiringyear and the sequence of features(employer foundingyear) consisting of the abstract feature employer and the concrete featurefoundingyear.
Concrete domains are rather important in many applications of DLs, including the two
mentioned above:
1. This fixed extension is why these predicates are often called “built-in”.
668

 
Keys, Nominals and Concrete Domains
• The standard way of using description logics for reasoning about conceptual database
models is to translate a given model into a DL representation and then use a DL rea-soner such as FaCT (Horrocks, 1998) or RACER (Haarslev & M¨
oller, 2001) to compute
the consequences of the information provided explicitly in the model. This includesdetecting inconsistencies and inferring additional, implicit containments between en-tities/classes (Calvanese et al., 1998). Since most databases store “concrete” datalike numbers and strings, constraints concerning such data are usually part of theconceptual model and should thus also be captured by the description logic used forreasoning. Indeed, the above example concepts can be viewed as the DL encodingof constraints from a database about companies and their employees. As discussedby Lutz (2002c), description logics with concrete domains are well-suited for concep-tual modeling applications involving concrete datatypes.
• So-called concrete datatypes play a prominent role in the construction of ontolo-
gies (Horrocks et al., 2002). Say, for example, that we want to construct an ontologywhich can be used for describing car dealers’ web pages and web services. In such anontology, concrete datatypes such as prices, manufacturing years, and names of carmodels will doubtlessly be very important. To formulate this ontology using a DL, weneed a way to represent these concrete datatypes. Consequently, almost all DLs thathave been proposed as an ontology language are equipped with some form of concretedomain (Fensel, van Harmelen, Horrocks, McGuinness, & Patel-Schneider, 2001; Hor-rocks et al., 2002; Dean, Connolly, van Harmelen, Hendler, Horrocks, McGuinness,Patel-Schneider, & Stein, 2002). Furthermore, since these ontology languages provideinverse abstract roles and functional restrictions, the users and ontology designerswere quite surprised to find that they do not provide inverse concrete functionalfeatures—which is due to the fact that such features correspond to “concrete keyconstraints”, for which no reasoning algorithms were known and whose effect on thedecidability/complexity was not yet investigated.
In this paper, we propose to further enhance the expressive power of description logics withconcrete domains by extending them with “concrete key constraints”. This extension isuseful both for knowledge representation and for the two applications sketched above. Thefollowing three examples describe the basic idea.
1. Suppose that, in a knowledge representation application, we represent nationalities
by concept names such as US and German and, for US citizens, we store the socialsecurity number using a concrete feature ssn. Then it would be natural to state thatUS citizens are uniquely identified by their social security number, i.e. any two distinctinstances of
Human
∃nationality.US
must have different values for the ssn feature. In our extension of DLs with concretedomains, this can be expressed by using the key assertion2
(ssn keyfor Human
∃nationality.US).
2. Readers familiar with the relationship between DLs and first order logic will notice that this key assertion
is equivalent to ∀x1x2.((V
(Human(x
i∈1,2
i)∧∃z.(nationality(xi, z)∧US(z)))∧¬(x1 = x2)) ⇒ ¬(ssn(x1) =
ssn(x2))).
669

 
Lutz, Areces, Horrocks, & Sattler
2. Returning to our database about companies and employees, it could be useful to
equip every employee with (i) a concrete feature branch storing the branch-ID inwhich she is working and (ii) a concrete feature id storing her personnel-ID. It wouldthen be natural to enforce that the branch-ID together with the personnel-ID uniquelyidentifies employees, even though personnel-IDs are not unique. We can do this byusing the composite key assertion
(branch, id keyfor Employee).
3. In the car dealers’ ontology, we may assume that cars as well as manufacturers are
equipped with identification numbers and that every car is uniquely identified by thecombination of its own identification number and its manufacturers one. To expressthis, we could employ a composite key assertion referring to sequences of features, inthis case (manufacturer id):
(id, (manufacturer id) keyfor Car).
More formally, we propose to extend DLs to provide for concrete domains with key boxes,which are sets of key assertions of the form
(u1, . . . , un keyfor C),
where each ui is a sequence f1 · · · fng of abstract features fj followed by a single concretefeature g, and C is a concept. As the above examples illustrate, the idea of key constraints isvery natural. Since, moreover, keys play an important role in databases and, as mentionedabove, reasoning about database conceptual models is an important, challenging applicationof description logics, several approaches to extend description logics with keys have alreadybeen investigated (Borgida & Weddell, 1997; Calvanese, De Giacomo, & Lenzerini, 2000;Khizder, Toman, & Weddell, 2001). What distinguishes our approach from existing ones,however, is the idea of using concrete domains for constructing key constraints, rather thandefining keys on an abstract, logical level.
The goal of this paper is to provide a comprehensive analysis of the effects on decid-
ability and computational complexity of adding key boxes to description logics with concretedomains. To this end, we extend the two description logics ALC(D) and SHOQ(D) with keyboxes, in this way obtaining ALCK(D) and SHOQK(D), respectively. While the basic DLwith concrete domains ALC(D) has already been discussed above, SHOQ(D) was proposedas an ontology language in (Horrocks & Sattler, 2001). It provides a wealth of expressivepossibilities such as general concept inclusion axioms (GCIs), transitive roles, role hierar-chies, nominals, and qualifying number restrictions. Moreover, it offers a restricted variantof the concrete domain constructor that disallows the use of sequences of features in orderto avoid undecidability of reasoning. The main outcome of our investigations is that keyconstraints can have a dramatic impact on the decidability and complexity of reasoning: forexample, whereas satisfiability of ALC(D)-concepts is known to be PSpace-complete (Lutz,2002b), we will show that satisfiability of ALCK(D)-concepts w.r.t. key boxes is, in general,undecidable. Decidability can be regained if we restrict the concepts used in key boxes
670

 
Keys, Nominals and Concrete Domains
to Boolean combinations of concept names (Boolean key boxes). Interestingly, satisfiabil-ity of ALCK(D)-concepts w.r.t. Boolean key boxes is still NExpTime-complete even forvery simple concrete domains. In the case of SHOQ(D) and SHOQK(D), the leap incomplexity is somewhat less dramatic since SHOQ(D)-concept satisfiability is already Ex-pTime-complete: again, the addition of key boxes results in NExpTime-complete reasoningproblems.
It is interesting to note that there exists a close connection between key assertions
and so-called nominals, i.e. concept names that can have at most one instance, such asPope. Nominals are a standard means of expressivity in description logics and sometimesappear in disguise as the “one-of” operator (Borgida & Patel-Schneider, 1994; Horrockset al., 2002). It is not hard to see that key boxes can “simulate” nominals: if, for example,we use a concrete domain based on the natural numbers and providing unary predicates=n for equality with n ∈ N, then the key assertion (g keyfor
), where
stands for
logical truth, obviously makes the concept ∃g.=n behave like a nominal, for each n ∈N. For this reason, we also consider ALCO(D), the extension of ALC(D) with nominals,and ALCOK(D), the extension of ALCK(D) with nominals.3 Our main result concerningnominals is that, although in general being of lower expressive power than key boxes, theyalready make reasoning NExpTime-hard if combined with concrete domains: there existconcrete domains D such that ALCO(D)-concept satisfiability is NExpTime-complete. Weshould like to stress that this and the other NExpTime-hardness results obtained in thispaper are in accordance with the observation made in (Lutz, 2004) that the PSpace-upperbound for reasoning with ALC(D) is not robust w.r.t. extensions of the logic: there existseveral “seemingly harmless” extensions of ALC(D) (for example with acyclic TBoxes andwith inverse roles) which make the complexity of reasoning leap from PSpace-completenessto NExpTime-completeness for many natural concrete domains.
The remainder of this paper is organized as follows: in Section 2, we formally introduce
concrete domains, key boxes, and the DL ALCOK(D) together with its fragments ALCK(D)and ALCO(D). Moreover, we define Boolean key boxes, which only allow Boolean com-binations of concept names to appear in key definitions. Additionally, we introduce someother important properties of key boxes: path-free key boxes prohibit the use of sequencesof features in key assertions; in unary key boxes, each key assertion involves exactly onesequence of features; and composite key boxes are simply non-unary ones.
Section 3 is devoted to establishing lower bounds for extensions of ALC(D) with key
boxes or nominals. In Section 3.1, we use a reduction of the Post Correspondence Problemto prove that ALCK(D)-concept satisfiability w.r.t. (non-Boolean) key boxes is undecidablefor a large class of concrete domains. We then shift our attention to Boolean key boxessince, in Section 4, we show that this restriction restores decidability.
In Section 3.2,
we introduce a NExpTime-complete variant of the domino problem and three concretedomains that are useful for the reduction of this problem to concept satisfiability in DLswith Boolean key boxes or nominals. In Section 3.3, we use these concrete domains toprove that ALCK(D)-concept satisfiability w.r.t. Boolean, path-free and unary key boxesis NExpTime-hard for some natural concrete domains. In Section 3.4, we prove that thereexist concrete domains D such that ALCO(D)-concept satisfiability without reference to
3. Note that the logic SHOQ(D) already provides for nominals.
671

 
Lutz, Areces, Horrocks, & Sattler
key boxes is already NExpTime-hard; we show that this is true even for some concretedomains that are computationally very simple (PTime) when considered in isolation.
The purpose of Section 4 is to develop reasoning procedures for description logics with
key boxes and to prove upper complexity bounds matching the NExpTime lower boundsestablished in the previous section. We start in Section 4.1 with a tableau algorithm thatdecides ALCOK(D)-concept satisfiability w.r.t. Boolean key boxes, provided that the con-crete domain D is key-admissible. Intuitively, a concrete domain D is key-admissible if thereexists an algorithm that takes a finite conjunction c of predicates from D over some set ofvariables, decides whether this conjunction is satisfiable and, if so, chooses a solution of cand returns the information on which variables take the same values in it. We call suchan algorithm a D-tester. We have chosen a tableau algorithm since this type of reasoningprocedure has the potential to be implemented in efficient reasoners and has been shown tobehave well in practice (Horrocks, Sattler, & Tobies, 2000; Haarslev & M¨
oller, 2001). Our
algorithm implies the following upper complexity bound: if D is a key-admissible concretedomain for which a non-deterministic polynomial time D-tester exists, then ALCO(D)-concept satisfiability w.r.t. Boolean key boxes is in NExpTime.
In Section 4.2, we devise a tableau algorithm for SHOQK(D)-concept satisfiability
w.r.t. path-free key boxes which might involve non-Boolean concepts. For the decidabilityof ALCOK(D), we restricted key boxes to Boolean ones. For SHOQK(D), such a restric-tion is not possible since SHOQ(D) provides TBoxes, and we can thus no longer distinguishbetween Boolean and non-Boolean concepts. On the other hand, it follows from an unde-cidability proof by Baader and Hanschke (1992) that SHOQ(D) is undecidable if we allowfor sequences of features in concrete domain constructors. Thus we restrict key assertionsanalogously to path-free ones, and show that this yields indeed a decidable logic. Its ex-pressive power is orthogonal to the one of ALCOK(D), and our previous undecidabilityresults imply that the combination of ALCOK(D) and SHOQK(D) is undecidable. As aby-product of the correctness proof of the algorithm, we obtain a bounded model prop-erty for SHOQK(D), which implies that SHOQK(D)-concept satisfiability w.r.t. path-freekey boxes is in NExpTime if D is a key-admissible concrete domain for which a non-deterministic polynomial time D-tester exists.
In Section 5, we summarize the results obtained and give an outlook to possible future
research.
2. Description Logics with Concrete Domains
In the following, we introduce the description logic ALCOK(D). Let us start by definingconcrete domains:
Definition 2.1 (Concrete Domain). A concrete domain D is a pair (∆D, ΦD), where ∆Dis a set and ΦD a set of predicate names. Each predicate name P ∈ ΦD is associated withan arity n and an n-ary predicate P D ⊆ ∆n
D.
Based on concrete domains, we can now define ALCOK(D)-concepts and key boxes.
Definition 2.2 (ALCOK(D) Syntax). Let NC, NO, NR, NcF be pairwise disjoint and count-ably infinite sets of concept names, nominals, role names, and concrete features. Further-more, we assume that NR contains a countably infinite subset NaF of abstract features. A
672

 
Keys, Nominals and Concrete Domains
path u is a composition f1 · · · fng of n abstract features f1, . . . , fn (n ≥ 0) and a concretefeature g. Let D be a concrete domain. The set of ALCOK(D)-concepts is the smallest setsuch that
• every concept name and every nominal is a concept, and
• if C and D are concepts, R is a role name, g is a concrete feature, u1, . . . , un are paths,
and P ∈ ΦD is a predicate of arity n, then the following expressions are also concepts:
¬C, C
D, C
D, ∃R.C, ∀R.C, ∃u1, . . . , un.P, and g↑.
A key assertion is an expression
(u1, . . . , uk keyfor C),
where u1, . . . , uk (k ≥ 1) are paths and C is a concept. A finite set of key assertions iscalled a key box.
As usual, we use
as an abbreviation for an arbitrary propositional tautology, ⊥ as an
abbreviation for ¬ , C → D as an abbreviation for ¬C
D, and C ↔ D as an abbreviation
for (C → D)
(D → C). Throughout this paper, we will also consider several fragments
of the description logic ALCOK(D). The DL ALCO(D) is obtained from ALCOK(D) byadmitting only empty key boxes. In particular, the set of ALCO(D)-concepts is just the setof ALCOK(D)-concepts. Furthermore, by disallowing the use of nominals, we obtain thefragment ALC(D) of ALCO(D) and ALCK(D) of ALCOK(D).
The description logic ALCOK(D) is equipped with a Tarski-style set-theoretic semantics.
Along with the semantics, we introduce the two standard inference problems: conceptsatisfiability and concept subsumption.
Definition 2.3 (ALCOK(D) Semantics). An interpretation I is a pair (∆I, ·I), where ∆I isa non-empty set, called the domain, and ·I is the interpretation function. The interpretationfunction maps
• each concept name C to a subset CI of ∆I,
• each nominal N to a singleton subset N I of ∆I,
• each role name R to a subset RI of ∆I × ∆I,
• each abstract feature f to a partial function f I from ∆I to ∆I, and
• each concrete feature g to a partial function gI from ∆I to ∆D.
673

 
Lutz, Areces, Horrocks, & Sattler
If u = f1 · · · fng is a path, then uI(d) is defined as gI(f I · · ·
n
(f I (d)) · · · ). The interpretation
1
function is extended to arbitrary concepts as follows:
(¬C)I := ∆I  CI
(C
D)I := CI ∩ DI
(C
D)I := CI ∪ DI
(∃R.C)I := d ∈ ∆I | There is e ∈ ∆I with (d, e) ∈ RI and e ∈ CI
(∀R.C)I := d ∈ ∆I | For all e ∈ ∆I, if (d, e) ∈ RI, then e ∈ CI
(∃u1, . . . , un.P )I := d ∈ ∆I | ∃x1, . . . , xn ∈ ∆D : uIi(d) = xi and (x1, . . . , xn) ∈ P D
(g↑)I := d ∈ ∆I | gI(d) undefined.
Let I be an interpretation. Then I is a model of a concept C iff CI = ∅. Moreover, Isatisfies a key assertion (u1, . . . , un keyfor C) if, for any a, b ∈ CI,
uI (a) = uI (b), . . . , uI
1
1
n(a) = uI
n(b) implies that a = b.
I is a model of a key box K iff I satisfies all key assertions in K. A concept C is satisfiablew.r.t. a key box K iff C and K have a common model. C is subsumed by a concept D w.r.t.a key box K (written C
K D) iff C I ⊆ DI for all models I of K.
It is well-known that, in description logics providing for all Boolean operators, subsumptioncan be reduced to (un)satisfiability and vice versa: C
K D iff C
¬D is unsatisfiable
w.r.t. K and C is satisfiable w.r.t. K iff C
K ⊥. This allows us to concentrate on concept
satisfiability when devising complexity bounds for reasoning with description logics: lowerand upper complexity bounds for concept satisfiability imply corresponding bounds forconcept subsumption—only for the complementary complexity class.
If decision procedures for description logics with concrete domains are to be devised
without committing to a particular concrete domain, then a well-defined interface betweenthe decision procedure and a concrete domain reasoner is needed. Usually, this interfaceis based on the assumption that the concrete domain is admissible (Baader & Hanschke,1991a; Lutz, 2002a, 2003):
Definition 2.4 (D-conjunction, Admissibility). Let D be a concrete domain and V a setof variables. A D-conjunction is a (finite) predicate conjunction of the form
(i)
c =
(x
, . . . , x(i)) : P
0
n
i,
i
i<k
(i)
where Pi is an ni-ary predicate for i < k and the x
are variables from V. A D-conjunction
j
c is satisfiable iff there exists a function δ mapping the variables in c to elements of ∆D such
(i)
(i)
that (δ(x
), . . . , δ(x
)) ∈ P D for each i < k. Such a function is called a solution for c.
0
ni
i
We say that the concrete domain D is admissible iff
1. ΦD contains a unary predicate
D such that
D
D = ∆D;
2. ΦD is closed under negation, i.e., for each n-ary predicate P ∈ ΦD, there is a predicate
D
P ∈ ΦD of arity n such that P
= ∆n  D
P D;
674

 
Keys, Nominals and Concrete Domains
3. satisfiability of D-conjunctions is decidable.
We refer to the satisfiability of D-conjunctions as D-satisfiability.
As we shall see, it sometimes makes a considerable difference w.r.t. complexity and decid-ability to restrict key boxes in various ways, for example to disallow paths of length greaterthan one. Therefore, we introduce some useful notions.
Definition 2.5 (Boolean, Path-free, Simple). A key box K is called
• Boolean if all concepts appearing in (key assertions in) K are Boolean combinations
of concept names;
• path-free if, for all key assertions (u1, . . . , un keyfor C) in K, u1, . . . , un ∈ NcF;
• simple if it is both path-free and Boolean;
• unary if all key assertions in K are unary key assertions, i.e. of the form (u keyfor C).
A concept C is called path-free if, in all its subconcepts of the form ∃u1, . . . , un.P , u1, . . . , unare concrete features.
To emphasize that a key box might not necessarily be Boolean or path-free, we sometimescall such a key box general. Similarly, to emphasize that a key box is not necessarily aunary key box, we sometimes call such a key box composite.
3. Lower Bounds
In this section, we prove lower complexity bounds for description logics with concrete do-mains and key boxes and/or nominals. In Section 3.1, we start by showing that the satisfi-ability of ALCK(D)-concepts w.r.t. (general) key boxes is undecidable for many interestingconcrete domains. The discouraging picture painted by this result is mitigated by the factthat, in Section 4.1, we shall prove that the restriction to Boolean key boxes restores de-cidability. It is thus interesting to look for lower complexity bounds that apply under thisrestriction. In preparation for this, we introduce in Section 3.2 a NExpTime-complete vari-ant of the domino problem and three concrete domains that are well-suited for reductionsof this problem.
In Section 3.3, we then prove that satisfiability of path-free ALCK(D)-concepts w.r.t.
simple key boxes is NExpTime-hard for a large class of concrete domains D and that, formany concrete domains, this holds even if we restrict key boxes to unary ones. Finally,we consider the description logic ALCO(D) in Section 3.4 and identify several concretedomains such that ALCO(D)-concept satisfiability (without key boxes!) is NExpTime-hard. As we already mentioned, key boxes and nominals are closely related: key boxes canexpress nominals, but are in general more powerful.
3.1 Undecidability of ALCK(D) with General Key Boxes
We prove that satisfiability of ALCK(D)-concepts w.r.t. key boxes is undecidable for alarge class of concrete domains if we allow complex ALCK(D)-concepts to occur in keyassertions. The proof is by a reduction of the well-known undecidable Post CorrespondenceProblem (Post, 1946; Hopcroft & Ullman, 1979).
675

 
Lutz, Areces, Horrocks, & Sattler
Definition 3.1 (PCP). An instance P of the Post Correspondence Problem (PCP) is givenby a finite, non-empty list ( 1, r1), . . . , ( k, rk) of pairs of words over some alphabet Σ. Asequence of integers i1, . . . , im, with m ≥ 1, is called a solution for P if i · · ·
= r · · · r
.
1
im
i1
im
The PCP is to decide whether a given instance P has a solution.
For reducing the PCP to the satisfiability of our DLs, we need an appropriate concretedomain. It is obviously natural to use a concrete domain based on words and concatenation.We will later see that the results obtained for this concrete domain carry over to otherconcrete domains based on numbers and arithmetics. The following concrete domain wasintroduced by Lutz (2004). Its definition presupposes a fixed alphabet Σ that is at leastbinary.
Definition 3.2 (Concrete domain W). The concrete domain W is defined by setting ∆W :=Σ∗ and defining ΦW as the smallest set containing the following predicates:
• unary predicates word and nword with wordW = ∆W and nwordW = ∅,
• unary predicates = and = with =W =   and =W = Σ+,
• a binary equality predicate = and a binary inequality predicate = with the obvious
interpretation, and
• for each w ∈ Σ+, two binary predicates concw and nconcw with
concW
w = (u, v) | v = uw and nconcW
w = (u, v) | v = uw.
It is readily checked that W satisfies properties 1 and 2 of admissibility (see Definition 2.4).Moreover, W-satisfiability is decidable:
Theorem 3.1 (Lutz, 2004). W-satisfiability is in PTime.
Thus, W is admissible and even of low complexity. This is important since our aim isto demonstrate that the undecidability of ALCK(W)-concept satisfiability is due to thepresence of keys, and not due to the high complexity of W-satisfiability.
We can now discuss the reduction of the PCP. A given instance ( 1, r1), . . . , ( k, rk) is
translated into an ALCK(D)-concept CP and key box KP as defined in Figure 1 such thatP has a solution iff CP is unsatisfiable w.r.t. KP . The idea behind the reduction is that acommon model of CP and KP encodes all potential solutions for P (i.e., sequences i1, . . . , inof integers ij between 1 and k) and makes sure that none of them is in fact a solution. InFigure 1, f1, . . . , fk denote abstract features while g, , and r denote concrete features. Thedefinition of the concept Step just serves as an abbreviation and should not be confusedwith so-called TBoxes (see Section 4.2 for the definition of TBoxes). Models of CP and KP ,such as the one displayed in Figure 2, have the form of an infinite k-ary tree whose root isconnected to an “extra node” x via the role R. Intuitively, each node of the tree representsone partial solution i1, . . . , in, its -successor represents the corresponding left concatenation
i · · ·
, and its r-successor the corresponding right concatenation r · · · r .
1
in
i1
in
To enforce the existence of the infinite tree, we employ the key box KP : consider for
example the root node’s f1-successor in Figure 2—let us call this node y. Due to Line 3
676

 
Keys, Nominals and Concrete Domains
Step :=
∃fi.(¬A
∃g.=
∃ , r.=)
1≤i≤k
(∃ , fi .conc
∃r, f
)
i
ir.concri
1≤i≤k
CP := ∃ .=
∃r.=
∃R.(A
∃g.=
¬Step)
Step
KP := g keyfor ¬Step
Figure 1: The ALCK(W) reduction concept CP and key box KP .
R
r
A
=
=
x
∃g.=
conc
f
1
1
f
conc
k
rk
concr conc
1
k
r
r
· · ·
f1
· · ·
fk
f1
· · ·
fk
· · ·
· · ·
Figure 2: An example model of CP and KP .
of CP and Line 1 of Step, we have y ∈ (∃g.= )I. Due to Line 2 of CP , we also havex ∈ (∃g.= )I and x ∈ (¬Step)I , where x is the “extra node” mentioned above. In view ofthe key box KP , this implies that either (i) x = y or (ii) y ∈ StepI. It is easy to see that(i) is impossible since Line 2 of CP and Line 1 of Step imply that x ∈ AI and y ∈ (¬A)I.Hence y ∈ StepI and, by Line 2 of Step, y has the appropriate fi-successors for 1 ≤ i ≤ n.In the same way, the construction of the tree can be continued ad infinitum. The secondline in the definition of Step enforces that I (z) = i · · ·
and rI (z) = r · · · r
for z an
1
in
i1
in
fi · · · f -successor of the root node. Finally, the concept ∃ , r.= in Line 1 of Step implies
1
in
that I (z) = rI (z) holds at all nodes z of the tree (except for the root), which implies thatno potential solution is a solution.
Since the size of CP and KP is clearly polynomial in k and the key box KP is a unary
key box, we obtain the following proposition.
Proposition 3.2. The satisfiability of ALCK(W)-concepts w.r.t. (non-Boolean) path-freeunary key boxes is undecidable.
677

 
Lutz, Areces, Horrocks, & Sattler
To emphasize that this undecidability result was obtained using a very simple concretedomain, let us combine Theorem 3.1 with Proposition 3.2.
Theorem 3.3. There exists a concrete domain D such that D-satisfiability is in PTimeand satisfiability of ALCK(D)-concepts w.r.t. (non-Boolean) path-free unary key boxes isundecidable.
At first sight, the concrete domain W might look artificial and one may question the rel-evance of lower bounds that have been obtained using W. However, it is straightforwardto encode words as natural numbers and to define concatenation of words as rather sim-ple operations on the natural numbers (Baader & Hanschke, 1992): a word w =
over
the alphabet Σ of cardinality Σ can be interpreted as a number written at base Σ + 1in which the symbol that is the “0 digit” does not occur. Hence, we can use the corre-sponding natural number (e.g., in base 10) to represent a word w, and the number 0 torepresent the empty word. The concatenation of two words v and w can then be expressedas vw = v · (Σ + 1)|w| + w, where |w| denotes the length of the word w. Moreover, exponen-tiation can be expressed as multiple multiplications, multiplication as multiple additions,and addition as multiple incrementation: this is shown in Section 5.6 of (Lutz, 2004) forthe case of ALC(D) extended with TBoxes (c.f. Section 4.2) and can easily be adapted toALC(D) with non-Boolean key boxes. This observation gives rise to the following theorem:
Theorem 3.4. Let D be a concrete domain such that N ⊆ ∆D, ΦD contains a unary predi-cate =0 with (=0)D = 0, binary equality and inequality predicates, and a binary predicateincr with incrD ∩ (n, x) | n ∈ N and x ∈ ∆D = (k, k + 1) | k ∈ N. Then satisfiability ofALCK(D)-concepts w.r.t. (non-Boolean) path-free unary key boxes is undecidable.
3.2 Domino Problems and Concrete Domains
In this section, we introduce a NExpTime-complete variant of the well-known, undecidabledomino problem (Berger, 1966; Knuth, 1968), and then define three concrete domains D1,D2, and D3. These concrete domains will be used in Sections 3.3 and 3.4 to establishlower bounds for reasoning with ALCK(D) and Boolean key boxes, and for reasoning withALCO(D).
In general, a domino problem is given by a finite set of tile types. Intuitively, all tile
types are of the same size, each type having a square shape and colored edges. An unlimitednumber of tiles of each type is available. In the NExpTime-hard variant of the dominoproblem that we use, the task is to tile a 2n+1 × 2n+1-torus (i.e., a 2n+1 × 2n+1-rectanglewhose borders are “glued” together) where neighboring edges have the same color.
Definition 3.3 (Domino System). A domino system D is a triple (T, H, V ), where T
N
is a finite set of tile types and H, V ⊆ T × T represent the horizontal and vertical matchingconditions. Let D be a domino system and a = a0, . . . , an−1 an initial condition, i.e. ann-tuple of tiles. A mapping τ : 0, . . . , 2n+1 − 1 × 0, . . . , 2n+1 − 1 → T is a solution forD and a iff, for all x, y < 2n+1, the following holds:
• if τ (x, y) = t and τ (x ⊕2n+1 1, y) = t , then (t, t ) ∈ H
• if τ (x, y) = t and τ (x, y ⊕2n+1 1) = t , then (t, t ) ∈ V
678

 
Keys, Nominals and Concrete Domains
• τ (i, 0) = ai for i < n.
where ⊕i denotes addition modulo i.
It follows from results in (B¨
orger, Gr¨
adel, & Gurevich, 1997) that the above variant of the
domino problem is NExpTime-complete.
We define the concrete domain D1 to be used in the reduction of the NExpTime-
complete domino problem to ALCK(D1)-concept satisfiability w.r.t. Boolean key boxes.
Definition 3.4 (Concrete Domain D1). The concrete domain D1 is defined by setting∆D := 0, 1 and Φ
to the (smallest) set containing the following predicates:
1
D1
• unary predicates
D
with (
)D1 = ∆
and ⊥
with (⊥
)D1 = ∅;
1
D1
D1
D1
D1
• unary predicates =0 and =1 with (=i)D1 = i, i ∈ 0, 1.
The second concrete domain D2 will be used for a reduction of the NExpTime-completedomino problem to ALCK(D2)-concept satisfiability w.r.t. Boolean unary key boxes. Forthis reduction we need to “store” vectors of bits in single concrete domain elements.
Definition 3.5 (Concrete Domain D2). For every n ∈ N, a function v : 0, . . . , n − 1 →0, 1 is called a bit vector of dimension n. We use BVn to denote the set of all bit vectorsof dimension n. The concrete domain D2 is defined by setting ∆D :=
BV
to
2
i>0
i and ΦD2
the (smallest) set containing the following predicates:
• unary predicates
D
with (
)D2 = ∆
and ⊥
with (⊥
)D2 = ∅;
2
D2
D2
D2
D2
• for every k, i ∈ N with i < k, unary predicates bit0i and bit1i with
k
k
(bitni
|
k )D2 = v ∈ ∆D
v ∈ BV
2
k and v(i) = n,
and unary predicates bit0i and bit1i with (bitni )D2 = ∆
 (bitni )D2.
k
k
k
D2
k
The last concrete domain D3 is used in the reduction of the NExpTime-complete dominoproblem to ALCO(D3)-concept satisfiability. In this reduction, the concrete domain D3contains two kinds of elements: firstly, there are elements of ∆D that can represent the
3
whole 2n+1 × 2n+1-torus, so-called domino arrays. Secondly, there are elements of ∆D that
3
represent positions in the torus. For technical reasons to be discussed later, these elementsare vectors of natural numbers rather than bit vectors, and in the following we shall just callthem vectors. A domino array is then a function mapping each pair of vectors (of certainlength) to a natural number which represents a tile type.
Definition 3.6 (Concrete Domain D3). For every k ∈ N, a function v : 0, . . . , k − 1 → Nis called a vector of dimension k. We use VEk to denote the set of all vectors of dimension k.For every k ∈ N, a function k : VEk × VEk → N is called a domino array of dimension k.We use DAk to denote the set of all domino arrays of dimension k. The concrete domain D3is defined by setting ∆D :=
VE
DA
to the (smallest) set containing
3
i>0
i ∪
i>0
i and ΦD3
the following predicates:
• unary predicates
D
with (
)D3 = ∆
and ⊥
with (⊥
)D3 = ∅;
3
D3
D3
D3
D3
679

 
Lutz, Areces, Horrocks, & Sattler
• for every k, i ∈ N with i < k, unary predicates pos0i and pos1i with
k
k
(posni
|
k )D3 = v ∈ ∆D
v ∈ VE
3
k and v(i) = n
and unary predicates pos0i and pos1i with (posni )D3 = ∆
 (posni )D3;
k
k
k
D3
k
• for every k, i ∈ N, a predicate tilei of arity 3 with
k
(tileik)D3 = (vx, vy, d) | vx, vy ∈ VEk, d ∈ DAk, and d(vx, vy) = i
and a predicate tilei of arity 3 with (tilei )D3 = (∆
)3  (tilei )D3 .
k
k
D3
k
The reason for using vectors of natural numbers rather than bit vectors in the definition ofD3 is that we want D3-satisfiability to be of low complexity, preferably in PTime: considerthe D3-conjunction
pos00(x) ∧ pos00(y) ∧ pos00(z) ∧
2
2
2
tile72(x, v, d) ∧ tile82(y, v, d) ∧ tile92(z, v, d).
If we use bit vectors rather than vectors of natural numbers, then the upper line enforcesthat at least two out of the three variables x, y, and z must take the same value. Sincethe value of v is fixed, the lower line makes the conjunction unsatisfiable: it tries to assignthe three different values 7, 8, 9 to two different positions in the domino array. It seemsunlikely that this kind of inconsistency can be detected in polynomial time. This problemis circumvented by using vectors of natural numbers in the definition of D3 (but enforcingthem to be bit vectors in the reduction): in this case, the above conjunction is clearlysatisfiable.
Proposition 3.5. For each i ∈ 1, 2, 3, the concrete domain Di is admissible and satisfi-ability of Di-conjunctions is in PTime.
For D1, this is trivial. For D2, a proof can be found in Appendix A. And for D3, a proofcan be found in (Lutz, Areces, Horrocks, & Sattler, 2002).
3.3 NExpTime-hardness of ALCK(D) with Boolean Key Boxes
In this section, we prove two NExpTime-lower bounds for ALCK(D)-concept satisfiabilityw.r.t. Boolean key boxes by reducing the NExpTime-complete domino problem introducedin the previous section. The first reduction uses the very simple concrete domain D1, butdepends on composite key assertions. The second reduction uses the slightly more complexconcrete domain D2, but only needs unary key assertions. As we will see, the two reductionsyield different, incomparable results.
We first reduce the NExpTime-complete domino problem to ALCK(D1)-concept satisfi-
ability w.r.t. Boolean composite key boxes. Each domino system D = (T, H, V ) with initialcondition a = a0, . . . , an−1 is translated into an ALCK(D1)-concept CD,a as displayed inFigure 3. Names such as TreeX and TreeY are used as abbreviations only. We use ∀Ri.C asan abbreviation for the n-fold nesting ∀R. · · · ∀R.C. The names xposi and yposi used in thefigure denote concrete features. In the definition of the Init concept, for each n ∈ N, biti(n)
680

 
Keys, Nominals and Concrete Domains
TreeX := ∃R.X0
∃R.¬X0
∀Ri.(DistXi−1
∃R.Xi
∃R.¬Xi)
i=1..n
TreeY := DistXn
∃R.Y0
∃R.¬Y0
∀Ri.(DistYi−1
DistXn
∃R.Yi
∃R.¬Yi)
i=1..n
DistXk :=
((Xi → ∀R.Xi)
(¬Xi → ∀R.¬Xi))
i=0..k
DistYk :=
((Yi → ∀R.Yi)
(¬Yi → ∀R.¬Yi))
i=0..k
TransXPos :=
(Xi → ∃xposi. =1)
(¬Xi → ∃xposi. =0)
i=0..n
TransYPos :=
(Yi → ∃yposi. =1)
(¬Yi → ∃yposi. =0)
i=0..n
Succs := ∃Rx.(TransXPos
TransYPos)
∃Ry.(TransXPos
TransYPos)
XSuccOk :=
(Yi → ∀Rx.Yi)
(¬Yi → ∀Rx.¬Yi)
i=0..n
Xj → (Xk → ∀Rx.¬Xk)
(¬Xk → ∀Rx.Xk)
k=0..n
j=0..k
¬Xj → (Xk → ∀Rx.Xk)
(¬Xk → ∀Rx.¬Xk)
k=0..n
j=0..k
YSuccOk :=
(Xi → ∀Ry.Xi)
(¬Xi → ∀Ry.¬Xi)
i=0..n
Yj → (Yk → ∀Ry.¬Yk)
(¬Yk → ∀Ry.Yk)
k=0..n
j=0..k
¬Yj → (Yk → ∀Ry.Yk)
(¬Yk → ∀Ry.¬Yk)
k=0..n
j=0..k
Label :=
Di
¬(Di
Dj)
i∈T
i,j∈T,i=j
CheckMatch :=
(Di
∀Rx.Dj)
(Di
∀Ry.Dj)
(i,j)∈H
(i,j)∈V
Init :=
¬Xj
Xj
¬Yj → Dai
i=0..n−1
j=0..n,bitj (i)=0
j=0..n,bitj (i)=1
j=0..n
CD,a := TreeX
∀Rn+1.TreeY
∀R2(n+1).(TransXPos
TransYPos
Succs
XSuccOk
YSuccOk)
∀R2(n+1).(Label
CheckMatch
Init)
Figure 3: The ALCK(D1) reduction concept CD,a.
is supposed to denote the i’th bit of the binary representation of n. We claim that CD,a issatisfiable w.r.t. the key box
(xpos0, . . . , xposn, ypos0, . . . , yposn keyfor )
iff there exists a solution for D and a. To substantiate this claim, let us go through thereduction and explain the various parts of the concept CD,a. The first step towards under-
681

 
Lutz, Areces, Horrocks, & Sattler
standing the structure of models of CD,a (which is the key to understanding the reductionitself) is to note that the purpose of the first line of CD,a is to enforce a tree structureof depth 2(n + 1), whose leaves correspond to positions in the 2n+1 × 2n+1-torus. Moreprecisely, the TreeX concept guarantees that, in every model I of CD,a, there exists a binarytree of depth n + 1. Moreover, the DistXk concepts (there exists one for each k ∈ 0, . . . , n)ensure that the leaves of this tree are binarily numbered (from 0 to 2n+1 − 1) by the conceptnames X0, . . . , Xn. More precisely, for a domain object d ∈ ∆I, set
1
if d ∈ XI
xpsn(d) = Σn
i
i=0αi(d) ∗ 2i
where
αi(d) =
0
otherwise.
The TreeX and DistX concepts ensure that there exist nodes d0, . . . , d2n+1−1 at level n + 1of the tree such that xpsn(di) = i. Intuitively, this numbering represents the horizontalpositions in the 2n+1 × 2n+1-torus. The vertical positions are coded in a similar way by theY0, . . . , Yn concept names. More specifically, the concepts TreeY, DistX, and DistY ensurethat every di (i ≤ 2n+1 − 1) is the root of another tree, in which (i) every node has thesame “X0, . . . , Xn-configuration” as its root node, and (ii) the leaves are numbered binarilyusing the concept names Y0, . . . , Yn (note that the TreeY concept appears in CD,a inside a∀Rn+1 value restriction). Define
1
if d ∈ Y I
ypsn(d) = Σn
i
i=0βi(d) ∗ 2i
where
βi(d) =
0
otherwise.
In the set of leaf nodes of all the trees enforced by the TreeY concept, there exists, for eachi, j < 2n+1, an object4 ei,j ∈ ∆I such that xpsn(ei,j) = i and ypsn(ei,j) = j, i.e., each ei,jrepresents the position (i, j) in the 2n+1 × 2n+1-torus.
The next step is to translate the individual bits of the numbering of the ei,j-objects,
which are up to now represented by concept names, into concrete domain values. This isdone by the TransXPos and TransYPos concepts which ensure that, for all
≤ n, we have
xposI (ei,j) = 0 if ei,j ∈ ¬X , xposI(ei,j) = 1 if ei,j ∈ X , and similarly for ypos and Y .Since I is a model for the key box
(xpos0, . . . , xposn, ypos0, . . . , yposn keyfor ),
grid positions are uniquely represented by domain elements from (TransXPos
TransYPos)I ,
i.e., if d, e ∈ (TransXPos
TransYPos)I such that xpsn(d) = xpsn(e) and ypsn(d) = yxpsn(e),
then d = e. This fact is used in the concepts Succs, XSuccOk, and YSuccOk to enforce that,for the two roles Rx and Ry and each i, j ≤ n, the following holds:
RI ∩
x
(ei,j × ∆I) = (ei,j, e(i⊕2n+11),j
(∗)
RI ∩
y
(ei,j × ∆I) = (ei,j, ei,(j⊕2n+11).
The Succs concept ensures that, for each ei,j, there exists an Rx-successor and an Ry-successor, and that both are in (TransXPos
TransYPos)I . Let d be an Rx-successor of ei,j.
Then the XSuccOk concept ensures that xpsn(d) = i ⊕2n+1 1 and ypsn(d) = j. Before we
4. It does not matter if there is more than one such object.
682

 
Keys, Nominals and Concrete Domains
explain how it does this, let us note that, since all ei,j are in (TransXPos
TransYPos)I and
the grid positions are uniquely represented by elements of (TransXPos
TransYPos)I , this
implies d = e(i⊕2n+11),j which shows that the upper line of (∗) does indeed hold.
Let us now consider the XSuccOk concept in some more detail. It is essentially the
DL-formulation of the well-known propositional formula
n
k−1
n
k−1
(
xj = 1) → (xk = 1 ↔ xk = 0) ∧
(
xj = 0) → (xk = xk)
k=0 j=0
k=0 j=0
which encodes incrementation modulo 2n+1, i.e., if t is the number (binarily) encoded bythe propositional variables x0, . . . , xn and t is the number encoded by the propositionalvariables x , . . . , x
0
n, then we have t = t + 1 modulo 2n+1 (see B¨
orger et al., 1997). Taking
into account the ∀Rx quantifiers in XSuccOk, it is readily checked that this concept hasjust the desired effect: to ensure that, for every Rx-successor d of ei,j, we have xpsn(d) =xpsn(e(i⊕2n+11),j) = i ⊕2n+1 1. The explanation of YSuccOk and how it enforces the lower
line of (∗) is analogous to the XSuccOk case.
It remains to ensure that every grid position is labeled with precisely one tile and that
the initial condition as well as the horizontal and vertical matching conditions are satisfied.The tiles are represented by concept names Di (where i is from the set of tiles T ) andthe described tasks are accomplished in the standard way by the concepts Label, Init, andCheckMatch.
It is worth noting that the reduction concept is path-free and the key box is simple,
i.e., path-free and Boolean. Path-freeness of concepts is often used to tame the complexityof description logics with concrete domains, although it largely sacrifices their expressivepower (Lutz, 2003; Baader, Lutz, Sturm, & Wolter, 2002b; Haarslev, M¨
oller, & Wessel, 2001;
Horrocks & Sattler, 2001). For example, if ALC(D) is augmented with general TBoxes, thenreasoning with arbitrary concepts is undecidable while reasoning with path-free conceptsis ExpTime-complete if D is admissible and D-satisfiability is in ExpTime (Lutz, 2002a).This “taming approach” does not work in the presence of key boxes since, as we have justseen, satisfiability of ALC(D)-concepts w.r.t. key boxes is (under some natural assumptions)
NExpTime-hard, even if both concept and key box are path-free.
Since the size of CD,a and of the used key box is clearly polynomial in n, we obtain the
following proposition.
Proposition 3.6. The satisfiability of path-free ALCK(D1)-concepts w.r.t. simple key boxesis NExpTime-hard.
It has been shown that (non path-free) ALC(D)-concept satisfiability is PSpace-completeif D-satisfiability is in PSpace (Lutz, 2002b). Hence, it follows from Proposition 3.5 thatALC(D1)-concept satisfiability is PSpace-complete. Thus, there is a rather dramatic in-crease of complexity if key boxes are added to ALC(D1). To stress that this increase is dueto the key boxes themselves and not to the complexity of D1-satisfiability, we reformulateProposition 3.6:
Theorem 3.7. There exists a concrete domain D such that D-satisfiability is in PTime andsatisfiability of path-free ALCK(D)-concepts w.r.t. simple key boxes is NExpTime-hard.
683

 
Lutz, Areces, Horrocks, & Sattler
Succs2 := ∃Rx.TransPos
∃Ry.TransPos
TransPos :=
(Xi → ∃bv.bit1i
)
¬X
)
2(n+1)
i → ∃bv.bit0i2(n+1)
i=0..n
(Yi → ∃bv.bit1n+i+1 )
¬Yi → ∃bv.bit0n+i+1 )
i=0..n
2(n+1)
2(n+1)
CD,a := TreeX
∀Rn+1.TreeY
∀R2(n+1).(TransPos
Succs2
XSuccOk
YSuccOk)
∀R2(n+1).(Label
CheckMatch
Init)
Figure 4: The ALCK(D2) reduction concept CD,a.
Although, due to its very low expressivity, the concrete domain D1 itself is not very naturalfor knowledge representation, it is a fragment of many concrete domains that have beenproposed in the literature (Baader & Hanschke, 1992; Haarslev & M¨
oller, 2001; Lutz, 2003,
2002b). Indeed, the presented reduction strategy can be adapted to several “standard”concrete domains. Let us formulate a (very weak) condition that a concrete domain mustsatisfy in order for the presented reduction strategy to be applicable.
Theorem 3.8. Let D be a concrete domain. If there exist a, b ∈ ∆D with a = b and P1, P2 ∈ΦD such that P D = a and P D = b, then the satisfiability of path-free ALCK(D)-concepts
1
2
w.r.t. simple key boxes is NExpTime-hard.
We now present the second NExpTime-hardness result for ALCK(D)-concept satisfiability.This time, we reduce the NExpTime-complete domino problem to the satisfiability of path-free ALCK(D2)-concepts w.r.t. simple unary key boxes. The reduction is very similar tothe previous one and we only discuss the differences.
In the first reduction, we represented the individual bits of grid positions by individual
concrete features xposi and yposi and used a composite key box to ensure that each pointin the torus is represented by at most one element. In the second reduction, we use a singleconcrete feature bv and represent an entire position (i, j) in the torus using a bit vectorfrom the concrete domain D2. This allows us to enforce the above mentioned uniqueness ofrepresentations using a unary key box.
The modified reduction concept CD,a can be found in Figure 4, where the concepts
TreeX, TreeY, DistXk, DistYk, XSuccOk, YSuccOk, Label, CheckMatch, and Init are definedas in Figure 3. The translation of the position in the torus encoded by X0, . . . , Xn, Y0, . . . , Yninto a bit vector is done by the TransPos concept in a straightforward manner. Given whatwas said about the first reduction, it is not hard to see that CD,a is satisfiable w.r.t. the keybox (bv keyfor
) iff there exists a solution for D and a. We thus obtain the following
proposition.
Proposition 3.9. The satisfiability of path-free ALCK(D2)-concepts w.r.t. simple unarykey boxes is NExpTime-hard.
Again, we relate the NExpTime lower bound to the complexity of D2-satisfiability, whichis determined in Proposition 3.5.
684

 
Keys, Nominals and Concrete Domains
Theorem 3.10. There exists a concrete domain D such that D-satisfiability is in PTimeand the satisfiability of path-free ALCK(D)-concepts w.r.t. simple unary key boxes is NExp-Time-hard.
Since the elements of ∆D are bit vectors, the concrete domain D
2
2 cannot be considered a
natural choice for many application areas. But, in the reduction, D2 can be replaced byseveral natural concrete domains.
The central observation is that we use bit vectors only to injectively translate sequences
of bits into values of the concrete domain, i.e., we translate sequences of 2(n + 1) bits(represented by the concept names X0, . . . , Xn and Y0, . . . , Yn) into elements of ∆D such
2
that, for distinct sequences, the results of the translation are also distinct. Due to thisrestricted use of bit vectors, there are several ways to replace them by natural numbers.For example, we can replace TransPos with the following concept TransPos which ensuresthat, for each d ∈ TransPos I , sI
(d) = xpsn(d) + 2n+1 · ypsn(d):
2n+1
TransPos := ∃zero.=0
∃ti.=2i
(¬X0 → ∃s0.=0)
(X0 → ∃s0.=1)
i=1...2n+1
¬Xi → ∃(si−1, zero, si).+
Xi → ∃(si−1, ti, si).+
i=1..n
¬Yi−(n+1) → ∃(si−1, zero, si).+
(Yi−(n+1) → ∃(si−1, ti, si).+
i=n+1..2n+1
where zero, si, and ti are concrete features, =k (with k ∈ N) denotes a unary predicate withthe obvious extension, and + denotes a ternary addition predicate such that, intuitively,the first two arguments are the addends and the third one is the sum.
I
It is easy to check that, whenever two objects d, e ∈ TransPos
do not agree on the
interpretation of the X0, . . . , Xn, Y0, . . . , Yn, then sI
(d) = sI
(e), and thus the key
2n+1
2n+1
box (s2n+1 keyfor
) can be used for the reduction. The size of TransPos is obviously
polynomial in n if the numbers k appearing in =k predicates are coded in binary. We thusobtain the following theorem:
Theorem 3.11. Let D be a concrete domain such that
1. N ⊆ ∆D,
2. ΦD contains, for each k ∈ N, a predicate =k with (=k)D = k where the size of (the
representation of ) =k is logarithmic in k, and
3. ΦD contains a predicate + with (+)D ∩ (k1, k2, x) | k1, k2 ∈ N and x ∈ ∆D =
(k1, k2, k1 + k2) | k1, k2 ∈ N.
Then the satisfiability of path-free ALCK(D)-concepts w.r.t. simple unary key boxes is
NExpTime-hard.
For example, this theorem yields NExpTime-lower bounds for ALCK(D) instantiated withthe concrete domains proposed in (Baader & Hanschke, 1992; Haarslev & M¨
oller, 2001; Lutz,
2003, 2002b). An alternative to the addition predicate is to use multiplication to injectively
685

 
Lutz, Areces, Horrocks, & Sattler
translate sequences of bits into natural numbers. More precisely, let p1, . . . , p2n+1 be thefirst 2n + 1 prime numbers and define another version of TransPos as follows:
TransPos := ∃one.=1
∃ti.=p
(¬X
i
0 → ∃s0.=0)
(X0 → ∃s0.=1)
i=1...2n+1
¬Xi → ∃(si−1, one, si).∗
Xi → ∃(si−1, ti, si).∗
i=1..n
¬Yi−(n+1) → ∃(si−1, one, si).∗
Yi−(n+1) → ∃(si−1, ti, si).∗
i=n+1..2n+1
where ∗ is a ternary multiplication predicate.
Since the factorization of natural numbers into prime numbers is unique, we can again
use the key box (s2n+1 keyfor
) for the reduction. Moreover, it is well-known that the
k’th prime is polynomial in k (Graham, Knuth, & Patashnik, 1990), and thus the size ofthe concept TransPos is polynomial in n even if the numbers k in =k predicates are codedunarily. We thus obtain another theorem concerning quite natural concrete domains:
Theorem 3.12. Let D be a concrete domain such that
1. N ⊆ ∆D,
2. ΦD contains, for each k ∈ N, a predicate =k with (=k)D = k, and
3. ΦD contains a predicate ∗ with (∗)D ∩ (k1, k2, x) | k1, k2 ∈ N and x ∈ ∆D =
(k1, k2, k1 · k2) | k1, k2 ∈ N.
Then the satisfiability of path-free ALCK(D)-concepts w.r.t. simple unary key boxes is
NExpTime-hard.
3.4 NExpTime-hardness of ALCO(D)
As we already pointed out in Section 1, the relationship between key boxes and nominalsis rather close: the latter can be “simulated” by the former if the concrete domain providespredicates that can be used to uniquely describe elements of ∆D. For example, in ALCK(D1)the concept ∃g.=0 behaves as a nominal if we use the key assertion (g keyfor
). We can
even define n nominals using n single concrete features in unary-key assertions. In thelogics ALCK(D2) and ALCK(D3), a single concrete feature and unary key assertions aresufficient to simulate an arbitrary number of nominals: for example, in ALCK(D2) theconcept C = ∃g.bit00
∃
2
g.bit112 uniquely describes the bit vector (0, 1) ∈ BV2 ⊆ ∆D , i.e.,
2
a ∈ CI implies gI (a) = (0, 1). Obviously, any other bit vector (of any length!) can bedescribed in a similar way.
This illustrates that, for most non-trivial concrete domains D, the logic ALCK(D) is
(at least) as expressive as ALCO(D). Although the converse does not hold, the expressivepower of ALCO(D) is still sufficient to prove NExpTime-hardness of concept satisfiability,provided that a suitable concrete domain D is used. Since ALCO concept satisfiability is
PSpace-complete (Areces, Blackburn, & Marx, 1999), this is yet another example of a DLwhere an even seemingly harmless extension with concrete domains has a dramatic effecton the computational complexity (Lutz, 2003).
686

 
Keys, Nominals and Concrete Domains
Nominal := ∃f.N
XSucc :=
Xj → (Xk ↔ ¬X
¬
k )
Xj → (Xk ↔ Xk)
k=0..n
j=0..k
k=0..n
j=0..k
YSucc :=
Yj → (Yk ↔ ¬Y
¬
k )
Yj → (Yk ↔ Yk)
k=0..n
j=0..k
k=0..n
j=0..k
TransXPos :=
(Xi → ∃bvx.pos1in+1)
(¬Xi → ∃bvx.pos0in+1)
i=0..n
TransYPos :=
(Yi → ∃bvy.pos1in+1)
(¬Yi → ∃bvy.pos0in+1)
i=0..n
TransXSucc :=
(X → ∃
→ ∃
i
bvxs.pos1in+1)
(¬Xi
bvxs.pos0in+1)
i=0..n
TransYSucc :=
(Y → ∃
→ ∃
i
bvys.pos1in+1)
(¬Yi
bvys.pos0in+1)
i=0..n
CheckHMatch :=
(∃(bvx, bvy, f ◦ darr).tilei
∃
n+1
(bvxs, bvy, f ◦ darr).tilej
)
n+1
i,j∈H
CheckVMatch :=
(∃(bvx, bvy, f ◦ darr).tilei
∃
n+1
(bvx, bvys, f ◦ darr).tilej
)
n+1
i,j∈V
Init2 :=
¬Xj
Xj
¬Yj
i=0..n−1
j=0..n,bitj (i)=0
j=0..n,bitj (i)=1
j=0..n
→ ∃(bvx, bvy, f ◦ darr).tileai
n+1
CD,a := TreeX
∀Rn+1.TreeY
∀R2(n+1).Nominal
∀R2(n+1).(TransXPos
TransYPos
XSucc
YSucc
TransXSucc
TransYSucc
Init2
CheckHMatch
CheckVMatch)
Figure 5: The ALCO(D3) reduction concept CD,a.
In this section, we reduce the NExpTime-complete domino-problem to ALCO(D3)-
concept satisfiability. Again, let D = (T, H, V ) be a domino system and a = a0, . . . , an−1an initial condition. The modified reduction concept CD,a is defined in Figure 5, where bvx,bvy, bvxs, bvys, and darr denote concrete features, N denotes a nominal, and the conceptsTreeX, TreeY, DistXk, and DistYk are defined as in Figure 3. As in the previous reductions,we now give a detailed explanation of the reduction strategy to show that CD,a is satisfiableiff there exists a solution for D and a. Formal details can then easily be worked out by theinterested reader.
Let I be a model for CD,a. To explain the structure of I, it is convenient to start
with the first line of CD,a. As in the previous reductions, the TreeX and TreeY conceptsare used to ensure that I contains a tree-shaped substructure of depth n + 1 whose leafnodes are the roots of additional trees of depth n + 1 such that the set of the leafs of the
687

 
Lutz, Areces, Horrocks, & Sattler
TreeX
...
TreeY
TreeY
TreeY
...
...
f
...
f
f
N
darr
Figure 6: The structure of models of CD,a.
latter trees correspond to the positions in the 2n+1 × 2n+1-torus, i.e., for each position,there is a leaf node representing it. The torus positions are binarily encoded by the conceptnames X0, . . . , Xn and Y0, . . . , Yn and we use ei,j to refer to the leaf with xpsn(ei,j) = i andypsn(ei,j) = j (see Section 3.3).
As in the previous reductions, the numbers coded by X0, . . . , Xn and Y0, . . . , Yn are
translated into concrete domain values, which is done by the TransXPos and TransYPosconcepts. Note that, in contrast to the ALCK(D2)-reduction, the x-position and the y-position are not stored in the same bit vector, but rather in the two distinct ones bvxand bvy. Also in contrast to the previous reduction, the actual tiling of the torus is notrepresented by the leaf nodes ei,j, but rather by a domino array: the last conjunct in thefirst line of CD,a ensures that every leaf ei,j is connected via the abstract feature f to the(unique) element w ∈ N I .The domain element w is associated with a domino array via the concrete feature darr (aswe shall see later, this is guaranteed by the CheckHMatch and CheckVMatch concepts). Thisdomino array represents the tiling of the 2n+1 × 2n+1-torus. Summing up, the structure ofI is roughly as shown in Figure 6.
Since the tiling is stored in a domino array, we need to explain the purpose of the leaf
nodes ei,j: these nodes are used to enforce the initial condition and the horizontal andvertical matching condition. Let us discuss the horizontal matching condition (the verticalmatching condition is enforced analogously): the XSucc concept is the DL reformulationof the propositional logic formula for incrementation modulo 2n+1 and ensures that, foreach ei,j, the concept names X , . . . , X
0
n encode the number i ⊕2n+1 1, i.e., the horizontal
position of ei,j’s horizontal neighbor. In addition to the storage of the horizontal and verticalposition of ei,j in bvx(ei,j) and bvy(ei,j), we also store the horizontal position i⊕2n+1 1 of ei,j’shorizontal successor in bvxs(ei,j). Finally, CheckHMatch verifies that the tiles at positions
688

 
Keys, Nominals and Concrete Domains
(i, j) and (i ⊕2n+1 1, j), which are both stored in the domino array, are compatible with thehorizontal matching condition.
Note that CheckHMatch also ensures that the domain element w (with w = N I ) has
a domino array attached via the concrete feature darr and that, for each position (i, j), the(unique!) tile stored in the domino array is from the set T . The initial condition is ensuredvia the Init2 concept in a similar way. We (again) use bitj(i) to denote the j’th bit of thebinary encoding of the natural number i.
Using the above considerations, the correctness of the reduction is readily checked.
Moreover, the size of CD,a is at most polynomial in n. Note that CD,a is not path-free:paths of length two appear in the concepts CheckHMatch, CheckVMatch, and Init2. Summingup, the reduction described yields the following result:
Proposition 3.13. The satisfiability of ALCO(D3)-concepts is NExpTime-hard.
Again, we relate the NExpTime lower bound to the complexity of D3-satisfiability, whichis determined in Proposition 3.5.
Theorem 3.14. There exists a concrete domain D such that D-satisfiability is in PTimeand the satisfiability of ALCO(D)-concepts is NExpTime-hard.
Note that the reduction uses only a single nominal N . This is a dramatic increase of com-plexity since it has been shown that satisfiability of ALC(D)-concepts (i.e., without nominalsand key boxes) is PSpace-complete provided that D is admissible and D-satisfiability is inPSpace (Lutz, 2002b).
As in previous sections, we note that D3 can be replaced by more natural concrete
domains in the NExpTime-hardness proof presented. The idea is to represent the wholedomino array by a single natural number and then to use arithmetic operations to access theindividual positions: a natural number k can be viewed as a domino array by partitioningits binary representation into 2n+1 · 2n+1 = 22(n+1) “sections” of length log(T ) , whereT denotes the cardinality of the set of tile types T . Each such section describes the tileof a single position in the torus. The sections can be accessed by using integer divisionand reminder operations: if k is the natural number representing the torus, then the tile ofposisition i is computed by
(k div 2i· log(T ) ) mod 2 log(T ) + 1.
Thus, we introduce ternary predicates div for integer division and mod for computing theremainder of a division, and a binary predicate 2x expressing exponentiation with basis 2.Then we modify the reduction as follows: we replace TransXPos and TransYPos by theTransPos concept from Section 3.3 to translate the two numbers encoded by X1, . . . , Xnand Y1, . . . , Yn into a single natural number that is stored in the concrete feature s2n+1. Wethen devise a new concept Tile[i] (for each i ∈ T ) enforcing that the position identified bythe feature s2n+1 is labeled with tile i:
Tile[i] := ∃r.= log(T )
∃s2n+1, r, r .∗
∃r , r .2x
∃one.=1
∃r, one, t.+
∃t, t .2x
∃f torus, r , u.div
∃u, t , tile.mod
∃tile.=i.
689

 
Lutz, Areces, Horrocks, & Sattler
Here, r, r , r , t, t , u, one, torus, and tile are concrete features. The torus feature is the coun-terpart of the darr feature in the original reduction, i.e., it stores the natural number thatrepresents the tiling array. We can use the Tile[i] concept in the obvious way inside theCheckHMatch, CheckVMatch, and Init2 concepts. The size of the resulting reduction conceptis polynomial in n if the numbers k appearing in =k predicates are coded in binary. Wethus obtain the following theorem:
Theorem 3.15. Let D be a concrete domain such that
1. N ⊆ ∆D,
2. ΦD contains the predicates a predicate =k (for each k ∈ N), 2x, +, ∗, div, mod with
the following extensions
(=k)D = k
(2x)D ∩ (k, x) | k ∈ N and x ∈ ∆D = (k, 2k) | k ∈ N
(+)D ∩ (k1, k2, x) | k1, k2 ∈ N and x ∈ ∆D = (k1, k2, k1 + k2) | k1, k2 ∈ N
(∗)D ∩ (k1, k2, x) | k1, k2 ∈ N and x ∈ ∆D = (k1, k2, k1 · k2) | k1, k2 ∈ N
(div)D ∩ (k1, k2, x) | k1, k2 ∈ N and x ∈ ∆D = (k1, k2, k1 div k2) | k1, k2 ∈ N
(mod)D ∩ (k1, k2, x) | k1, k2 ∈ N and x ∈ ∆D = (k1, k2, k1 mod k2) | k1, k2 ∈ N
Then the satisfiability of ALCO(D)-concepts is NExpTime-hard.
4. Reasoning Procedures
This section is devoted to developing reasoning procedures for DLs with concrete domains,nominals, and keys. We start with devising a tableau algorithm that decides the satisfiabilityof ALCOK(D)-concepts w.r.t. Boolean key boxes. This algorithm yields a NExpTime uppercomplexity bound matching the lower bounds established in Section 3.3.
Then we consider the rather powerful description logic SHOQK(D). This DL, which is
an extension of SHOQ(D) (Horrocks & Sattler, 2001; Pan & Horrocks, 2002), provides awealth of expressive means such as transitive roles, role hierarchies, nominals, and qualifyingnumber restrictions. Moreover, SHOQK(D) is equipped with a restricted variant of theconcrete domain constructor and with key boxes.
We develop a tableau algorithm for
deciding the satisfiability of SHOQK(D)-concepts w.r.t. path-free key boxes. Due to therestrictedness of SHOQK(D)’s concrete domain constructor, we can even admit generalrather than only Boolean key boxes. Again, the algorithm yields a tight NExpTime uppercomplexity bound.
4.1 A Tableau Algorithm for ALCOK(D) with Boolean Key Boxes
Tableau algorithms decide the satisfiability of the input concept (in our case w.r.t. the inputkey box) by attempting to construct a model for it. More precisely, a tableau algorithmstarts with an initial data structure induced by the input concept and then repeatedly ap-plies so-called completion rules to it. This rule application can be thought of as attemptingto construct a model for the input concept. Finally, either the algorithm will find an obvi-ous contradiction or it will encounter a situation that is contradiction-free and in which no
690

 
Keys, Nominals and Concrete Domains
more completion rules are applicable. In the former case, the input concept is unsatisfiable,while it is satisfiable in the latter.
When devising a tableau algorithm for a description logic with concrete domains but
without committing to a particular concrete domain, it is commonly assumed that the con-crete domain is admissible, which implies decidability of the satisfiability of D-conjunctions.In the presence of keys, however, this is not enough: if a D-conjunction is satisfiable, we alsowant to know which of its variables take the same values in an arbitrary but fixed solution.As an example, consider the concrete domain N = (N, <n| n ∈ N) and the N-conjunction
c = <2(v1) ∧ <2(v2) ∧ <2(v3).
Obviously, one solution δ for c satisfies δ(v1) = δ(v2), another satisfies δ(v1) = δ(v3), and soon. Our tableau algorithm uses such identity information passed from the concrete domainreasoner since, in the presence of key boxes, it can have an impact on the structure of theconstructed model. For example, this information reveals the unsatisfiability of
∃R.A
∃R.(¬A
B)
∃R.(¬A
¬B)
∀R.∃g.<2 w.r.t. (g keyfor
).
To formalize this requirement, we strengthen the notion of admissibility into key-admissibility.Since the tableau algorithm developed in this section is non-deterministic, we formulate key-admissibility in a non-deterministic way.
Definition 4.1 (Key-admissible). A concrete domain D is key-admissible iff it satisfies thefollowing properties:
1. ΦD contains a name
D for ∆D;
2. ΦD is closed under negation;
3. there exists an algorithm that takes as input a D-conjunction c, returns clash if c is
unsatisfiable, and otherwise non-deterministically outputs an equivalence relation ∼on the set of variables V used in c such that there exists a solution δ for c with thefollowing property: for all v, v ∈ V
δ(v) = δ(v ) iff v ∼ v .
An algorithm showing the behaviour described in item 3 above is called a D-tester, andthe equivalence relations ∼ are called concrete equivalences.
We say that extended D-
satisfiability is in NP if there exists a D-tester running in polynomial time.
Please note that key-admissibility is less esoteric than it might seem: any concrete domainthat is admissible and provides for an equality predicate is also key-admissible. Due toadmissibility, the presence of an equality predicate implies that an inequality predicate isalso available. We can thus construct a D-tester from an algorithm for D-satisfiability:when presented with a predicate conjunction c, we simply “guess” an equivalence relation∼ on the set of variables used in c. Then we decide the (non-extended) satisfiability ofthe conjunction c ∧
=(v, v ) ∧
=(v, v ), return clash if it is unsatisfiable and
v∼v
v∼v
∼ otherwise. The rather weak condition that an equality predicate should be present is
691

 
Lutz, Areces, Horrocks, & Sattler
¬(C
D)
¬C
¬D ¬(C
D)
¬C
¬D
¬¬C
C
¬(∃R.C)
∀R.¬C
¬(∀R.C)
∃R.¬C
¬(∃u1, . . . , un.P )
∃u1, . . . , un.P
u1↑
· · ·
un↑
¬(g↑)
∃g. D
Figure 7: The NNF rewrite rules.
satisfied by almost all concrete domains proposed in the literature (see, e.g. (Lutz, 2003;Baader & Hanschke, 1991b; Kamp & Wache, 1996; Haarslev, Lutz, & M¨
oller, 1998; Baader
& Sattler, 1998)).
Throughout this chapter, we assume that any concrete domain is equipped with an
equality predicate. This assumption is w.l.o.g. since any D-conjunction using equality canbe translated into an equivalent one without equality by identifying variables according tothe stated equalities. This assumption must not be confused with what was discussed in theprevious paragraph: even if the concrete domain D is admissible and its set of predicates isthus closed under negation, this assumption does not imply the presence of an inequalitypredicate.
We need some more prerequisites before we can start the presentation of the tableau
algorithm: a concept is in negation normal form (NNF) if negation occurs only in front ofconcept names and nominals. It is easily seen that, if the concrete domain D is admissible,then every ALCOK(D)-concept can be converted into an equivalent one in NNF by exhaus-tively applying the rewrite rules displayed in Figure 7. We use ˙
¬ C to denote the result of
converting ¬C to NNF. A key box is in NNF if all concepts occurring in key assertions arein NNF. In what follows, we generally assume input concepts and key boxes to be in NNF.Let C be an ALCOK(D)-concept and K a key box. We use sub(C) to denote the set ofsubconcepts of C (including C itself) and con(K) to denote the set of concepts appearingon the right-hand side of key assertions in K. For a set of concepts Γ, sub(Γ) denotes theset
sub(C). Moreover, we write cl(C, K) as abbreviation for the set
C∈Γ
sub(C) ∪ sub(con(K)) ∪  ˙
¬D | D ∈ sub(con(K)).
We now start the presentation of the tableau algorithm by introducing the underlying datastructure.
Definition 4.2 (Completion System). Let Oa and Oc be disjoint and countably infinitesets of abstract and concrete nodes. A completion tree for an ALCOK(D)-concept C and akey box K is a finite, labeled tree T = (Va, Vc, E, L) with nodes Va ∪ Vc such that Va ⊆ Oa,Vc ⊆ Oc, and all nodes from Vc are leaves. The tree is labeled as follows:
• each node a ∈ Va is labeled with a subset L(a) of cl(C, K);
• each edge (a, b) ∈ E with a, b ∈ Va is labeled with a role name L(a, b) occurring in C
or K;
• each edge (a, x) ∈ E with a ∈ Va and x ∈ Vc is labeled with a concrete feature L(a, x)
occurring in C or K.
692

 
Keys, Nominals and Concrete Domains
For a ∈ Va, we use levT(a) to denote the depth at which a occurs in T (starting with theroot node on depth 0). A completion system for an ALCOK(D)-concept C and a key boxK is a tuple (T, P,
, ∼), where
• T = (Va, Vc, E, L) is a completion tree for C and K,
• P is a function mapping each P ∈ ΦD of arity n in C to a subset of V n
c ,
•
is a linear ordering of Va such that levT(a) ≤ levT(b) implies a
b, and
• ∼ is an equivalence relation on Vc.
Let (Va, Vc, E, L) be a completion tree. A node b ∈ Va is an R-successor of a node a ∈ Vaif (a, b) ∈ E and L(a, b) = R, while a node x ∈ Vc is a g-successor of a if (a, x) ∈ E andL(a, x) = g. For a path u, the notion of u-successor is defined in the obvious way.
Intuitively, the relation ∼ records equalities between concrete nodes found during the
(non-deterministic) model construction process. The recording is necessary since equali-ties between concrete nodes can induce equalities between abstract nodes which, in turn,can imply more equalities between concrete nodes. This can be seen in the following ex-ample: assume the completion tree contains, for i ∈ 1, 2, an abstract node ai with aconcrete g-successor xi and a concrete g -successor yi. Now assume that the key box con-tains (g keyfor
), and that the D-tester returns x1 ∼ x2. As a consequence, a1 and a2
represent the same element and thus functionality of g implies that also y1 and y2 representthe same (concrete) element. To deal with such effects, we define an equivalence relation≈a on abstract nodes and a second equivalence relation ≈c on concrete nodes.
Definition 4.3 (≈a and ≈c Relations). Let S = (T, P, , ∼) be a completion system fora concept C and a key box K with T = (Va, Vc, E, L), and let ≈ be an equivalence relationon Va. For each R ∈ NR, a node b ∈ Va is an R/≈-neighbor of a node a ∈ Va if there existsa node c ∈ Va such that a ≈ c and b is an R-successor of c. Similarly, for each g ∈ NcF, anode x ∈ Vc is a g/≈-neighbor of a if there exists a node c ∈ Va such that a ≈ c and x is ag-successor of c. For paths u, the notion of u/≈-neighbor is defined in the obvious way.
We define a sequence of equivalence relations ≈0 ⊆ ≈1 ⊆ · · ·
a
a
on Va as follows:
≈0
 ∪
a
=
(a, a) ∈ V 2
a
(a, b) ∈ V 2 |
a
there is an N ∈ NO such that N ∈ L(a) ∩ L(b)
≈i+1
∪
a
=
≈ia(a, b) ∈ V 2 |
a
there is a c ∈ Va and an f ∈ NaF such that
a and b are f /≈ia-neighbors of c ∪
(a, b) ∈ V 2 |
a
there is a (u1, . . . , un keyfor C) ∈ K,
ui/≈ia-neighbors xi of a for 1 ≤ i ≤ n, andui/≈ia-neighbors yi of b for 1 ≤ i ≤ nsuch that C ∈ L(a) ∩ L(b) and xi ∼ yi for 1 ≤ i ≤ n.
Finally, set ≈a =
≈i
i≥0
a. Then define
≈c = ∼ ∪ (x, y) ∈ V 2 |
c
there is an a ∈ Va and a g ∈ NcF such that
x and y are g/≈a-neighbors of a.
693

 
Lutz, Areces, Horrocks, & Sattler
This definition reflects the above mentioned tight coupling between the concrete and ab-stract equalities: if the D-tester finds (or guesses) that two concrete nodes are equal, thetableau algorithm may use this to deduce (via the computation of ≈a and ≈c) even moreequalities between concrete nodes.
Let D be a key-admissible concrete domain. To decide the satisfiability of an ALCOK(D)-
concept C0 w.r.t. a Boolean key box K (both in NNF), the tableau algorithm is started withthe initial completion tree
TC = (a
0
0, ∅, ∅, a0 → C0)
in the initial completion system
SC = (T , P
0
C0
∅, ∅, ∅),
where P∅ maps each P ∈ ΦD occurring in C0 to ∅. We now introduce an operation that isused by the completion rules to add new nodes to completion trees.
Definition 4.4 (“+” Operation). An abstract or concrete node is called fresh in a comple-tion tree T if it does not appear in T. Let S = (T, P,
, ∼) be a completion system with
T = (Va, Vc, E, L). We use the following notions:
• Let a ∈ Va, b ∈ Oa fresh in T, and R ∈ NR. We write S +aRb to denote the completion
system S that can be obtained from S by adding b to Va and (a, b) to E and settingL(a, b) = R and L(b) = ∅. Moreover, b is inserted into
such that b
c implies
levT(b) ≤ levT(c).
• Let a ∈ Va, x ∈ Oc fresh in T and g ∈ NcF. We write S +agx to denote the completion
system S that can be obtained from S by adding x to Vc and (a, x) to E and settingL(a, x) = g.
When nesting the + operation, we omit brackets, writing, for example, S + aR1b + bR2c for(S + aR1b) + bR2c. Let u = f1 · · · fng be a path. When a ∈ Va and x ∈ Oc is fresh in T,we use S + aux to denote the completion system that is obtained from S by taking distinctnodes b1, . . . , bn ∈ Oa which are fresh in T and setting
S + aux
:=
S + af1b1 + · · · + bn−1fnbn + bngx.
Strictly speaking, the S + aRb operation is non-deterministic since we did not specify howprecisely the node b is inserted into
. However, since this is don’t care non-determinism,
we will view the “+” operation as being deterministic.
The completion rules can be found in Figure 8. Note that the R
and Rch rules are
non-deterministic, i.e., they have more than one possible outcome (this is true don’t knownon-determinism). Some further remarks on the completion rules are in order: the upperfive rules are well-known from existing tableau algorithms for ALC(D)-concept satisfiability(see, e.g., Lutz, 2002a). Only the use of R/ ≈a-neighbors and u/ ≈a-neighbors in the rulesR∀, R∃, and R∃c deserves a comment. Take for example R∀: intuitively, if we have a ≈a bfor two abstract nodes a and b of the completion tree, then a and b describe the samedomain element of the constructed model (and similarly for the ≈c relation on concrete
694

 
Keys, Nominals and Concrete Domains
R
if C1
C2 ∈ L(a) and C1, C2 ⊆ L(a)
then L(a) := L(a) ∪ C1, C2
R
if C1
C2 ∈ L(a) and C1, C2 ∩ L(a) = ∅
then L(a) := L(a) ∪ C for some C ∈ C1, C2
R∃
if ∃R.C ∈ L(a) and there is no R/≈a-neighbor b of a such that C ∈ L(b),then set S := S + aRb for a fresh b ∈ Oa and L(b) := C
R∀
if ∀R.C ∈ L(a), b is an R/≈a-neighbor of a, and C /
∈ L(b)
then set L(b) := L(b) ∪ C
R∃c
if ∃u1, . . . , un.P ∈ L(a) and there exist no x1, . . . , xn ∈ Vc such that
xi is ui/≈a-neighbor of a for 1 ≤ i ≤ n and (x1, . . . , xn) ∈ P(P )
then set S := (S + au1x1 + · · · + aunxn) with x1, . . . , xn ∈ Oc fresh
and P(P ) := P(P ) ∪ (x1, . . . , xn)
Rch
if (u1, . . . , un keyfor C) ∈ K and there exist x1, . . . , xn ∈ Vc such that
xi is ui/≈a-neighbor of a for 1 ≤ i ≤ n and C, ˙¬C ∩ L(a) = ∅
then set L(a) := L(a) ∪ D for some D ∈ C, ˙
¬C
Rp
if L(b) ⊆ L(a) and a ∈ Va is minimal w.r.t.
such that a ≈a b
then set L(a) := L(a) ∪ L(b)
Figure 8: Completion rules for ALCOK(D).
nodes). Thus if a ≈a b and c is an R-successor of a, then c should also be an R-successorof b. However, since we want the completion tree to be a tree, we do not make the lattersuccessorship explicit. To compensate for this, the R∀ rule talks about R/≈a-neighborsrather than about R-successors.
The lower two rules are necessary for dealing with key boxes.
The Rch rule is a
so-called “choose rule” (Hollunder & Baader, 1991; Horrocks et al., 2000): intuitively,it guesses whether or not an abstract node a satisfies C if there exists a key assertion(u1, . . . , un keyfor C) ∈ K such that there are neighbors of a for all the paths ui. This isnecessary since both possibilities may have ramifications: if a satisfies C, then it must betaken into account in the construction of the relation ≈a; if a does not satisfy C, then wemust deal with the consequences of it satisfying ˙
¬C (e.g. in case that C is
).
The Rp rule deals with equalities between abstract nodes as recorded by the ≈a relation:
since a ≈a b means that a and b describe the same node in the constructed model, theirnode labels should be identical. It suffices, however, to choose one representative for eachequivalence class of ≈a and make sure that this representative’s node label contains thelabels of all its ≈a-equivalent nodes. As the representative, we use the node that is minimalw.r.t. the ordering
, which has been introduced solely for this reason. The Rp rule does
the appropriate copying of node labels.
Let us now formalize what it means for a completion system to contain a contradiction.
Definition 4.5 (Clash). Let S = (T, P,
, ∼) be a completion system for a concept C and
a key box K with T = (Va, Vc, , ∼). We say that the completion system S is concrete
695

 
Lutz, Areces, Horrocks, & Sattler
define procedure sat(S)
do
if S contains a clash then
return unsatisfiable
∼ := test(ζS)compute ≈acompute ≈c
while ∼ = ≈cif S contains a clash then
return unsatisfiable
if S is complete then
return satisfiable
S := the application of a completion rule to Sreturn sat(S )
Figure 9: The ALCOK(D) tableau algorithm.
domain satisfiable iff the conjunction
ζS
=
P (x1, . . . , xn) ∧
=(x, y)
P used in C (x
x≈
1,...,xn)∈P (P )
cy
is satisfiable. S is said to contain a clash iff
1. there is an a ∈ Va and an A ∈ NC such that A, ¬A ⊆ L(a),
2. there are a ∈ Va and x ∈ Vc such that g↑ ∈ L(a) and x is g/≈a-neighbor of a,
3. S is not concrete domain satisfiable.
If S does not contain a clash, S is called clash-free. S is called complete iff no completionrule is applicable to S.
The tableau algorithm is described in Figure 9 in pseudo-code notation. In this figure, testcalls a D-tester as specified in Definition 4.1. Let us say a few words about the while loop.There obviously exist close relationships between the relations ∼ and ≈c and the predicateconjunction ζS:
• ∼ ⊆ ≈c (note that both ≈a and ≈c depend on ∼ and are thus recomputed in each
step of the while loop);
• by definition of ζS and D-tester, the result of test(ζS) yields a relation containing ≈c
(and thus also ∼).
Using these facts, one may check that, in each step of the while loop, new tuples are addedto the ∼ relation, but none are deleted (see the proof of Lemma B.2 in the appendix).The while loop is needed because (i) ≈a is defined using ∼, (ii), ≈c is defined using ≈a,
696

 
Keys, Nominals and Concrete Domains
and (iii) new concrete equalities in ≈c may then imply even more concrete and/or abstractequalities, and so on.
A similar concrete-abstract interplay takes place in the course of several recursion steps:
equalities between concrete nodes provided by the D-tester may make new rules applicable(for example Rp and R∃c) which changes P and thus also ζS. This may subsequently lead tothe detection of more equalities between concrete nodes by the D-tester, and so on. Theseconsiderations show that, in the presence of keys, there exists a close interplay between theconcrete domain reasoner and the tableau algorithm, which is not needed if keys are notpresent: without keys, it suffices to apply the concrete domain satisfiability check only onceafter the completion rules have been exhaustively applied (Baader & Hanschke, 1991a).
The detailed proof of termination, soundness, and completeness together with a com-
plexity analysis of the tableau algorithm defined in this section is given in Appendix B.
Theorem 4.1. Let D be a key-admissible concrete domain. If extended D-satisfiability isin NP, then ALCOK(D)-concept satisfiability w.r.t. Boolean key boxes is in NExpTime.
We should note that, in the way it is presented here, the algorithm leaves considerableroom for optimizations. One possible optimization concerns the “re-use” of f -successors(for abstract features f ): for example, when applying the R∃ rule to a concept ∃f.C ∈ L(a),where a already has an f -successor b, we could simply add C to L(b) instead of adding anew f -successor c and recording that b ≈a c.
Another candidate for optimizations is the test function. Recall that this function takes a
predicate conjunction c with set of variables V and non-deterministically returns a concreteequivalence, i.e., a relation ∼ such that there exists a solution δ for c with vi ∼ vj iffδ(vi) = δ(vj) (see Definition 4.1). It is not hard to devise an ALC(D)-concept that forcescompletion systems to have exponentially many concrete nodes by slightly adapting well-known ALC-concepts that require models of exponential size (Halpern & Moses, 1992).Hence, the size of input conjunctions c to test can be exponential in the size of the inputconcept. Even for trivial D-conjunctions
c =
D(v1) ∧ · · · ∧
D(vk)
we have an exponential number of distinct concrete equivalences ∼. Thus, the number ofpossible outcomes of a call to the test function may be double exponential in the size ofthe input concept. Considering the above example, a natural response to this problem isto require test to return only minimal concrete equivalences: intuitively, an equivalence isminimal if only those variables are equivalent whose equality is enforced by the conjunction.
More precisely, ∼ is called minimal if there exists no concrete equivalence ∼ such that
(x, y) | x ∼ y ⊂ (x, y) | x ∼ y. We conjecture that restricting test in this way doesnot destroy the soundness and completeness of the tableau algorithm. However, althoughthis definitely is a worthwhile optimization, it does not help to overcome the existence ofdoubly exponentially many outcomes of test in the worst case—at least not for all concretedomains D: consider the concrete domain N from Page 691 and conjunctions of the form
ci = <i(v1) ∧ · · · ∧ <i(v2i).
It is readily checked that, for each i ≥ 1, the number of minimal concrete equivalences forci is exponential in i. Moreover, it is not hard to devise a concept Ci of size logarithmic
697

 
Lutz, Areces, Horrocks, & Sattler
in i that leads to completion systems S such that ζS = ci. Hence, there are still doublyexponentially many possible outcomes of the test function.
In the example just discussed, the exponential branching of test is clearly due to the
discreteness of the natural numbers. Indeed, if we use a dense structure for defining concretedomains, it seems that the restriction to minimal concrete equivalences can have the desiredeffect, namely that the number of test’s possible outcomes becomes polynomial in the sizeof its input and thus exponential in the size of the input concept. For example, considerthe concrete domain Q, which is defined as follows:
• ∆Q is the set Q of rational numbers;
• ΦQ contains unary predicates
Q and its negation ⊥Q, unary predicates =q and =q
for each q ∈ Q, binary comparison predicates <, ≤, =, =, ≥, >, a ternary additionpredicate +, and its negation + (all with the obvious semantics).
It is readily checked that Q is key-admissible (note that it provides a binary equality pred-icate) and thus falls into our framework. We conjecture that there exists only one minimalconcrete equivalence for every Q-predicate conjunction c: intuitively, it seems possible to(inductively) determine a relation ∼ on the set of variables V used in c such that (i) x ∼ yimplies that δ(x) = δ(y) for every solution δ for c and (ii) there exists a solution δ for c suchthat v ∼ v implies δ(v) = δ(v ). Clearly, ∼ is a minimal concrete equivalence. Moreover,due to (i) it is the only one.
4.2 A Tableau Algorithm for SHOQK(D)
Although ALCOK(D) is a quite powerful DL, it lacks several expressive means that can befound in most state-of-the-art description logic systems such as FaCT and RACER (Horrocks,1998; Horrocks et al., 2000; Haarslev & M¨
oller, 2001). In this section, we consider the
very expressive description logic SHOQK(D) which provides for concrete domains, keyboxes, and nominals, but also for many other means of expressivity such as transitiveroles, role hierarchies, qualifying number restrictions, and general TBoxes. Modulo somedetails, SHOQK(D) can be viewed as the extension of the DL SHOQ(D) with key boxes.SHOQ(D) was proposed by Horrocks and Sattler (2001) (see also Pan & Horrocks, 2002)as a tool for ontology reasoning in the context of the semantic web (Berners-Lee, Hendler,& Lassila, 2001; Baader et al., 2002a).
One very important feature of SHOQK(D) are so-called TBoxes, i.e. concept equations5
.
of the form C = D that are used as a “background theory” in reasoning. Since it is well-known that combining general TBoxes and the concrete domain constructor easily leadsto undecidability (Baader & Hanschke, 1992; Lutz, 2004), SHOQK(D) only offers a path-free variant of the concrete domain constructor—i.e. only concrete features are admittedinside this constructor rather than paths of arbitrary length. This restriction indeed regainsdecidability (Haarslev et al., 2001; Horrocks & Sattler, 2001). Path-freeness of the concretedomain constructor obviously renders abstract features unnecessary, and thus this syntactictype is not available in SHOQK(D).
5. Some TBox formalisms also allow for concept inclusions C
D, but these can be re-written into
equivalent equations, see Section 2.2.2.5 of (Baader et al., 2003).
698

 
Keys, Nominals and Concrete Domains
4.2.1 The Description Logic SHOQK(D)
Let us now define SHOQK(D) in a formal way, starting with the syntax.
Definition 4.6 (SHOQK(D) Syntax). A role axiom is either a role inclusion, which is ofthe form R
S with R, S ∈ NR, or a transitivity axiom Trans(R) where R ∈ NR. A role
box R is a finite set of role axioms. Let
* be the reflexive-transitive closure of the role
inclusions in R. A role name R is called simple if S * R implies Trans(S) /
∈ R for all role
names S. Let D be a concrete domain. The set of SHOQK(D)-concepts is the smallest setsuch that
• every concept name and every nominal is a concept, and
• if C and D are concepts, R is a role name, S a simple role name, n and k are natural
numbers, g1, . . . , gn are concrete features, and P ∈ ΦD is a predicate of arity n, thenthe following expressions are also concepts:
¬C, C
D, C
D, ∃R.C, ∀R.C, (
k S C), (
k S C), ∃g1, . . . , gn.P, and g1↑.
.
A concept equation is an expression C = D with C and D concepts. A TBox is a finite setof concept equations.
For SHOQK(D), we consider key boxes that differ in two aspects from the ones we consid-ered for ALCOK(D): in the following, we assume key boxes to be path-free, but we admitcomplex concepts to occur in key assertions. Note that abstract features and paths donot occur in the syntax of SHOQK(D)—as will become clear after the semantics has beendefined, the former can be “simulated” by the more general number restrictions (
n R C).
As usual in description logics of the SHIQ/SHOQ family, we require role names in
number restrictions to be simple since admitting arbitrary roles yields undecidability ofreasoning (Horrocks et al., 2000; Horrocks & Sattler, 2001). If the role box R is clear fromthe context, we will usually write Trans(R) instead of Trans(R) ∈ R. We now introduce thesemantics of SHOQK(D) and the relevant reasoning problems.
Definition 4.7 (SHOQK(D) Semantics). Interpretations I = (∆I, ·I) are defined as inDefinition 2.3, where the function ·I is extended to the novel SHOQK(D)-concepts asfollows:
(
k R C)I := d ∈ ∆I | e | (d, e) ∈ RI ≤ k and
(
k R C)I := d ∈ ∆I | e | (d, e) ∈ RI ≥ k.
.
Let I be an interpretation. Then I satisfies a concept equation C = D if CI = DI . I isa model of a TBox T if I satisfies all concept equations in T . Similarly, I satisfies a roleinclusion R
S if RI ⊆ SI and a transitivity axiom Trans(R) if RI is a transitive relation.
I is a model of a role box R if I satisfies all role inclusions and transitivity axioms in R.
Let T be a TBox, R a role box, and K a key box. A concept C is satisfiable w.r.t. T ,
R, and K iff C, T , R, and K have a common model. C is subsumed by a concept D w.r.t.T , R, and K (written C
T ,R,K D) iff C I ⊆ DI for all common models I of T , R, and K.
699

 
Lutz, Areces, Horrocks, & Sattler
Note that, due to the requirement that role names used inside number restrictions should besimple, existential and universal value restrictions are not just syntactic sugar: in contrastto number restrictions, they can be used on all roles.
It is well-known that, in many expressive description logics, reasoning with TBoxes
can be reduced to reasoning without them (Schild, 1991; Horrocks & Sattler, 2001): forSHOQK(D), a concept C is satisfiable w.r.t. T , R, and K iff the concept
∃R.C
∀R.
.
D ↔ E
∃R.N
D=E∈T
nominal N used
in C, T , or K
is satisfiable w.r.t. to R , K, and the empty TBox, where R is a fresh role not appearing inC, R, and T , and
R := R ∪ Trans(R) ∪
S
R.
role name S used
in C, T , R, or K
Since subsumption can be reduced to satisfiability as described in Section 2, in the followingwe will only consider satisfiability of concepts w.r.t. role boxes and key boxes, but withoutTBoxes. We will also generally assume role boxes R to be acyclic, i.e. to satisfy the followingcondition: for each role name R, there are no role names R1, . . . , Rk such that R = R1 = Rkand Ri
Ri+1 ∈ R for 1 ≤ i < k. It is not hard to see that this is not a restriction since
cycles can be eliminated: if R1, . . . , Rk is a cycle in R, then we have RI = · · · = RI
1
k
for all interpretations I. Thus we can simply remove the cycle from R and replace everyoccurrence of R2, . . . , Rk in C, R, and K with R1, and add Trans(R1) if, before the cycleelimination, we had Trans(Ri) for some i with 1 ≤ i ≤ n.
Before we turn our attention to the construction of a tableau algorithm for SHOQK(D),
let us comment on a few minor differences between SHOQK(D) as introduced here andthe original version of SHOQ(D) as described in (Horrocks & Sattler, 2001). The maindifference is that our logic, like the extensions investigated in (Haarslev et al., 2001; Pan &Horrocks, 2002), allows n-ary predicates while Horrocks and Sattler restrict themselves tounary predicates. Moreover, SHOQ(D) as introduced in (Horrocks & Sattler, 2001) usesconcrete roles rather than concrete features, the difference being that concrete roles are notnecessarily functional. Due to this non-functionality, the original SHOQ(D) admits twovariants ∃T.P and ∀T.P of the concrete domain constructor (where T is a concrete role andP a unary predicate). In SHOQK(D), we can simulate the universal variant by writing∃g.P
g↑ since concrete features g are interpreted as partial functions and, in contrast to
Horrocks and Sattler, we have the undefinedness constructor g↑ available. Except for then-ary predicates which provide important additional expressivity, we view these deviationsas minor ones since it is easy to see that they do not affect decidability and complexity ofreasoning.
4.2.2 A Tableau Algorithm for SHOQK(D)
The basic intuitions of the SHOQK(D) tableau algorithm are similar to the ALCOK(D)algorithm, with one exception: to deal with the various expressive means of SHOQK(D),
700

 
Keys, Nominals and Concrete Domains
¬(
n R C)
(
(n − 1) R C) if n ≥ 1
¬(
0 R C)
⊥
¬(
n R C)
(
(n + 1) R C)
Figure 10: The SHOQK(D) NNF rewrite rules.
it is convenient to introduce a certain abstraction of models, so-called tableaux. The maindifference between tableaux and models is that, in tableaux, roles declared to be transitiveare not necessarily described by transitive relations. We show that there exists a tableaufor a given concept and key box if and only if they have a common model. The aim of theSHOQK(D) algorithm is then to construct a tableau for its input rather than trying toconstruct a model. To do this, the algorithm employs completion forests as its underlyingdata structure.
We first introduce tableaux. Let us start by discussing some preliminaries. As for
ALCOK(D), we assume all concepts and key boxes to be in NNF, i.e. negation occurs onlyin front of concept names and nominals. We again use ˙
¬ C to denote the NNF of ¬C. The
additional NNF rewrite rules for SHOQK(D) can be found in Figure 10 and complete thosegiven for ALCOK(D) in Figure 7.
For a concept D, role box R, and key box K, we define
cl(D, K) := sub(D) ∪ sub(con(K)) ∪  ˙
¬C | C ∈ sub(D) ∪ sub(con(K))
cl(D, R, K) := cl(D, K) ∪ ∀R.C | R * S and ∀S.C ∈ cl(D, K).
Obviously, the cardinality of cl(D, R, K) is linear in the size of D, R, and K. In whatfollows, we write ND,R,K to denote the set of role names occurring in D, R, or K, and ND,K
R
cF
to denote the sets of concrete features occurring in D or K. We are now ready to definetableaux.
Definition 4.8 (Tableau). Let D be a SHOQK(D)-concept in NNF, R a role box, and Ka path-free key box in NNF. A tableau T for D w.r.t. R and K is a tuple (Sa, Sc, L, E, e, P)such that
• Sa, Sc are sets of abstract and concrete individuals,
• L : Sa → 2cl(D,R,K) maps each abstract individual to a subset of cl(D, R, K),
• E : Sa × Sa → 2ND,R,K
R
maps pairs of abstract individuals to sets of roles,
• e : Sa×ND,K → S
cF
c maps pairs of abstract individuals and concrete features to concrete
individuals,
• P maps each n-ary concrete predicate in cl(D, R, K) to a set of n-tuples over Sc,
• there is an abstract individual s0 ∈ Sa such that D ∈ L(s0), and
for all s, t ∈ Sa, C, C1, C2 ∈ cl(D, R, K), R, S ∈ ND,R,K, and for
R
ST (s, C) := t ∈ Sa | S ∈ E(s, t) and C ∈ L(t),
it is the case that:
701

 
Lutz, Areces, Horrocks, & Sattler
(T1) if C ∈ L(s), then ˙
¬ C /
∈ L(s),
(T2) if C1
C2 ∈ L(s), then C1 ∈ L(s) and C2 ∈ L(s),
(T3) if C1
C2 ∈ L(s), then C1 ∈ L(s) or C2 ∈ L(s),
(T4) if R ∈ E(s, t) and R * S, then S ∈ E(s, t),
(T5) if ∀R.C ∈ L(s) and R ∈ E(s, t), then C ∈ L(t),
(T6) if ∃R.C ∈ L(s), then there is some t ∈ Sa such that R ∈ E(s, t) and C ∈ L(t),
(T7) if ∀S.C ∈ L(s) and R ∈ E(s, t) for some R * S with Trans(R), then ∀R.C ∈ L(t),
(T8) if (
n S C) ∈ L(s), then ST (s, C)
n,
(T9) if (
n S C) ∈ L(s), then ST (s, C)
n,
(T10) if either (
n S C) ∈ L(s) and S ∈ E(s, t) or (g1, . . . , gn keyfor C) ∈ K and e(t, gi)
is defined for all 1 ≤ i ≤ n, then C, ˙
¬ C ∩ L(t) = ∅,
(T11) if N ∈ L(s) ∩ L(t), then s = t,
(T12) if ∃g1, . . . , gn.P ∈ L(s), then there are x1, . . . , xn ∈ Sc with e(s, gi) = xi and
(x1, . . . , xn) ∈ P(P ),
(T13)
P (x
x = y is satisfiable,
P used in D,K
(x
1, . . . , xn) ∧
1,...,xn)∈P (P )
x=y
(T14) if (g1, . . . , gn keyfor C) ∈ K, C ∈ L(s) ∩ L(t), and e(s, gi) = e(t, gi) for all 1 ≤ i ≤ n,
then s = t,
(T15) if g↑ ∈ L(s), then e(s, g) is undefined.
Note that the predicate conjunction in (T13) uses a binary inequality predicate. In general,we do not require the concrete domain D to be equipped with such a predicate and thus thispredicate conjunction is not necessarily a D-conjunction. However, it is nevertheless “safe”to use (T13) in the given form since tableaux are only used in proofs and we do not needa concrete domain reasoner that is capable of deciding the satisfiability of this conjunction.The following lemma, whose proof is provided in Appendix C, shows that our definition oftableaux provides an adequate abstraction of models.
Lemma 4.2. Let D be a SHOQK(D)-concept in NNF, R a role box, and K a key box inNNF. Then D is satisfiable w.r.t. R and K iff D has a tableau w.r.t. R and K.
Given Lemma 4.2, in order to decide satisfiability of SHOQK(D)-concepts w.r.t. role andkey boxes, we may use a (tableau) algorithm that tries to construct a tableau for the input.In the following, we will describe such an algorithm in detail.
As in the previous section, the algorithm works on completion systems. However, in
the case of SHOQK(D) the core component of completion systems is a completion forestrather than a completion tree. The reason for this is that some completion rules removenodes and edges from the completion system and in this way can disconnect one tree intotwo subtrees.
702

 
Keys, Nominals and Concrete Domains
Definition 4.9 (Completion System). Let D be a SHOQK(D)-concept in NNF, R a rolebox, and K a path-free key box in NNF. For each concept (
n R C) ∈ cl(D, R, K) and
1 ≤ i ≤ n, we reserve a concept name AnRC not appearing in cl(D, R, K) and define an
i
extended closure
cl+(D, R, K) := cl(D, R, K) ∪ AnRc
|
1
, . . . , AnRc
n
(
n R C) ∈ cl(D, R, K).
Let Oa and Oc be disjoint and countably infinite sets of abstract and concrete nodes. Acompletion forest for D, R, and K is a finite forest F = (Va, Vc, E, L) with nodes Va ∪ Vcsuch that Va ⊆ Oa, Vc ⊆ Oc, and all nodes from Vc are leaves. The forest is labelled asfollows:
• each node a ∈ Va is labelled with a subset L(a) of cl+(D, R, K),
• each edge (a, b) ∈ E with a, b ∈ Va is labeled with a non-empty set of role names
L(a, b) occurring in D, R, or K, and
• each edge (a, x) ∈ E with a ∈ Va and x ∈ Vc is labeled with a concrete feature L(a, x)
occurring in D, R, or K.
A completion system for D, R, and K is a tuple S = (F, P, ∼c, ) such that
• F = (Va, Vc, E, L) is a completion forest for D, R, and K,
• P maps each n-ary concrete predicate in cl(D, R, K) to a set of n-tuples in Vc,
• ∼c is an equivalence relation on Vc, and
•
is a linear ordering on Va.
A node t ∈ Va is called an R-successor of a node s ∈ Va if, for some R with R * R, we haveR ∈ L(s, t). A node x ∈ Vc is called a g-successor of a node s ∈ Va if L(s, x) = g. Finally,
.
we write s = t if s and t are R-successors of the same node and there is some AnRC ∈ L(s)
i
and AnRC ∈ L(t) with i = j.
j
Some remarks are in order here. Firstly, in contrast to the ALCOK(D) case, the relation
is no longer required to respect the level of a node. This is due to the fact that (a)
we have to enforce termination artificially and the mentioned property of
was used to
ensure “automatic” termination, and (b) the level of a node might change since a nodemight become a root node because some completion rules will remove nodes and edges.
Secondly, the relation ∼c will be returned by a D-tester, and is used to compute a
relation ≈a which is then used by the tableau algorithm. However, we do not need tocompute the relation ≈c from ≈a as in the ALCOK(D) case since all concepts and keyboxes are assumed to be path-free.
Thirdly, the new concept names AnRC will be used to ensure that successors of a node
i
x generated for some (
n R C) ∈ L(x) will not be merged later due to a concept (
n R C ) ∈ L(x): each generated successor is labelled with a different concept AnRC ;
i
since merging two nodes means unifying their node labels, it then suffices to disallow the
703

 
Lutz, Areces, Horrocks, & Sattler
occurrence of distinct concepts AnRC in the same node label through a suitable definition
i
of “clash”.
Since SHOQK(D) provides for transitive roles, we need some cycle-detection mechanism
in order to guarantee termination of our algorithm: roughly speaking, if we encounter anode which is “similar” to an already existing one, then this node does not need to befurther explored. Speaking in terms of (Horrocks et al., 2000; Baader & Sattler, 2000), weemploy a mechanism called subset blocking.
Definition 4.10 (Blocked). Let
be the reflexive closure of
. A node t ∈ Va is blocked
by a node s ∈ Va if L(t) ⊆ L(s), and s
s , for all s with L(t) ⊆ L(s ).
Note that, unlike to what is done, e.g., in (Horrocks et al., 2000), the blocking node is notnecessarily an ancestor of the blocked node, but can be anywhere in the forest. It may evenbe that blocked nodes have unblocked successors. This modification is used later to obtaina NExpTime upper bound.
To decide the satisfiability of an ALCOK(D)-concept D w.r.t. a role box R and a path-
free key box K (where D and K are in NNF), the tableau algorithm is started with theinitial completion system
SD = (FD, P∅, ∅, ∅), where
FD = (s0, ∅, ∅, s0 → D) and
P∅
maps each P ∈ ΦD occurring in D and K to ∅.
Then the algorithm repeatedly applies completion rules. Before the actual rules are given,we introduce some new notions: firstly, we define the equivalence relation ≈a over Va asfollows: s ≈a t if one of the following conditions is satisfied:
• N ∈ L(s) ∩ L(t) for some nominal N or
• (g1 . . . , gn keyfor C) ∈ K, C ∈ L(s)∩L(t), and there are xi, yi such that gi ∈ E(s, xi)∩
E(t, yi) and xi ∼c yi for 1 ≤ i ≤ n.
Intuitively, two abstract nodes related via the ≈a relation describe the same individual ina tableau.
Secondly, we use the following abbreviations in the formulation of the rules (written in
italic):
• To remove an abstract node s and all its incoming and outgoing edges, remove s from
Va and each (s, t) and (t, s) from E for all t ∈ Va ∪ Vc.
• Adding a g-successor of an abstract node s means doing nothing if there exists a
g-successor x ∈ Vc of s and, otherwise, adding E(s, x) = g for some x ∈ Oc that doesnot yet occur in the completion forest.
• To update the relation ∼c, a D-tester is asked to decide the satisfiability of the D-
conjunction
ζS :=
P (x1, . . . , xn) ∧
x = y
P used in D,K
x∼cy
(x1,...,xn)∈P(P )
and returns, in case that this conjunction is satisfiable, an “updated” concrete equiv-alence ∼c as defined in Definition 4.1.
704

 
Keys, Nominals and Concrete Domains
Concerning the predicate conjunction used in updates, recall that we can w.l.o.g. assumethe concrete domain to contain an equality predicate as discussed after Definition 4.1.
The completion rules are given in Figure 11. We generally assume that new nodes x
are introduced into the completion forest such that y
x for all already existing nodes y.
Before further describing the tableau algorithm, we comment on the completion rules. Therules R , R , R∃c, and Rch are non-deterministic, i.e., their application has more than onepossible outcome. For the R∃c rule, this is due to the update operation performed on ∼cusing the D-tester: as discussed at the end of Section 4.1, computing a concrete equivalencefor a given D-conjunction may result in a high degree of non-determinism. Please note that,in contrast to ALCOK(D), we now only need to call the D-tester in this rule—and not aftereach rule application.
Next, the R≈a rule takes care of abstract nodes related via ≈a. Since all the nodes from
a ≈a-equivalence class denote the same individual, we choose only one representative whosenode label contains the labels of all other nodes in the class. This representative simplyis the
-minimal node of the equivalence class and the R≈a rule performs the appropriate
copying of node labels.
The R
rule is the only rule to remove nodes and edges: it removes a surplus R-successor
t of a node s with (
n R C) ∈ L(s). Since the subtree below t is not removed, t’s successors
are new, additional root nodes. This behavior is the reason why we work on a completionforest.
As in the ALCOK(D) case, the tableau algorithm stops applying rules if it finds an
obvious contradiction, a “clash”, or if no more completion rules are applicable.
Definition 4.11 (Clash). Let S = (F, P, ∼c, ) be a completion system for D, R and K,and F = (Va, Vc, E, L). Then S is said to contain a clash if one of the following conditionsapplies:
(C1) for some concept name A ∈ NC and some node s ∈ Va, A, ¬A ⊆ L(s);
(C2) the D-conjunction ζS defined above is not satisfiable;
.
(C3) s = s for some s ∈ Va;
(C4) for some s ∈ Va and g ∈ NcF, we have g↑ ∈ L(s) and s has a g-successor.
A completion system not containing a clash is called clash-free. The completion system iscomplete if none of the completion rules is applicable.
Due to the simplicity of the algorithm, we refrain from describing it in pseudo-code nota-tion: the algorithm starts with the initial completion system and then repeatedly appliesthe completion rules, checking for clashes after each rule application. If a clash is de-tected, it returns unsatisfiable. If a complete and clash-free completion system is found,then the algorithm returns satisfiable. Note that, since some of the completion rules arenon-deterministic, the algorithm is also non-deterministic.
Details of the proof of termination, soundness, and completeness are given in Ap-
pendix C. Unfortunately, we have to leave the complexity of the algorithm as an openproblem: it is not hard to prove that it runs in double exponential time, but it is not clearwhether exponential time also suffices. However, we can still use the algorithm to obtain a
705

 
Lutz, Areces, Horrocks, & Sattler
R
if C1
C2 ∈ L(s), s is not blocked, and C1, C2 ⊆ L(s),
then L(s) := L(s) ∪ C1, C2
R
if C1
C2 ∈ L(s), s is not blocked, and C1, C2 ∩ L(s) = ∅,
then L(s) := L(s) ∪ C for some C ∈ C1, C2
R∃
if ∃R.C ∈ L(s), s is not blocked, and s has no R-successor t with C ∈ L(t)then create a new node t such that t
t for all t ∈ Va
and set E(s, t) := R and L(t) := C
R
if (
n S C) ∈ L(s), s is not blocked, and there are no n S-successors
.
t1, . . . , tn of s with C ∈ L(ti) and ti = tj for 1 ≤ i < j ≤ n,
then create n new nodes t1, . . . , tn s.t. t
ti for 1 ≤ i ≤ n and all t ∈ Va,
and set E(s, ti) := S and L(ti) := C, AnSC for 1 ≤ i ≤ n
i
R
if (
n S C) ∈ L(s), s is not blocked, s has n + 1 S-successors t0, . . . , tn
with C ∈ L(ti) for 0 ≤ i ≤ n,
then choose i, j such that ti
tj, set L(ti) := L(ti) ∪ L(tj),
L(s, ti) := L(s, ti) ∪ L(s, tj), and remove tj and all its incomingand outgoing edges
R∃c
if ∃g1, . . . , gn.P ∈ L(s), s is not blocked, and
there are no gi-successors xi with (x1, . . . , xn) ∈ P(P )
then add a gi-successor of s for each 1 ≤ i ≤ n,
for yi the gi-successor of s, add (y1, . . . , yn) to P(P ), andupdate ∼c
R∀
if ∀R.C ∈ L(s), s is not blocked, and
there is an R-successor t of s with C /
∈ L(t),
then L(t) := L(t) ∪ C
R∀+
if ∀S.C ∈ L(s), s is not blocked, there is some R with
Trans(R) and R * S, and an R-successor t of s with ∀R.C /
∈ L(t),
then L(t) := L(t) ∪ ∀R.C
Rch
if s is an S-successor of s and (
n S C) ∈ L(s ) or
s has gi-successors xi for all 1 ≤ i ≤ n and (g1, . . . gn keyfor C) ∈ K ands is not blocked and C, ˙
¬ C ∩ L(s) = ∅,
then L(s) := L(s) ∪ E for some E ∈ C, ˙
¬ C
R≈a
if s ≈a t, L(t) ⊆ L(s), s
t, and s is not blocked,
then set L(s) := L(s) ∪ L(t)
Figure 11: The completion rules for SHOQK(D).
706

 
Keys, Nominals and Concrete Domains
tight complexity bound for SHOQK(D): the following corollary is an easy by-product ofthe correctness proofs (for a proof see again Appendix C).
Corollary 4.3. If a SHOQK(D)-concept D is satisfiable w.r.t. a role box R and a path-freekey box K, then D is satisfiable w.r.t. R and K in a model of size at most |∆I| ≤ 2m form =  cl+(D, R, K).
Thus the following is an alternative algorithm for deciding satisfiability of a SHOQK(D)-concept D w.r.t. a role box R and a path-free key box K: first, guess an interpretationI with cardinality of ∆I bounded by 2m, using placeholder variables from Oc instead ofconcrete values in the interpretation of concrete features. Let Vc be the set of variablesfrom Oc occuring in I. Additionally guess an “interpretation” P for the concrete domainpredicates: just as in completion forests, P maps each n-ary concrete predicate used in D orK to an n-ary relation on Vc. Then perform standard (polynomial-time) model checking toensure that I is a model of D. In doing this, treat concepts of the form ∃g1, . . . , gn.P usingthe interpretation of predicates P. It is easily checked in polynomial time that I is also amodel of R and K—for the latter, assume that all placeholder variables stand for differentvalues. Finally, use the concrete domain D-tester to check whether the conjunction
P (x1, . . . , xn)
P used inD,K
(x1,...,xn)∈P(P )
is satisfiable. Answer “yes” if it is and “no” otherwise. Since this algorithm can clearly beimplemented in NExpTime provided that there is a D-tester running in non-deterministicpolynomial time, we obtain the following:
Theorem 4.4. Let D be a key-admissible concrete domain such that extended D-satisfiabilityis in NP, then SHOQK(D)-concept satisfiability w.r.t. TBoxes, role boxes, and path-freekey boxes is in NExpTime.
5. Conclusion
In this paper, we have identified key constraints as an interesting extension of descriptionlogics with concrete domains. Starting from this observation, we introduced a number ofnatural description logics and provided a comprehensive analysis of the decidability andcomplexity of reasoning. The main observation of our investigations is that key boxes canhave dramatic consequences on the complexity of reasoning: for example, the PSpace-complete DL ALC(D) becomes NExpTime-complete if extended with path-free, unary,Boolean key boxes and undecidable if extended with path-free, unary, non-Boolean keyboxes. Thus the effect of our key boxes on the complexity are quite different from the effectof key assertions where only abstract features are allowed (Calvanese et al., 2000): theseabstract key assertions can be said to be “for free” since they do not increase the complexityfor expressive description logics.
We show that the restriction to Boolean key boxes (in the ALCOK(D) case) and to
path-free key boxes (in the SHOQK(D) case) yield decidabile and NExpTime-completereasoning problems. We selected ALC(D) and SHOQ(D) as the basis for our analysis since,
707

 
Lutz, Areces, Horrocks, & Sattler
in our opinion, these are the most fundamental description logics with concrete domains.Going one step further, it would be interesting to combine key boxes with other extensionsof concrete domains, such as the ones presented by Lutz (2003, 2004). To name only onepossibility, the extension of both ALCOK(D) and SHOQ(D) with inverse roles seems tobe a natural idea. Note that inverse roles interact with several of the available means ofexpressivity: while ALC with inverse roles is PSpace complete (Horrocks, Sattler, & Tobies,1999), ALCO with inverse roles is ExpTime-complete (Areces et al., 1999) and ALC(D)with inverse roles even NExpTime-complete (Lutz, 2004).
Other options for future research are more closely related to the material presented in
this paper. For example, is SHOQK(D)-concept satisfiability still decidable if we dropthe requirement of key boxes to be path-free? Moreover, we had to leave the exact timerequirements of our tableau algorithm as an open problem. If this algorithm runs in (non-deterministic) exponential time, it directly yields Theorem 4.4 rather than via a boundedmodel property.
Acknowledgments
We would like to thank the anonymous reviewers for valuable comments. This paper is anextended version of (Lutz, Areces, Horrocks, & Sattler, 2003).
Appendix A. Proofs of Section 3.2
We prove that D2-satisfiability can be decided in PTime.
Proposition A.1. D2-satisfiability is in PTime.
Proof. Let c be a D2-conjunction. We show that c is satisfiable iff none of the followingconditions applies:
1. c contains a conjunct ⊥D (x);
2
2. c contains conjuncts bit0i (x) and bit1i (x);
k
k
3. c contains conjuncts bitni (x) and bitmj(x) with k = ;
k
4. c contains conjuncts bitni (x) and bitni (x);
k
k
5. c contains conjuncts bitni (x), bit0j (x), and bit1j (x).
k
k
k
It is easily seen that c is unsatisfiable if one of the conditions applies. Assume now thatConditions 1 to 5 do not apply to c and let X be the set of variables used in c. For eachx ∈ X, set t(x) = k if bitni (x) ∈ c for some n, i ∈ N.6 If bitni (x) /
∈ c for all n, i, k ∈ N, then
k
k
set t(x) = r for some r not appearing as an index ·r to a predicate in c. The mapping t iswell-defined since c is finite, Condition 3 does not apply, and the only predicates availableare bitni (·), ⊥
(·), and
(·). We define a solution δ for c as follows: for each x ∈ X, set
k
D2
D2
δ(x) to the bit vector v ∈ BVt(x) in which the i’th bit is 1 if bit1i
(x) ∈ c or bit0i
(x) ∈ c,
t(x)
t(x)
and 0 otherwise. It remains to prove that δ is indeed a solution for c:
6. We use “P (x) ∈ c” as an abbreviation for “P (x) is a conjunct in c”.
708

 
Keys, Nominals and Concrete Domains
• Let bit0i (x) ∈ c. Then t(x) = k and thus δ(x) ∈ BV
k
k .
Since Condition 2 does
not apply, we have bit1i (x) /
∈ c. Moreover, non-applicability of Condition 4 implies
k
bit0i (x) /
∈ c. By definition of δ, the i’th bit of δ(x) is thus 0.
k
• Let bit1i (x) ∈ c. Then t(x) = k and δ(x) ∈ BV
k
k . By definition of δ, the i’th bit of
δ(x) is 1.
• Let bit0i (x) ∈ c. If t(x) = k, then δ(x) /
∈ BV
)D2 and we are
k
k .
Thus δ(x) ∈ (bit0ik
done. If t(x) = k, then the i’th bit of δ(x) is 1 by definition of δ and thus again
δ(x) ∈ (bit0i )D2 .
k
• Let bit1i (x) ∈ c. If t(x) = k, then δ(x) /
∈ BV
k
k and we are done. If t(x) = k, then
bitnj (x) ∈ c for some n, j ∈ N. Since Condition 5 does not apply, we thus have
k
bit0i (x) /
∈ c. Moreover, non-applicability of Condition 4 yields bit1i (x) /
∈ c. Thus, by
k
k
definition of δ, the i’th bit of δ(x) is 0.
It is obvious that the listed properties can be checked in polynomial time.
Appendix B. Proofs of Section 4.1
We prove termination, soundness, and completeness of the ALCOK(D) tableau algorithmpresented in Section 4.1, starting with termination. We start with establishing a few notionsand technical lemmas.
Let C be a concept and K a key box. We use |C| to denote the length of C, i.e. the
number of symbols used to write it down, and |K| to denote
|C|. For
(u1,...,uk keyfor C)∈K
a path u = f1 · · · fkg, we use |u| to denote k + 1. The role depth of concepts is definedinductively as follows:
rd(A) = rd(N ) = rd(g↑) = 0rd(∃u1, . . . , un.P ) = max|ui| | 1 ≤ i ≤ n − 1
rd(C
D) = rd(C
D) = maxrd(C), rd(D)
rd(∃R.C) = rd(∀R.C) = rd(C) + 1.
The following series of lemmas will eventually allow us to prove termination.
Lemma B.1. There is a constant k such that, if the tableau algorithm is started on inputC0, K and T = (Va, Vc, E, L) is a completion tree constructed during the run of the algorithm,then Va ≤ 2|C0|k and Vc ≤ 2|C0|k .
Proof. Using induction on the number of rule applications and a case distinction accordingto the applied rule, it is straightforward to show that
C ∈ L(a) implies rd(C) ≤ |C0| − levT(a)
(∗)
for all constructed completion trees T. We omit the details but note that, (1) for treatingthe Rch rule, one needs to employ the fact that K is Boolean and thus only adds conceptsof role depth 0 to node labels, and (2) for treating the Rp rule, we use that a
b implies
levT(a) ≤ levT(b).
709

 
Lutz, Areces, Horrocks, & Sattler
This implies an upper bound on the depth of constructed completion trees: first, only
the R∃ and R∃c rules generate new nodes, and an application of either rule to a nodea ∈ Va implies L(a) = ∅ and thus levT(a) ≤ |C0| by (∗). Second, each new (abstract orconcrete) node b generated by an application of these rules to a node a ∈ Va clearly satisfieslevT(b) ≤ levT(a) + max(1, mpl(C0)), where mpl(C0) denotes the maximum length of pathsin C0 (note that concepts in K may not contain any paths since it is Boolean). Sincempl(C0) ≤ |C0|, the above observations imply that the depth of constructed completiontrees is bounded by 2 · |C0|.
Now for the out-degree. If a node a is generated, then this is due to the application of
a rule R∃ or R∃c and, initially, a has at most one successor. Let us analyze the numberof successors generated by later applications of the rules R∃ and R∃c to a: these rulescan be applied at most once for each concept of the form ∃R.C or ∃u1, . . . , un.P in L(a).By definition of cl(C0, K) and since K is Boolean, the number of such concepts per nodelabel is bounded by sub(C0) ≤ |C0|. Moreover, each rule application creates at most |C0|successors. Hence, the out-degree of constructed completion trees is bounded by |C0|2 + 1.
Lemma B.2. There is a constant k such that, if the tableau algorithm is started with C0, K,then, in every recursion step, the while loop terminates after at most 2|C0|k steps.
Proof. Fix an argument S = (T, P,
, ∼) with T = (Va, Vc, E, L) passed to the sat function,
let ∼1, ∼2, . . . be the sequence of concrete equivalences computed in the while loop, and let≈1c, ≈2c, . . . be the corresponding ≈c relations. Since test(ζS) calls a D-tester, each of thesecalls indeed terminates.
We show that
∼1
∼2
· · · ,
(∗)
which implies Lemma B.2: by Lemma B.1, there exists a constant k such that Vc ≤ 2|C0|k .Hence, we have ∼i ≤ 22·|C0|k which, together with (∗), implies that the number of stepsperformed by the while loop is also bounded by 22·|C0|k .
Now for the proof of (∗). If the while loop reaches the i-th step, then we had ∼i−1 = ≈i−1
c
after step i − 1. Since ∼i−1 ⊆ ≈i−1
c
by definition, this implies ∼i−1
≈i−1
c
. By definition
of ζS, it is easy to see that ≈i−1 ⊆ ∼
c
i for i ≥ 1. Hence ∼i−1
∼i.
Lemma B.3. There is a constant k such that, if the tableau algorithm is started with C0, K,then the number of recursive calls is bounded by 2(|C0|+|K|)k .
Proof. It obviously suffices to establish an appropriate upper bound on the number of ruleapplications. The R , R , R∃, and R∃c rules can be applied at most once for each conceptin a node label. By Lemma B.1, the number of nodes is at most exponential in |C0| + |K|.Since neither nodes nor concepts in node labels are ever deleted, the fact that node labelsare subsets of cl(C0, K) thus implies that the number of applications of these rules is at mostexponential in |C0| + |K|. The same holds for the rules R∀ and Rp, which can be appliedat most once for every concept C ∈ cl(C0, K) and every pair of (abstract) nodes. Finally,the number of Rch applications is at most exponential in |C0| + |K| since this rule can beapplied at most once for every abstract node and every key assertion in K.
710

 
Keys, Nominals and Concrete Domains
Termination is now an obvious consequence of Lemmas B.2 and B.3.
Corollary B.4 (Termination). The tableau algorithm terminates on any input.
Let us now prove soundness of the algorithm.
Lemma B.5 (Soundness). If the tableau algorithm returns satisfiable, then the input conceptC0 is satisfiable w.r.t. the input key box K.
Proof. If the tableau algorithm returns satisfiable, then there exists a complete and clash-free completion system S = (T, P,
, ∼) for C0. Let T = (Va, Vc, E, L). By definition of
the tableau algorithm, there is a completion system S = (T, P,
, ∼ ) such that a call to
test(ζS ) returned ∼. Moreover, we have ∼ = ≈c in S. Thus, there exists a solution δ forζS such that
δ(x) = δ(y) iff x ≈c y.
(†)
Clearly, δ is also a solution for ζS: since the second component P is the same in S and S ,δ is a solution for the first part
P (x1, . . . , xn) of ζS. Moreover, for
P used in C (x1,...,xn)∈P(P )
each conjunct =(x, y) from the second part of ζS, we have x ≈c y by definition of ζS andthus δ(x) = δ(y) by (†).
We now use S and δ to construct an interpretation I by setting
∆I
=
a ∈ Va | there is no b ∈ Va such that a ≈a b and b
a ∪ w
AI
=
a ∈ ∆I | A ∈ L(a)
a ∈ ∆
N I
=
I | N ∈ L(a)
if there is an a ∈ ∆I such that N ∈ L(a)
w
otherwise
RI
=
(a, b) ∈ ∆I × ∆I | there are a , b ∈ Va such that a ≈a a , b ≈a b , and
b is an R-successor of a 
gI
=
(a, δ(x)) ∈ ∆I × ∆D | x is a g/≈a-neighbor of a
for all A ∈ NC, N ∈ NO, R ∈ NR, and g ∈ NcF. We first show that I is well-defined:
• N I is a singleton for each N ∈ NO. Assume that there exist a, b ∈ ∆I such that a = b
and N ∈ L(a) ∩ L(b). By definition of ≈a (Definition 4.3), N ∈ L(a) ∩ L(b) impliesa ≈a b. This, together with a, b ∈ ∆I, yields a
b and b
a, contradicting
being
a linear ordering.
• f I is functional for each f ∈ NaF. Assume that there exist a, b, c ∈ ∆I such that
(a, b), (a, c) ⊆ f I and b = c. Then there exist a1, a2, b , c ∈ Va such that a ≈a a1 ≈aa2, b ≈a b , c ≈a c , b is an f -successor of a1, and c is an f -successor of a2. Bydefinition of ≈a, we thus have b ≈a c implying b ≈a c. Since b, c ∈ ∆I, this yieldsb
c and c
b, a contradiction.
• gI is functional for each g ∈ NcF. Assume that there exist an a ∈ ∆I and x, y ∈ Vc
such that (a, δ(x)), (a, δ(y)) ⊆ f I and δ(x) = δ(y). Then x and y are both g/≈a-neighbors of a. By definition of ≈c, we thus have x ≈c y implying δ(x) = δ(y) by (†),a contradiction.
711

 
Lutz, Areces, Horrocks, & Sattler
Now we show the following claim. In the proof, we use the notion of f1 · · · fk/≈a-neighbors(with f1, . . . fk abstract features), which is defined analogously to u/≈a-neighbors for paths u.
Claim 1: For all a ∈ ∆I and all paths u, we have uI(a) = α iff there is a ui/ ≈a-neighborx of a with δ(x) = α.
Proof: Let u = f1 · · · fkg. Using induction on i it is easily proved that, for all i and allb ∈ ∆I, we have f I(· · · (f I(a)) · · · ) = b iff there is a f
i
1
1 · · · fi/≈a-neighbor b
of a with
b ≈a b . Thus we have in particular that f I(· · · (f I(a)) · · · ) = b iff there is an f
k
1
1 · · · fk/≈a-
neighbor b of a with b ≈a b . To prove the claim, it hence remains to use the definitionof gI together with (†).
The following claim is central for showing that I is a model for C0 and K.
Claim 2: For all a ∈ ∆I and C ∈ cl(C0, K), if C ∈ L(a), then a ∈ CI.
Since C0 is in the label of the root node, Claim 2 clearly implies that I is a model for C0.Moreover, we can use it to prove that I satisfies all key assertions (u1, . . . , un keyfor C) inK: fix a, b ∈ CI such that uI (a) = uI (b) for 1 ≤ i ≤ n. Non-applicability of Rch yields
i
i
C, ˙
¬ C ∩ L(a) = ∅. If ˙
¬ C ∈ L(a), then Claim 2 implies a ∈ ( ˙
¬ C)I in contradiction to
a ∈ CI . Thus we obtain C ∈ L(a). In an analogous way, we can argue that C ∈ L(b). SinceuI (a) and uI (b) are defined for 1 ≤ i ≤ n, Claim 1 yields that a has a u
i
i
i/≈a-neighbor xi
with δ(xi) = uI(a) and b a u
(b) for 1 ≤ i ≤ n. Thus the
i
i/≈a-neighbor yi with δ(yi) = uI
i
fact that uI (a) = uI (b) yields δ(x
i
i
i) = δ(yi) for 1 ≤ i ≤ n. By (†) we obtain xi ≈c yi and
thus xi ∼ yi for 1 ≤ i ≤ n. By definition of ≈a, we thus get a ≈a b. Since a, b ∈ ∆I, weobtain a
b and b
a by definition of ∆I and thus a = b.
It remains to prove Claim 2, which we do using structural induction:
• C is a concept name or a nominal. Easy by construction of I.
• C = ¬D. Since C ∈ cl(C0, K), C is in NNF and D is a concept name. Since S is
clash-free, C ∈ L(a) implies D /
∈ L(a). Thus, a /
∈ DI by construction of I, which
yields a ∈ (¬D)I .
• C = ∃u1, . . . , un.P . Since the R∃c rule is not applicable, there exist x1, . . . , xn ∈ Vc
such that xi is a ui/≈a-neighbor of a for 1 ≤ i ≤ n and (x1, . . . , xn) ∈ P(P ). Claim 1yields uI (a) = δ(x
i
i) for 1 ≤ i ≤ n. Since (x1, . . . , xn) ∈ P (P ) and δ is a solution for
ζS, we have (δ(x1), . . . , δ(xn)) ∈ P D and thus a ∈ CI.
• C = g↑. Since S is clash-free, there exists no x ∈ Vc such that x is g/≈a-neighbor of
a. Thus by Claim 1 there is no α such that (a, α) ∈ gI .
• C = D
E or C = D
E. Straightforward using completeness and the induction
hypothesis.
• C = ∃R.D. Since the R∃ rule is not applicable, a has an R/≈a-neighbor b such that
D ∈ L(b). Let b be minimal w.r.t.
such that b ≈a b . By definition of I, we have
(a, b ) ∈ RI . Non-applicability of the Rp rule yields D ∈ L(b ). By induction, we getb ∈ DI and thus a ∈ CI .
712

 
Keys, Nominals and Concrete Domains
• C = ∀R.D. Let (a, b) ∈ RI . By definition of I, this implies that there exist a , b ∈ Va
such that a is minimal w.r.t.
and a ≈a a , b is minimal w.r.t.
and b ≈a b , and b
is an R-successor of a . Since b is clearly an R/≈a-neighbor of a, non-applicability ofR∀ yields D ∈ L(b ), which implies D ∈ L(b) due to the non-applicability of Rp. Byinduction, we get b ∈ DI . Since this holds independently of the choice of b, we obtaina ∈ (∀R.D)I .
Lemma B.6 (Completeness). If the input concept C0 is satisfiable w.r.t. the input key boxK, then the tableau algorithm returns satisfiable.
Proof. Let I be a model of C0 and K. We use I to “guide” (the non-deterministic partsof) the algorithm such that it constructs a complete and clash-free completion system. Acompletion system S = (T, P,
, ∼) with T = (Va, Vc, E, L) is called I-compatible if there
exist mappings π : Va → ∆I and τ : Vc → ∆D such that
(Ca) C ∈ L(a) ⇒ π(a) ∈ CI
(Cb) b is an R-successor of a ⇒ (π(a), π(b)) ∈ RI
(Cc) x is a g-successor of a ⇒ gI (π(a)) = τ (x)
(Cd) (x1, . . . , xn) ∈ P(P ) ⇒ (τ (x1), . . . , τ (xn)) ∈ P D
(Ce) x ∼ y ⇒ τ (x) = τ (y).
We first establish the following claim:
Claim 1: If a completion system S is I-compatible, then (i) a ≈a b implies π(a) = π(b)and (ii) x ≈c y implies τ (x) = τ (y).
Proof: We show by induction on i that a ≈ia b implies π(a) = π(b) (see Definition 4.3),which yields (i).
• Start. If a ≈0a b, then there exists a nominal N such that N ∈ L(a) ∩ L(b). By (Ca)
we obtain π(a) ∈ N I and π(b) ∈ N I , which yields π(a) = π(b) by definition of thesemantics.
• Step. For a ≈ia b, we distinguish three cases:
1. If a ≈i−1
a
b, then π(a) = π(b) by induction.
2. There is a c ∈ Va and an f ∈ NaF such that both a and b are f /≈i−1
a
-neighbors of
c. Hence, there exist c1, c2 ∈ Va such that c ≈i−1
a
c1 ≈i−1
a
c2, a is an f -successor
of c1, and b is an f -successor of c2. By induction, we have π(c) = π(c1) = π(c2).Thus (Cb) yields (π(c), π(a)), (π(c), π(b)) ⊆ f I , which implies π(a) = π(b) bydefinition of the semantics.
3. There exist (u1, . . . , un keyfor C) ∈ K, ui/≈i−1
a
-neighbors xi of a and ui/≈i−1
a
-
neighbors yi of b for 1 ≤ i ≤ n such that C ∈ L(a)∩L(b) and xi ∼ yi for 1 ≤ i ≤ n.(Ca) yields a, b ∈ CI . Using induction, (Cb), and (Cc), it is straightforward to
713

 
Lutz, Areces, Horrocks, & Sattler
show that uI (π(a)) = τ (x
(π(b)) = τ (y
i
i) and uI
i
i) for 1 ≤ i ≤ n. By (Ce), this
implies uI (π(a)) = uI (π(b)) for 1 ≤ i ≤ k. Since I is a model of the key box K,
i
i
this yields π(a) = π(b) by definition of the semantics.
Now for Part (ii) of Claim 1. If x ≈c y, then either x ∼ y or there is an a ∈ Va and a g ∈ NcFsuch that both x and y are g/≈a-neighbors of a. In the former case, (Ce) yields τ (x) = τ (y).In the latter case, Part (i) of the claim and (Cc) yields (π(a), τ (x)), (π(a), τ (y)) ⊆ gI whichimplies τ (x) = τ (y). This finishes the proof of Claim 1.
We can now show that the completion rules can be applied such that I-compatibility ispreserved.
Claim 2: If a completion system S is I-compatible and a rule R is applicable to S, then Rcan be applied such that an I-compatible completion system S is obtained.
Proof: Let S be an I-compatible completion system, let π and τ be functions satisfying(Ca) to (Ce), and let R be a completion rule applicable to S. We make a case distinctionaccording to the type of R.
R
The rule is applied to a concept C1
C2 ∈ L(a). By (Ca), C1
C2 ∈ L(a) implies
π(a) ∈ (C1
C2)I and hence π(a) ∈ CI and π(a) ∈ CI. Since the rule adds C
1
2
1 and
C2 to L(a), it yields a completion system that is I-compatible via the same π and τ .
R
The rule is applied to C1 C2 ∈ L(a). C1 C2 ∈ L(a) implies π(a) ∈ CI or π(a) ∈ CI.
1
2
Since the rule adds either C1 or C2 to L(a), it can be applied such that it yields acompletion system that is I-compatible via the same π and τ .
R∃ The rule is applied to a concept ∃R.C ∈ L(a), generates a new R-successor b of a and
sets L(b) = C. By (Ca), we have π(a) ∈ (∃R.C)I and, hence, there exists a d ∈ ∆Isuch that (π(a), d) ∈ RI and d ∈ CI . Set π := π ∪ b → d. It is readily checkedthat the resulting completion system is I-compatible via π and τ .
R∀ The rule is applied to a concept ∀R.C ∈ L(a) and adds C to L(b) of an existing
R/≈a-neighbor b of a. Hence, there exists an a such that a ≈a a and b is an R-successor of a . By Part (i) of Claim 1, we have π(a) = π(a ). Thus, by (Ca) we haveπ(a ) ∈ (∀R.C)I while (Cb) yields ((π(a ), π(b)) ∈ RI . By definition of the semantics,π(b) ∈ CI and thus the resulting completion system is I-compatible via π and τ .
(i)
(i)
R∃c The rule is applied to a concept ∃u1, . . . , un.P ∈ L(a) with ui = f
· · · f
g
1
k
i for
i
(i)
1 ≤ i ≤ n. The rule application generates new abstract nodes b
and x
j
j for 1 ≤ i ≤ n
and 1 ≤ j ≤ ki such that
(i)
(i)
– b
is an f
-successor of a for 1 ≤ i ≤ n,
1
1
(i)
(i)
(i)
– b
is an f
-successor of b
for 1 ≤ i ≤ n and 2 ≤ j ≤ k
j
j
j−1
i,
(i)
– xi is gi-successor of b
for 1 ≤ i ≤ n, and
ki
– (x1, . . . , xn) ∈ P(P ).
714

 
Keys, Nominals and Concrete Domains
(i)
By (Ca), we have π(a) ∈ (∃u1, . . . , un.P )I. Hence, there exist d
∈ ∆
j
I for 1 ≤ i ≤ n
and 1 ≤ j ≤ ki and α1, . . . , αn ∈ ∆D such that
(i)
(i)
– (π(a), d
) ∈ (f
)I for 1 ≤ i ≤ n,
1
1
(i)
(i)
(i)
– (d
, d
) ∈ (f
)I for 1 ≤ i ≤ n and 2 ≤ j ≤ k
j−1
j
j
i,
(i)
– gI (d
) = α
i
k
i for 1 ≤ i ≤ n, and
i
– (α1, . . . , αn) ∈ P D.
(i)
(i)
Set π := π ∪
b
→ d  and τ := τ ∪
x
1≤i≤n and 1≤j≤k
i → αi.
i
j
j
1≤i≤n
The resulting completion system is I-compatible via π and τ .
Rch The rule is applied to an abstract node a and a key assertion (u1, . . . , un keyfor C)
∈ K and non-deterministically adds either C or ˙
¬ C. By definition of the semantics,
π(a) ∈ CI or π(a) ∈ ( ˙
¬ C)I . Hence, Rch can be applied such that the resulting
completion system is I-compatible via π and τ .
Rp The rule is applied to a concept C ∈ L(a) and adds C to the label L(b) of a node b
with a ≈a b. By (Ca), we have π(a) ∈ CI. Since Claim 1 yields π(a) = π(b), it followsthat the resulting completion system is I-compatible via π and τ .
Finally, we show that I-compatibility implies clash-freeness.
Claim 3: Every I-compatible completion system is clash-free.
Proof: Let S = (T, P,
, ∼) be an I-compatible completion system. Consider the three
kinds of a clash:
• Due to (Ca), a clash of the form A, ¬A ∈ L(a) clearly contradicts the semantics.
• Assume that there are a ∈ Va and x ∈ Vc such that g↑ ∈ L(a) and x is g/≈a-neighbor
of a. Then there exists b ∈ Va such that a ≈a b and x is g-successor of b. By Claim 1,a ≈a b implies π(a) = π(b). Thus, g↑ ∈ L(a) and (Ca) give π(b) ∈ (g↑)I. We obtain acontradiction since (Cc) yields (π(b), τ (x)) ∈ gI .
• Properties (Cd) and (Ce) and Part (ii) of Claim 1 imply that τ is a solution for ζS.
Thus, S is concrete domain satisfiable.
We can now describe the “guidance” of the tableau algorithm by the model I in detail:we ensure that, at all times, the considered completion systems are I-compatible. Thisobviously holds for the initial completion system
SC = (T , P
= (a
0
C0
∅, ∅, ∅) with TC0
0, ∅, ∅, a0 → C ).
We guide the non-deterministic test function such that, when given a predicate conjunctionζS with set of variables Vc ⊆ Oc as input, it returns the relation ∼ defined by setting x ∼ yiff τ (x) = τ (y) for all x, y ∈ V . The relation ∼ is a concrete equivalence since τ is a solutionfor ζS (see above). With this guidance, (Ce) is obviously satisfied after each call to test, andthe other properties are not affected by such a call. According to Claim 2, we can apply the
715

 
Lutz, Areces, Horrocks, & Sattler
completion rules such that I-compatibility is preserved. By Corollary B.4, the algorithmalways terminates, hence also when guided in this way. Since, by Claim 3, we will not finda clash, the algorithm returns satisfiable.
The tableau algorithm yields decidability and a tight upper complexity bound for ALCOK(D)-concept satisfiability w.r.t. key boxes.
Theorem B.7 (Theorem 4.1 of Section 4.1). Let D be a key-admissible concrete domain.If extended D-satisfiability is in NP, then ALCOK(D)-concept satisfiability w.r.t. Booleankey boxes is in NExpTime.
Proof. Corollary B.4 and Lemmas B.5 and B.6 yield decidability of ALCOK(D)-conceptsatisfiability w.r.t. Boolean key boxes. For complexity, Lemma B.3 provides an exponentialbound on the number of recursive calls. Hence, it remains to show that each single recursionstep needs at most exponential time. By Lemma B.2, the while loop terminates after at mostexponentially many steps. In each such step, we compute the relations ≈a and ≈c, whichare used in the construction of the predicate conjunction ζS and for checking terminationof the while loop. Since, by Lemma B.1, there exists an exponential bound on the numberof abstract and concrete nodes in the completion system S, this can obviously be done inexponential time. Moreover, Lemma B.1 implies that the size of ζS is at most exponential.This together with the fact that extended D-satisfiability is in NP implies that the call totest needs at most exponential time. All remaining tasks (checking for clashes, completeness,and rule applicability) can clearly also be performed in exponential time.
Appendix C. Proofs of Section 4.2
We first provide the proof of Lemma 4.2 which shows that the notion of tableaux introducedin Section 4.2 is an adequate abstraction of models.
Lemma C.1 (Lemma 4.2 in Section 4.2). Let D be a SHOQK(D)-concept in NNF, R arole box, and K a path-free key box in NNF. Then D is satisfiable w.r.t. R and K iff D hasa tableau w.r.t. R and K.
Proof. For the “only-if” direction, we construct a tableau T from a common model I of D,R, and K as follows:
Sa := ∆I
Sc := x ∈ ∆D | gI(s) = x for some s ∈ Sa
L(s) := C ∈ cl(D, R, K) | s ∈ CI 
E(s, t)
:=
S ∈ ND,R,K | (s, t) ∈ SI 
R
e(s, g) := gI (s) if gI (s) is defined
P(P ) := (x1, . . . , xn) ∈ Sn |
c
(x1, . . . , xn) ∈ P D.
It can be easily verified that T is a tableau for D w.r.t. R and K: the proof that T satisfies(T1) – (T9) is identical to the corresponding cases in (Horrocks et al., 2000; Horrocks &Sattler, 2001); (T10) holds by definition of L; (T11) by definition of L and the fact thatnominals are interpreted as singleton sets; (T12) by definition of L, e, and P together with
716

 
Keys, Nominals and Concrete Domains
the semantics of concepts ∃g1, . . . , gn.P ; (T13) since the identity function on Sc is clearly asolution for the listed predicate conjunction; (T14) by definition of L and e together withthe semantics of key constraints; and finally (T15) by definition of L and e together withthe semantics of concepts g↑.
For the “if” direction, let T = (Sa, Sc, L, E, e, P) be a tableau for D w.r.t. R and K and
let δ be a solution for the predicate conjunction in (T13). We construct a model I for Das follows:
∆I
:=
Sa
AI
:=
s ∈ ∆I | A ∈ L(s)
for concept names A
N I
:=
s ∈ ∆I | N ∈ L(s) for nominals N
SI ∪ (s, t) | R ∈ E(s, t)
for R ∈ N
S * R
R  NcF with not Trans(R)
RI
:=
S=R
(s, t) | R ∈ E(s, t)+
for R ∈ NR  NcF with Trans(R)
δ(x)
if e(s, g) = x
gI (s)
:=
for g ∈ N
undefined
if e(s, g) is undefined
cF.
Due to (T11), the interpretation of nominals is a singleton. Moreover, the interpretation ofroles is well-defined since role boxes are acyclic. The following claim is central for provingthat I is indeed a model for D, R, and K:
Claim: For each C ∈ cl(D, R, K), C ∈ L(s) implies s ∈ CI .
Proof: We proceed by induction on the norm ||C|| of C, which is defined as follows:
||A|| := ||¬A||
:=
0 for A concept name
||g↑|| := ||∃u1, . . . , un.P || := 0
||C1
C2|| := ||C1
C2||
:=
1 + ||C1|| + ||C2||
||(
n R C)||
:=
||(
n R C)||
:=
1 + ||C||
For concept names A and nominals N , the claim follows by definition of AI and N I . For thenegation of concept names A and nominals N (note that C is in NNF), the claim follows bydefinition of AI and N I together with (T1). Concepts C of the form C1
C2 and C1
C2
can be treated using (T2) and (T3) together with the induction hypothesis. For existential,universal, and number restrictions, the proof is analogous to the one for SHIQ in (Horrockset al., 2000). For concepts of the form C = ∃g1, . . . gn.P ∈ L(s), s ∈ CI is an immediateconsequence of (T12), the definition of gI , and the fact that (x
i
1, . . . , xn) ∈ P (P ) implies
(δ(x1), . . . , δ(xn)) ∈ P D by (T13). Finally, for concepts C = g↑, s ∈ CI is an immediateconsequence of the definition of gI together with (T15). This finishes the proof of theclaim.
By definition of tableaux, there exists an s0 ∈ Sa such that C ∈ L(s0). By the claim,s0 ∈ CI and thus I is a model of C.
Next, we show that I is a model of R. By definition of RI , it is obvious that Trans(R) ∈
R implies that RI is a transitive relation. Now let S
R ∈ R. If Trans(R) /
∈ R, then we
have SI ⊆ RI by definition of RI . Now let Trans(R) ∈ R and (s, t) ∈ SI . If S ∈ E(s, t),then (T4) implies R ∈ E(s, t), and thus (s, t) ∈ RI . Otherwise, there is an S * S withTrans(S ) ∈ R and (s, t) ∈ (u, v) | S ∈ E(u, v)+. Now (T4) together with S * R implies
717

 
Lutz, Areces, Horrocks, & Sattler
that (u, v) | S ∈ E(u, v) ⊆ (u, v) | R ∈ E(u, v), and thus Trans(R) ∈ R implies that(s, t) ∈ RI .
It remains to show that I is a model of K. To this end, let (g1, . . . , gn keyfor C) ∈ K
and s, t ∈ CI such that gI (s) = gI (t) for 1 ≤ i ≤ n. Since the predicate conjunction in
i
i
(T13) contains explicit inequalities for all distinct concrete individuals, this implies thate(s, gi) = e(t, gi) for 1 ≤ i ≤ n. (T10) implies C, ˙¬ C ∩ L(s) = ∅ and C, ˙¬ C ∩ L(t) = ∅.If ˙
¬ C ∈ L(s), then the claim yields s ∈ ( ˙
¬ C)I contradicting s ∈ CI . Thus we obtain
C ∈ L(s) and, in a similar way, C ∈ L(t). Finally, (T14) implies that s = t, and thus Isatisfies K.
We now proceed to prove termination, soundness, and completeness of the tableau algorithmpresented in Section 4.2, starting with termination. In the following, we use |D, R, K| todenote | cl+(D, R, K)|. Recall that this number is polynomial in the size of D, R, K.
Lemma C.2 (Termination). Let D be a key-admissible concrete domain. When startedwith a SHOQK(D) concept D in NNF, a role box R, and a path-free key box K in NNF,the tableau algorithm terminates.
Proof. Assume that there are D, R, and K such that the tableau algorithm does not ter-minate. Since D is key-admissible, this means that there is an infinite sequence S0, S1, . . .of completion systems such that (a) S0 is the initial completion system SD and (b) Si+1 isthe result of applying a completion rule to Si.
This is only possible if the R∃ or the R
rules are applied infinitely often: it is easily seen
that the rules R , R , R , R∃c, R∀, R∀+, Rch, and R≈a can only be applied finitely oftento completion systems whose set of abstract nodes Va does not increase since they eitheradd concepts into node labels (whose size is bounded), or they add concrete nodes (whosenumber is bounded linearly by the number of abstract nodes), or they remove abstractnodes from the forest. Hence there is a sub-sequence Si , S , . . . of S
1
i2
0, S1, . . . such that
Si is the result of applying the R∃ or the R
rule to S
j
ij −1. Let si
be the abstract node
to which the R∃ or the R
rule was applied in Si −1. Since s
t implies that t was not
generated before s, the linear ordering
is well-founded. Thus, we find an infinite sub-
sequence Sj , S , . . . of S , S , . . . such that either s
for each
≥ 1 or s
1
j2
i1
i2
j
= sj +1
j
sj +1
for each
≥ 1. The former, however, is not possible since the R∃ and the R
rules are
applied at most once per node and concept in cl(D, R, K): even if a node is removed, thelabel copying performed by the R
rule together with clashes of type (C3) ensures that
the R
rule is not re-applied to the same concept and node. Thus only the second option
remains: there is a subsequence Sj , S , . . . of S , S , . . . such that s
for each
1
j2
i1
i2
j
sj +1
≥ 1. Let Lj be the labeling function in Sj. Since each abstract node is labeled with a
subset Lj of cl+(D, R, K), there are nodes sj
s
(s ) = L
k
j
with k
and Ljk jk
j (sj ).
Now node labels can only increase and, if a node t is removed, its label is conjoined to thelabel of a node ˆ
t with ˆ
t
t. Thus there is a node t in the completion system Sj with
t
sj and Lj (sj ) ⊆ Lj (t). By definition, sj is thus blocked in Sj , contradicting the
assumption that the R∃ or the R
rule is applied to sj in Sj .
Lemma C.3 (Soundness). If the expansion rules can be applied to a SHOQK(D) conceptD in NNF, a role box R, and a path-free key box K such that they yield a complete andclash-free completion forest, then D has a tableau w.r.t. R and K.
718

 
Keys, Nominals and Concrete Domains
Proof. Let S = ((Va, Vc, E, L), P, ∼c, ) be a complete and clash-free completion system.We can find a solution δ for ζS such that δ(x) = δ(y) iff x ∼c y: only the R∃c rule updatesthe predicate conjunction ζS, and after each rule application the ∼c relation is updatedusing the concrete equivalence that a D-tester returns for ζS (note that ζS is satisfiable dueto clash-freeness). According to Definition 4.1, we can thus find a solution δ as required.From S and δ, we define a finite tableau T = (Sa, Sc, ˆ
E, ˆ
L, ˆ
P) as follows:
Sa := s ∈ Va | s occurs in S and is not blocked
Sc := δ(x) | (s, x) ∈ E(g) for some s ∈ Sa and some g
ˆ
L(s) := L(s) ∩ cl(D, R, K) (the intersection is due to the auxiliary concepts AnRC
i
),
ˆ
E(s, t)
:=
R | t is an R-successor of s or t blocks an R-successor t of s
δ(x)
if x is a g-successor of s
e(s, g) :=
undefined
if x has no g-successor
ˆ
P
:=
the restriction of P to Sc.
Note that the function e is well-defined due to the definition of adding g-successors. Itremains to show that T satisfies (T1)–(T14), which is basically a consequence of S beingclash-free and complete.
• (T1) is satisfied since S does not contain a clash (C1).
• (T2) is satisfied since the R
rule cannot be applied, and thus C1
C2 ∈ ˆ
L(s) implies
C1, C2 ∈ ˆ
L(s).
• (T3) is satisfied since the R
rule cannot be applied, and thus C1
C2 ∈ ˆ
L(s) implies
C1, C2 ∩ ˆ
L(s) = ∅.
• For (T4), consider s, t ∈ Sa with R ∈ ˆ
E(s, t) and R * R . Then R ∈ ˆ
E(s, t) implies
that t is or blocks an R-successor of s. By definition of “successor”, t is or blocks anR -successor of s, and thus R ∈ ˆ
E(s, t).
• For (T5), let ∀R.C ∈ ˆ
L(s) and R ∈ ˆ
E(s, t). If t is an R-successor of s, then s not
being blocked implies C ∈ L(t) since the R∀ rule cannot be applied. If t blocks anR-successor t of s, then s not being blocked and the fact that the R∀ rule cannot beapplied yields C ∈ L(t ), and the blocking condition implies C ∈ L(t).
In both cases, we thus have C ∈ ˆ
L(t).
• (T6) and (T7) are satisfied for the same reasons as (T5) with R∀ replaced with R∃
and R∀+.
• For (T8), consider s with (
n R C) ∈ ˆ
L(s). Hence (
n R C) ∈ L(s) and
completeness of S implies the existence of R-successors t1, . . . , tn of s with C ∈ L(ti)
.
and ti = tj for i = j. The latter implies, for each i = j, the existence of integers k,such that k = , AnRC ∈ L(t
k
i), and AnRC ∈ L(tj ). For (T8) to be satisfied, it remains
to verify that
– no ti can block a tj: if this was the case, the blocking condition would imply that
AnRC , AnRC  ⊆ L(t
k
i).
719

 
Lutz, Areces, Horrocks, & Sattler
– no t can block both ti and tj with i = j: similarly, this would imply that
AnRC , AnRC  ⊆ L(t).
k
In each case, we would have a clash (C3), in contradiction to S being clash-free.
• For (T9), consider s with (
n R C) ∈ ˆ
L(s). Hence (
n R C) ∈ L(s) and, since
the R
rule cannot be applied, there are at most n R-successors ti of s. Since each
ti is either not blocked or blocked by exactly one other node (due to
being a linear
ordering), there are at most n ui ∈ Sa with R ∈ ˆ
E(s, ui) and C ∈ ˆ
L(ui).
• For (T10), let (
n R C) ∈ ˆ
L(s) and R ∈ ˆ
E(s, t). Hence (
n R C) ∈ L(s) and
t either is an R-successor of s or blocks an R-successor of s. In the first case, non-applicability of the Rch rule implies that C, ˙
¬ C ∩ L(t) = ∅. In the second case,
C, ˙
¬ C ∩ L(t ) = ∅ for t the R-successor of s blocked by t, and thus the blocking
condition yields C, ˙
¬ C ∩ L(t) = ∅. In both cases, this implies C, ˙
¬ C ∩ ˆ
L(t) = ∅.
Next, consider (g1, . . . , gn keyfor C) ∈ K and s such that e(s, gi) is defined for eachi. Hence s has a gi-successor for each i, and thus s not being blocked and the non-applicability of the Rch rule imply that C, ˙
¬ C ∩ ˆ
L(t) = ∅.
• For (T11), consider N ∈ ˆ
L(s) ∩ ˆ
L(t). By definition, N ∈ L(s) ∩ L(t) and thus s ≈a t.
Moreover, totality of
implies that we can assume without loss of generality that
s
t or s = t. Thus non-applicability of the R≈a rule implies that L(t) ⊆ L(s), and
thus t not being blocked implies s = t.
• (T12) is satisfied since the rule R∃c cannot be applied.
• For (T13), clash-freeness implies the satisfiability of
P (x1, . . . , xn).
P used in D,K (x1,...,xn)∈P(P )
By choice of δ, δ(x) = δ(y) iff x ∼c y, and thus (T13) is satisfied.
• For (T14), let (g1, . . . , gn keyfor C) ∈ K, C ∈ ˆ
L(s) ∩ ˆ
L(t), and e(s, gi) = e(t, gi), for
all 1 ≤ i ≤ n. Thus C ∈ L(s) ∩ L(t) and, by choice of e and δ, we have xi ∼c yifor gi ∈ E(s, xi) ∩ E(t, yi). Hence s ≈a t. Without loss of generality, we assume thats
t or s = t. Thus non-applicability of the R≈a rule implies that L(t) ⊆ L(s), and
thus t not being blocked implies s = t.
• (T15) is satisfied by definition of T and since S does not contain a clash (C4).
Lemma C.4 (Completeness). If a SHOQK(D)-concept D in NNF has a tableau w.r.t. arole box R and a path-free key box K, then the expansion rules can be applied to D, R, andK such that they yield a complete and clash-free completion forest.
720

 
Keys, Nominals and Concrete Domains
Proof. Given a tableau T = (Sa, Sc, ˆ
L, ˆ
E, e, ˆ
P) for D w.r.t. R and K, we can “guide” the
non-deterministic rules R , Rch, and R≈a in such a way that each rule application preservesclash-freeness. This together with termination from Lemma C.2 finishes the proof.
Along with rule application, we perform a stepwise construction of a total mapping π
that takes abstract nodes of the completion forest to elements of Sa and concrete nodes ofthe completion forest to elements of Sc.
• L(s) ∩ cl(D, R, K) ⊆ ˆ
L(π(s)) for each s ∈ Va,
• if t is an R-successor of s, then R ∈ ˆ
E(π(s), π(t)),
• if x is a g-successor of s, then e(π(s), g) = π(x),
• x ∼c y iff π(x) = π(y), and
.
• if s = t, then π(s) = π(t).
A mapping satisfying these four conditions is called correct in the following. Note that acompletion system for which there exists a correct mapping does not contain a clash: due to(T1) and the first property, we do not encounter a clash (C1). A clash (C3) cannot occurdue to the last property. The first and the third property together with (T15) ensure thata clash (C4) does not occur. Finally, a clash (C2) cannot occur for the following reason:by construction of P and since edges labelled with abstract features are never removed, foreach tuple (x1, . . . , xn) ∈ P(P ), we find an abstract node s and paths u1, . . . , un such that∃u1, . . . , un.P ∈ L(s) and xi is a ui-successor of s for 1 ≤ i ≤ n. Thus, the first, second,and third property together with (T12) and (T13) ensure that the conjunction
P (π(x1), . . . , π(xn))
P used inD,K
(x1,...,xn)∈P(P )
has a solution δ with δ(π(x)) = δ(π(x)) iff π(x) = π(y). By the fourth property, settingδ (x) := δ(π(x)) for all x ∈ Vc thus yields a solution δ for ζS.
The total mapping π is inductively defined as follows: let δ be a solution for the equation
in (T13). Choose a node ˆ
s0 with D ∈ ˆ
L(ˆ
s0), and set π(s0) := ˆ
s0 for s0 the (only) node of the
initial completion forest. Obviously, π is correct. We will now show that each completionrule can be applied in such a way that π either is still correct or that π can be extended toa correct mapping.
• An application of the rule R
preserves correctness of π due to (T2).
• Due to (T3), the rule R
can be applied such that correctness is preserved.
• If the rule R∃ adds a new node t for ∃R.C ∈ L(s), then correctness implies ∃R.C ∈
ˆ
L(π(s)), and thus (T6) implies the existence of some ˆ
t ∈ Sa with R ∈ E(π(s), ˆ
t) and
C ∈ ˆ
L(ˆ
t). Thus extending π with π(t) := ˆ
t obviously yields a correct mapping.
• If the rule R
adds n nodes ti for (
n R C) ∈ L(s), then correctness implies
(
n R C) ∈ ˆ
L(π(s)), and thus (T8) implies the existence of ˆ
t1, . . . , ˆ
tn ∈ ˆ
Sa with
ˆ
ti = ˆ
tj for i = j, R ∈ E(π(s), ˆ
ti), and C ∈ ˆ
L(ˆ
ti). Thus extending π with π(ti) := ˆ
ti
obviously yields a correct mapping.
721

 
Lutz, Areces, Horrocks, & Sattler
• Assume that the R
rule is applicable to a node s with (
n R C) ∈ L(s) and more
than n R-successors ti with C ∈ L(ti). Then correctness implies that (
n R C) ∈
ˆ
L(π(s)), R ∈ ˆ
E(π(s), π(ti)), and C ∈ ˆ
L(ti). Thus, by (T9), there are i = j with
.
π(ti) = π(tj). Again, correctness implies that not ti = tj and, without loss of general-ity, we can assume that ti
tj. Hence applying the rule and thereby merging L(tj)
into L(ti) preserves correctness.
• For the rule R∃c, π can be extended in a similar way as for R∃: if a new gi-successor xi
of s is added, then extending π with π(xi) := e(π(s), gi) yields a correct π. Moreover,(T13) ensures that ∼c can be updated in such a way that the fourth condition ispreserved.
• For the R∀ rule, π does not need to be extended, and (T5), (T4), and the definition
of R-successors imply that correctness is preserved.
• The R∀+ rule is similar, with the only difference that (T7) takes the place of (T5).
• Due to (T10), the rule Rch can be applied without violating correctness.
• For R≈a, we consider two reasons for R≈a to be applicable:
– N ∈ L(s) ∩ L(t). Then correctness of π and (T11) imply that π(s) = π(t).
– (g1, . . . , gn keyfor C) ∈ K, C ∈ L(s) ∩ L(t), and gi ∈ E(s, xi) ∩ E(t, yi) and
xi ∼c yi for 1 ≤ i ≤ n. Then correctness implies that ˆe(π(s), gi) = e(π(t), gi), andthus (T14) together with the first property of correctness imply that π(s) = π(t).
In both cases, applying R≈a to s and t preserves correctness.
As an immediate consequence of Lemmas 4.2, C.2, C.3, and C.4, the tableau algorithmalways terminates and answers “D is satisfiable w.r.t. R and K” if and only if the inputconcept D is satisfiable w.r.t. the input role box R and the input key box K. Since conceptsatisfiability w.r.t. TBoxes can be reduced to concept satisfiability without TBoxes, weobtain the following result:
Proposition C.5. Let D be a key-admissible concrete domain.
The tableau algorithm
decides satisfiability of SHOQK(D) concepts w.r.t. TBoxes, role boxes, and path-free keyboxes.
It is not hard to verify that the proof of Lemma C.4 together with Lemmas 4.2 and C.2yield a bounded model property for SHOQK(D), where the bound is exponential.
Corollary C.6. If a SHOQK(D)-concept D is satisfiable w.r.t. a role box R and a path-free key box K, then D is satisfiable w.r.t. R and K in a model of size at most |∆I| ≤ 2mfor m =  cl+(D, R, K).
722

 
Keys, Nominals and Concrete Domains
Proof. If a SHOQK(D)-concept D is satisfiable w.r.t. a role box R and a path-free keybox K, Lemma C.4 implies that the tableau algorithm constructs a complete and clash-freecompletion forest for D, R, and K. By the definition of blocking, the number of abstractnodes in a completion forest that are not blocked is bounded by 2m: if s = t ∈ Va areabstract nodes in a completion forest and L(s) = L(t), then either s blocks t, t blocks s, orthey are both blocked by another node u. Moreover, it is easily seen that the number ofconcrete successors per abstract node is bounded by the number of concrete features in C, R,and K. Now, in the proof of Lemma C.4, the abstract nodes in the tableau constructed froma complete and clash-free completion forest coincide with the nodes that are not blockedin the completion forest. Finally, in the proof of Lemma 4.2 the interpretation domainof a model constructed from a tableau coincides with the abstract nodes in the tableau.Summing up, a SHOQK(D)-concept that is satisfiable w.r.t. R and K has a model of size|∆I| ≤ 2m.
References
Areces, C., Blackburn, P., & Marx, M. (1999). A road-map on complexity for hybrid logics.
In Flum, J., & Rodr´ıguez-Artalejo, M. (Eds.), Computer Science Logic, No. 1683 inLecture Notes in Computer Science, pp. 307–321. Springer-Verlag.
Baader, F., Horrocks, I., & Sattler, U. (2002a). Description logics for the semantic web. KI
– K¨
unstliche Intelligenz, 16 (4), 57–59.
Baader, F., Lutz, C., Sturm, H., & Wolter, F. (2002b). Fusions of description logics and
abstract description systems. Journal of Artificial Intelligence Research (JAIR), 16,1–58.
Baader, F., & Sattler, U. (1998). Description logics with concrete domains and aggrega-
tion. In Prade, H. (Ed.), Proceedings of the 13th European Conference on ArtificialIntelligence (ECAI’98), pp. 336–340. John Wiley & Sons.
Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., & Patel-Schneider, P. F. (2003).
The Description Logic Handbook: Theory, implementation and applications. Cam-bridge University Press, Cambridge, MA, USA.
Baader, F., & Hanschke, P. (1991a). A scheme for integrating concrete domains into concept
languages. In Proceedings of the 12th International Joint Conference on ArtificialIntelligence (IJCAI-91), pp. 452–457, Sydney, Australia.
Baader, F., & Hanschke, P. (1991b). A scheme for integrating concrete domains into concept
languages. DFKI research report RR-91-10, German Research Center for ArtificialIntelligence (DFKI).
Baader, F., & Hanschke, P. (1992).
Extensions of concept languages for a mechanical
engineering application. In Proceedings of the 16th German AI-Conference (GWAI-92), Vol. 671 of Lecture Notes in Computer Science, pp. 132–143. Springer-Verlag.
Baader, F., & Sattler, U. (2000). Tableau algorithms for description logics. In Dyckhoff,
R. (Ed.), Proceedings of the International Conference on Automated Reasoning withTableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in ArtificialIntelligence, pp. 1–18. Springer-Verlag.
723

 
Lutz, Areces, Horrocks, & Sattler
Berger, R. (1966). The undecidability of the domino problem. Memoirs of the American
Mathematical Society, 66, 1–72.
Berners-Lee, T., Hendler, J., & Lassila, O. (2001). The semantic web. Scientific American,
284 (5), 34–43.
B¨
orger, E., Gr¨
adel, E., & Gurevich, Y. (1997). The Classical Decision Problem. Perspectives
in Mathematical Logic. Springer-Verlag.
Borgida, A., & Patel-Schneider, P. F. (1994). A semantics and complete algorithm for
subsumption in the CLASSIC description logic. Journal of Artificial Intelligence Re-search, 1, 277–308.
Borgida, A., & Weddell, G. E. (1997). Adding uniqueness constraints to description logics
(preliminary report). In Bry, F., Ramakrishnan, R., & Ramamohanarao, K. (Eds.),Proceedings of the 5th International Conference on Deductive and Object-OrientedDatabases (DOOD97), Vol. 1341 of LNCS, pp. 85–102. Springer.
Calvanese, D., De Giacomo, G., & Lenzerini, M. (1998). On the decidability of query
containment under constraints. In Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS’98), pp. 149–158.
Calvanese, D., De Giacomo, G., & Lenzerini, M. (2000). Keys for free in description logics.
In Baader, F., & Sattler, U. (Eds.), Proceedings of the 2000 International Workshop inDescription Logics (DL2000), No. 33 in CEUR-WS (http://ceur-ws.org/), pp. 79–88.
Calvanese, D., Lenzerini, M., & Nardi, D. (1998). Description logics for conceptual data
modeling. In Chomicki, J., & Saake, G. (Eds.), Logics for Databases and InformationSystems, pp. 229–263. Kluwer Academic Publisher.
Dean, M., Connolly, D., van Harmelen, F., Hendler, J., Horrocks, I., McGuinness, D. L.,
Patel-Schneider, P. F., & Stein, L. A. (2002). Web ontology language (OWL) referenceversion 1.0. W3C Working Draft.
Fensel, D., van Harmelen, F., Horrocks, I., McGuinness, D. L., & Patel-Schneider, P. F.
(2001).
OIL: An ontology infrastructure for the semantic web.
IEEE Intelligent
Systems, 16 (2), 38–45.
Graham, R. L., Knuth, D. E., & Patashnik, O. (1990). Concrete Mathematics. Addison
Wesley Publ. Co., Reading, Massachussetts.
Haarslev, V., Lutz, C., & M¨
oller, R. (1998). Foundations of spatioterminological reasoning
with description logics. In Cohn, A., Schubert, L., & S.C.Shapiro (Eds.), Proceedingsof the 6th International Conference on Principles of Knowledge Representation andReasoning (KR’98), pp. 112–124. Morgan Kaufman.
Haarslev, V., & M¨
oller, R. (2001).
RACER system description.
In Gor´
e, R., Leitsch,
A., & Nipkow, T. (Eds.), Proceedings of the 1st International Joint Conference onAutomated Reasoning (IJCAR’01), No. 2083 in Lecture Notes in Artificial Intelligence,pp. 701–705. Springer-Verlag.
Haarslev, V., M¨
oller, R., & Wessel, M. (2001). The description logic ALCN HR+ extended
with concrete domains: A practically motivated approach. In Gor´
e, R., Leitsch, A.,
724

 
Keys, Nominals and Concrete Domains
& Nipkow, T. (Eds.), Proceedings of the 1st International Joint Conference on Auto-mated Reasoning IJCAR’01, No. 2083 in Lecture Notes in Artificial Intelligence, pp.29–44. Springer-Verlag.
Halpern, J. Y., & Moses, Y. (1992). A guide to completeness and complexity for modal
logics of knowledge and belief. Artificial Intelligence, 54 (3), 319–380.
Hollunder, B., & Baader, F. (1991). Qualifying number restrictions in concept languages.
In Proceedings of the 2nd International Conference on Principles of Knowledge Rep-resentation and Reasoning (KR’91), pp. 335–346, Boston, MA, USA.
Hopcroft, J. E., & Ullman, J. D. (1979). Introduction to Automata Theory, Languages and
Computation. Addison-Wesley.
Horrocks, I., Sattler, U., & Tobies, S. (2000). Practical reasoning for very expressive de-
scription logics. Logic Journal of the IGPL, 8 (3), 239–264.
Horrocks, I. (1998). Using an expressive description logic: FaCT or fiction?. In Proceedings
of the 6th International Conference on the Principles of Knowledge Representationand Reasoning (KR98), pp. 636–647.
Horrocks, I. (2002). Reasoning with expressive description logics: Theory and practice. In
Voronkov, A. (Ed.), Proceedings of the 18th International Conference on AutomatedDeduction (CADE 2002), No. 2392 in Lecture Notes in Artificial Intelligence, pp. 1–15.Springer.
Horrocks, I., Patel-Schneider, P. F., & van Harmelen, F. (2002). Reviewing the design of
DAML+OIL: An ontology language for the semantic web. In Proceedings of the 18thNational Conference on Artificial Intelligence (AAAI 2002), pp. 792–797.
Horrocks, I., & Sattler, U. (2001). Ontology reasoning in the SHOQ(D) description logic. In
Nebel, B. (Ed.), Proceedings of the 17th International Joint Conference on ArtificialIntelligence (IJCAI’01), pp. 199–204. Morgan-Kaufmann.
Horrocks, I., Sattler, U., & Tobies, S. (1999). Practical reasoning for expressive description
logics. In Ganzinger, H., McAllester, D., & Voronkov, A. (Eds.), Proceedings of the6th International Conference on Logic for Programming and Automated Reasoning(LPAR’99), No. 1705 in Lecture Notes in Artificial Intelligence, pp. 161–180. Springer-Verlag.
Kamp, G., & Wache, H. (1996). CTL - a description logic with expressive concrete domains.
Tech. rep. LKI-M-96/01, Laboratory for Artificial Intelligence (LKI), Universitity ofHamburg, Germany.
Khizder, V. L., Toman, D., & Weddell, G. E. (2001). On decidability and complexity of de-
scription logics with uniqueness constraints. In den Bussche, J. V., & Vianu, V. (Eds.),Proceedings of the 8th International Conference on Database Theory (ICDT2001), Vol.1973 of LNCS, pp. 54–67. Springer.
Knuth, D. (1968). The Art of Computer Programming, Vol. 1. Addison-Wesley.
Lutz, C. (2003). Description logics with concrete domains—a survey. In Advances in Modal
Logics Volume 4, pp. 265–296. World Scientific Publishing Co. Pte. LTd.
725

 
Lutz, Areces, Horrocks, & Sattler
Lutz, C. (2002a). The Complexity of Reasoning with Concrete Domains. Ph.D. thesis,
LuFG Theoretical Computer Science, RWTH Aachen, Germany.
Lutz, C. (2002b). PSpace reasoning with the description logic ALCF(D). Logic Journal
of the IGPL, 10 (5), 535–568.
Lutz, C. (2002c). Reasoning about entity relationship diagrams with complex attribute
dependencies. In Horrocks, I., & Tessaris, S. (Eds.), Proceedings of the InternationalWorkshop in Description Logics 2002 (DL2002), No. 53 in CEUR-WS (http://ceur-ws.org/), pp. 185–194.
Lutz, C. (2004).
NExpTime-complete description logics with concrete domains.
ACM
Transactions on Computational Logic, 5 (4), 669–705.
Lutz, C., Areces, C., Horrocks, I., & Sattler, U. (2002). Keys, nominals, and concrete
domains. LTCS-report 02-04, Technical University Dresden. See http://lat.inf.tu-dresden.de/research/reports.html.
Lutz, C., Areces, C., Horrocks, I., & Sattler, U. (2003). Keys, nominals, and concrete
domains. In Proceedings of the 18th International Joint Conference on Artificial In-telligence (IJCAI’03), pp. 349–354. Morgan-Kaufmann Publishers.
Pan, J. Z., & Horrocks, I. (2002). Reasoning in the SHOQ(Dn) description logic. In Hor-
rocks, I., & Tessaris, S. (Eds.), Proceedings of the International Workshop in Descrip-tion Logics 2002 (DL2002), No. 53 in CEUR-WS (http://ceur-ws.org/), pp. 53–62.
Post, E. M. (1946). A variant of a recursively unsolvable problem. Bulletin of the American
Mathematical Society, 52, 264–268.
Schild, K. D. (1991). A correspondence theory for terminological logics: Preliminary report.
In Mylopoulos, J., & Reiter, R. (Eds.), Proceedings of the 12th International JointConference on Artificial Intelligence (IJCAI-91), pp. 466–471. Morgan Kaufmann.
Schmidt-Schauß, M., & Smolka, G. (1991). Attributive concept descriptions with comple-
ments. Artificial Intelligence, 48 (1), 1–26.
726