Reasoning with Concrete Domains

1 Introduction

Description logics are knowledge representation and reason­ ing formalisms dealing with conceptual knowledge on an ab­ stract logical level. However, for a variety of applications, it is essential to integrate the abstract knowledge with knowl­ edge of a more concrete nature. Examples of such "concrete knowledge" include all kinds of numerical data as well as temporal and spatial information. Important application ar­ eas which have been found to depend on integrated reasoning with concrete knowledge are, e.g., mechanical engineering [Baader and Hanschke, 1993], reasoning about aggregation in databases [Baader and Sattler, 1998], as well as temporal and spatial reasoning (see [Haarslev et al., 1998] and [Lutz, 1998]). Many description logic systems such as e.g. CLASSIC and KRIS (see [Borgida eta!., 1989], [Baader and Hollun­ der, 1991 ], resp.), provide interfaces that allow the attachment of external reasoning facilities which deal with concrete in­ formation. Surprisingly, the complexity of combined reason­ ing with abstract and concrete knowledge has, to the best of our knowledge, never been formally analyzed and provably optimal algorithms have not been developed. Recent efficient implementations of expressive description logics like FACT (see [Horrocks, 1998]) concentrate on logics for which rea­ soning is in PSPACE. An important reason why these systems fail to integrate concrete knowledge is that no complexity re­ sults and no efficient algorithms are available.

Baader and Hanschke [1991] extend description logics by concrete domains, a theoretically well-founded approach to integrated reasoning with abstract and concrete knowledge. On basis of the well-known description logic A.CC, they de­ fine the description logic A.CC(V), which can be param­ eterized by a concrete domain V . In this paper, we ex­ tend A.CC(V) by the operators feature agreement and fea­ ture disagreement. This leads to the new logic A.CC:F(V), which combines A.CC(V) with the logic A.CC:F [Hollun­ der and Nutt, 1990]. Algorithms for deciding the concept satisfiability and ABox consistency problems for the logic A.CC:F(V) are given. Furthermore, the complexity of rea­ soning with A.CC:F(V) is formally analyzed. Since reason­ ing with A.CC:F(V) involves a satisfiability check for the concrete domain, the complexity of the combined formal­ ism depends on the complexity of reasoning in the con­ crete domain. The proposed algorithms are proved to need polynomial space which implies that, first, reasoning with A.CC:F(V) is PSPACE-complete provided that reasoning with the concrete domain is in PSPACE, and, second, the devised algorithms are optimal. The obtained complexity results carry over to the description logic A.CC(V). The algorithmic tech­ niques introduced in this paper are vital for efficient imple­ mentations of both A.CC:F(V) and A.CC(V).

As a simple example illustrating the expressivity of A.CC:F(V), consider the concept Man n wifdboss n 3wage, (wife wage). >. In this example, Man is a primi­ tive concept, wife and wage are features (i.e., single valued roles), and > is a concrete predicate. The given concept de­ scribes the set of men whose boss coincides with their wife and who, furthermore, have a higher wage than their wife. In this example, the wage of a person is knowledge of a con­ crete type while being a man is knowledge of a more abstract nature. The coincidence of wife and boss is described using the feature agreement operator _j.. and cannot be expressed in A.CC(V). The syntax used is defined in the next section.

2 The Description Logic A.CC:F(D)

In this section, the description logic A.CC:F(V) is introduced. We start the formal specification by recalling the definition of a concrete domain given in [Baader and Hanschke, 1991].

Definition 1. A concrete domain V is a pair (6.v, <I>v), where 6.v is a set called the domain, and <I>v is a set of predicate names. Each predicate name Pin <T>v is associated with an arity n and an n-ary predicate pv <;;; 6.1J. A concrete domain V is called admissible iff (1) the set of its predicate names is closed under negation and contains a name Tv for 6.v and (2) the satisfiability problem for finite conjunctions of predicates is decidable.

On the basis of concrete domains, the syntax of A£C:F(V) concepts can be defined.

Definition 2. Let C, R, and F be disjoint sets of concept, role, and feature names 1 . A composition f J.f 2 · ·1 n of fea­ tures is called a feature chain. Any element of C is a con­ cept. If C and D are concepts, R is a role or feature, P E <l>v is a predicate name with arity n, and u1 , ... ,un are feature chains, then the following expressions are also concepts:

• ·C (negation), CnD (conjunction), CUD (disjunction), 1:/R.C (value restriction), 3R.C (exists restriction),
• 3u1 , . .. , Un .P (predicate operator)
• ud.u2 (feature agreement), u1 tu2 (feature disagreement).

A simple feature is a feature chain of length one. For a feature chain u = h · · 1 n, 3u.C and 1:/u.C will be used as abbrevi­ ations for 3/1 .. .. 3f n·C and 1:/h . ... 1:/f n·C, respectively. As usual, a set theoretic semantics is given.

Definition 3. An interpretation I = ( 6.I , .I) consists of a set 6.I (the abstract domain) and an interpretation function .I. The sets 6.v and 6.I must be disjoint. The interpretation function maps each concept name C to a subset ci of 6.I, each role name R to a subset RI of 6.I x 6.I, and each feature name f to a partial function fi from 6.I to 6.v U 6.I, where fi(a) = x will be written as (a,x) E fi . If u = h · · ·!k is a feature chain, then ui is defined as the composition ff o · · · o ff of the partial functions If, . .. Jf. Let the symbols C, D, R, P, and u1 , ... ,un be defined as in Definition 2. Then the interpretation function can be extended to complex concepts as follows:

1 In the following, the notion role (feature) is used synonymously for role name (feature name).

An interpretation I is a model of a concept C iff ci -:j: 0. A concept C is satisfiable iff there exists a model I of C. A concept C subsumes a concept D (written D -< C) iff DI C ci for all interpretations I. - -

Subsumption can be reduced to satisfiability since D ~ C iff the concept D n ·C is unsatisfiable. Please note that the fea­ ture agreement and feature disagreement operators consider only objects from 6.I and no objects from 6.v . Agreement and disagreement over concrete objects can be expressed by using a concrete domain which includes an equality predicate. Using disjunction, "global" agreement and disagreement over both the concrete and the abstract domain can then also be ex­ pressed (see [Lutz, 1998]). This approach was chosen since global agreement and disagreement are not considered to be very "natural" operators. We will now introduce the asser­ tional formalism of A£C:F(V).

Definition 4. Let 0 v and 0 A be disjoint sets of ob­ ject names. Elements of 0 D are called concrete objects and elements of 0 A are called abstract objects. If C, R, f, and P are defined as in Definition 2, a and b are elements of OA and x, x1, ... ,Xn are elements of Ov, then the following expressions are assertional axioms:

A finite set of assertional axioms is called an A£C:F(V) ABox. An interpretation for the concept language can be extended to the assertional language by mapping every object name from 0 A to an element of 6.I and every object name from 0 D to an element of 6.v. The unique name assumption is not imposed, i.e. ai = bi may hold even if a and b are distinct ob­ ject names. An interpretation satisfies an assertional axiom

An interpretation is a model of an ABox A iff it satisfies all assertional axioms in A. An ABox is consistent iff it has a model.

Satisfiability of concepts, as introduced in Definition 3, can be reduced to ABox consistency since a concept C is satisfi­ able iff the ABox {a: C} is consistent. In the next section, an algorithm for deciding the consistency of A£C:F(V) ABoxes is presented.

3 Algorithms

Completion algorithms, also known as tableau algorithms, are frequently used to decide concept satisfiability and ABox consistency for various description logics. Completion algo­ rithms work on (possibly generalized) ABoxes and are char­ acterized by a set of completion rules and a strategy to apply these rules to the assertional axioms of an ABox. The algo­ rithm starts with an initial ABox Ao whose consistency is to be decided. If the satisfiability of a concept Cis to be decided, the ABox {a: C} is considered. The algorithm repeatedly ap­ plies completion rules adding new axioms, and, by doing so, makes all knowledge implicitely contained in the ABox ex­ plicit. If the algorithm succeeds to construct an ABox which is complete (i.e., to which no more completion rules are appli­ cable) and which does not contain an obvious contradiction, then Ao has a model. Otherwise, Ao does not have a model.

In [Hollunder and Nutt, 1990], a completion algorithm for deciding the satisfiability of A£CF concepts is given which can be executed in polynomial space. In [Baader and Han­ schke, 1991 ], an algorithm for deciding the consistency of A£C(V) (i .e., A£CF(V) without feature agreement and dis­ agreement) ABoxes is given. However, this algorithm needs exponential space in the worst case. This is due to the fact that the algorithm collects all axioms of the form (x1, ... , Xn) : P (concrete domain axioms) obtained during rule application, conjoins them into one big conjunction c, and finally tests c for satisfiability w.r.t. the concrete domain. Unfortunately, the size of this conjunction may be exponential in the size of Ao (see [Lutz, 1998] for an example). To obtain a polynomial space algorithm for deciding the consistency of A£CF(V) ABoxes, the concrete domain satisfiability test has to be bro­ ken up into independent "chunks" of polynomial size.

The completion algorithm for deciding the consistency of A£CF(V) ABoxes is developed in two steps: First, an algo­ rithm for deciding the satisfiability of A£CF(V) concepts is devised. Second, an algorithm is given which reduces ABox consistency to concept satisfiability by constructing a num­ ber of "reduction concepts" for a given ABox Ao. A similar reduction can be found in [Hollunder, 1994].

Before giving a formal description of the completion algorithms themselves, the completion rules are defined. To define the rules in a succinct way, the functions succA and chainA are introduced. Let A be an ABox. For an object a E 0 A and a feature chain u, succA(a, u) denotes the object b that can be found by following u starting from a in A. If no such object exists, succA(a, u) denotes the special object E that cannot be part of any ABox. An object name a E 0 A is called fresh in A if a is not used in A. Let a be an object from OA, x be an object from Ov, and u = h · · ·!k be a feature chain. The function chain is defined as follows :

Now, the set of completion rules can be formulated. Please note that the completion rule RU is nondeterministic, i.e., there is more than one possible outcome of a rule application.

Definition 5. The following completion rules replace a given ABox A nondeterministically by an ABox A'. An ABox A is said to contain a fork (for a feature f) iff it contains the two axioms (a, b) :f and (a, c) :for the two axioms (a,x) :f and (a,y) :f, where b, c E OA and x, y E Ov . A fork can be eliminated by replacing all occurrences of c in A with b, or of x with y, resp. It is assumed that forks are eliminated as soon as they appear (as part of the rule application) with the proviso that newly generated objects are replaced by older ones and not vice versa. In the following, C and D denote concepts, R a role, f a feature, P a predicate name from <l>v with arity n, u1 , ... ,un feature chains, a and b objects from OA, and x1, ... , Xn objects from Ov.

Rn The conjunction rule.

Ifa :C nD E A, {a :C, a :D} ~A

then A' =AU{a :C, a:D}

RU The (nondeterministic) disjunction rule. Ifa :CUDEA, {a:C, a:D}nA=0 then A' = A u {a : C} v A' = A u {a : D}

Rr3C, RGC The role/feature exists restriction rule. Ifa :3R.CEA, ~bEOA : {(a ,b) :R, b:C}<:;;A then A'= AU {(a , b) :R, b: C} where bE OA is fresh in A. This is the Rr3C rule. To obtain RGC, replace R by f.

RrV'C, Rf:YC The role/feature value restriction rule. Ifa :V'k.CEA, 3bEOA : (a , b) :REAI\b:C ~A then A' = A u { b: C}

This is the RrV'C rule. To obtain Rf:YC, replace R by f.

R3P The predicate exists restriction rule (may create forks).

If a: 3ul ' ... 'Un .P E A , tlxl' ... 'Xn E 0 D :

(succA(a, u!) =X! 1\ . .. 1\ succA(a, un) = Xn 1\ (xJ, .. . ,xn): PE A)

then Co := AU {(x,, ... ,xn) :P}

where the x; E 0 D are distinct and fresh in A.

cl :=chaine a (a, X!' ui), ... 'Cn := chaincn-1 (a, Xn, Un)

A' = u i=O ... n C;

R.!. The agreement rule (may create forks).

If a: u1.!.u2 E A , ~bE OA: succA(a, u,) = succA(a, u2) = b then C =AU chainA(a, b, u,) where bE OA is fresh in A. A'= C U chainc(a,b, u2)

Rt The disagreement rule (may create forks).

Ifa:u1tu2 E A, ~b1,b2 E OA:

(succA(a, u1) = b, 1\ succA(a, u2) = b2 1\ b1 # b2 E A)

then C =AU chainA(a, b, , u!)

A'= C U chainc(a, b2, u2) U {b1 # b2}

where b,, b2 E 0 A are distinct and fresh in A.

Rule applications that generate new objects are called generating. All other rule applications are called non­ generating. All applications of the Rr:JC rule are generating. Application of the rules RSC, R:JP, R.!., Rt are usually generating but may be non-generating if fork elimination takes place.

A formalized notion of contradictory and of complete ABoxes is introduced in the following.

Definition 6. Let the same naming conventions be given as in Definition 5. An ABox A is called contradictory if one of the following clash triggers is applicable. If none of the clash triggers is applicable to an ABox A, then A is called clash-free.

• Primitive clash: {a: C, a: -.C} ~ A
• Featuredomainclash: {(a,x):f , (a,b):f} ~A
• All domain clash: {(a,x):f, a :'Vf.C} ~A
• Agreement clash: a =f. a E A

An ABox to which no completion rule is applicable is called complete. An ABox A is called concrete domain satisfi­ able iff there exists a mapping J from Ov to V, such that t\cx 1 , ·.· ,xn!PEA (J(xi), · · ·, J(xn)) E pV is true in D.

define procedure sat( A) A' := feature-complete(A) if A' contains a clash then return inconsistent C :={a E A' I a is of the form (xt, .. . ,xn) :P} ifsatisfiable?(D,C) =no then return inconsistent forall a: 3kD E A', where R is a role, do Let b be an object name from 0 A. ifsat({b :D} U {b:£ I a:'ikE E A'}) returns inconsistent then return inconsistent return consistent define procedure feature-complete( A) while a rule r from the set {Rn, RU, RGC, Rf'iC, R:JP, R.). , Rt} is applicable to A, do A := Au apply(A, r) return A

We are now ready to define the completion algorithm sat for deciding the satisfiability of A£C:F(V) concepts. Sat takes an ABox {a : C} as input, where C has to be in negation normal form, i.e., negation is allowed only in front of concept names. Conversion to NNF can be done by exhaustively ap­ plying appropriate rewrite rules to push negation inwards. We only give the conversion rules needed for the new construc­ tors feature agreement and feature disagreement, and refer to [Baader and Hanschke, 1991] for the A£C (V) rule set.

Any A£C:F(V) concept can be converted into an equivalent concept in NNF in linear time. Some comments about the application of nondeterministic completion rules are in order. The application of the nondeterministic rule RU yields more . than one possible outcome. It. is not specified which possibil­ ity is chosen in a given run of a completion algorithm. This means that the algorithms to be specified are nondeterministic algorithms. Such algorithms returns a positive result if there is any way to make the nondeterministic decisions such that a positive result is obtained.

The satisfiability algorithm makes use of two auxiliary functions which will be described only informally. The func­ tion apply takes two arguments, an ABox A and a completion ruler. It applies r once to arbitrary axioms from A match­ ing r 's premise and (nondeterministically) returns a descen­ dant of A that is obtained by rule application. The function satisfiable? takes as arguments a concrete domain V and a set C of concrete domain axioms. It returns yes if the conjunction of all axioms inC is satisfiable w.r.t. V and no otherwise. The sat algorithm is given in figure 1. Based on sat, we define the ABox-cons algorithm for deciding ABox consistency. This algorithm can be found in figure 2.

A formal correctness proof for the algorithms is omitted for the sake of brevity and can be found in [Lutz, 1998]. A

short, informal discussion of the employed strategies is given instead. The sat algorithm performs depth-first search over role successors. This technique, first introduced by Schmidt­ SchauB and Smolka [ 1991] for the logic A£C, allows to keep only a polynomial fragment (called "trace") of the model in memory, although the total size of the model rriay be expo­ nential. Tracing algorithms usually expand the axioms be­ longing to a single object, only, and make a recursive call for each role successor of this object. This is not feasible in the case of A£C:F(V) since more than a single object may have to be considered when checking concrete domain sat­ isfiability. The central idea to overcome this problem is to expand axioms not for single objects but for "clusters" of ob­ jects which are connected by features . This is done by the feature-complete function. During cluster expansion, chunks of concrete domain axioms are collected. Any such chunk can separately be checked for satisfiability. To see this, it is important to note that roles are not allowed inside the pred­ icate operator, and thus concrete domain axioms cannot in­ volve objects from different clusters (which are connected by roles) . A similar strategy is employed for A£C:F in [Hollun­ der and Nutt, 1990]. The ABox-cons reduces ABox consis­ tency to satisfiability by performing preprocessing on the ini­ tial ABox and then constructing a reduction concept for each role successor of any object in the resulting ABox. In the next section, the complexity of both algorithms is analyzed.

4 Complexity of Reasoning

To characterize space requirements, a formal notion for the size of an ABox is introduced.

Definition 7. The size II q I of a concept C is defined inductively. Let C and D be concepts, A a concept name, R a role or feature, u f 1 · · · f k a feature chain, and let u1 , ... , un also be feature chains.

The size of an axiom a is II Cll if a is of the form x: C and 1 otherwise. The size of an ABox A is the sum of the sizes of all axioms in A.

For the analysis of the space needed by sat, two lemmata are needed.

Lemma 8. For any input A, the function feature-complete constructs an ABox A' with I lA' II :S IIAII 2 + IIAII .

Proof The upper bound for the size of A' is a consequence of the following two points:

1. feature-complete generates no more than IIAII new ax­ ioms.
2. Foreachaxioma,wehavellall :S IIAII.

The second point is obvious, but the first one needs to be proven. The rules Rr:JC and Rr'v'C will not be considered since they are not applied by feature-complete. For all other completion rules, the most important observation is that they can be applied at most once per axiom a : C. This is also true for axioms a : 'v'f.C and the Rf'v'C rule since there is at most one axiom (a, b) :f per feature/ and object a. We make the simplifying assumption that the premise of the Rf'v'C rule does only contain the axiom a : 'v'f.C, i.e., that it is applied to every axiom of this form regardless if there is an axiom (a, b) :for not. This may result in too high an estimation of the number of generated axioms but not in one that is too low. We now prove the first point from above by showing that, for each axiom a in A, no more than llall axioms are generated by feature-complete.

No new axioms are generated for axioms of the form (a, b): R, (a,x) :f, a=/:- b, and (x1, . .. ,xn): P since they do not appear in the premise of any completion rule (please re­ call the simplification we made about Rf'v'C). The remaining axioms are of the form a : C. For these axioms, the property in question can be proved by induction on the structure of C.

For the induction start, let C be :Ju1, ... , Un.P, udu2 , u1 tu2, :JkC, 'v'kC, or a concept name. In any of these cases, it is trivial to verify that at most II Cll new axioms may be gen­ erated. For the induction step, we need to make a case distinc­ tion according to the form of C. Let C be of the form D n E. The application of the Rn rule generates two axioms a : D and a : E. By induction hypothesis, from these two axioms, at most IIDII and II Ell axioms may be generated, respectively. Hence, from a : D n E, at most IIDII +I lEI I +2 = liD nEll new axioms may be generated. The cases for the I;emaining operators DUE, :Jf.C, and 'v'f.C are analogous. Because of the simplifying assumptions made, the 'v'f.C case does not need a special treatment. ·

Lemma 9. For any input A0 , the recursion depth of sat is bounded by I lAo II·

Proof The role depth of a concept Cis the maximum nesting depth of exists and value restrictions in C. The role depth of an ABox A is the maximum role depth of all concepts occurring in A. As an immediate consequence of the way in which the input ABo xes of recursive calls are constructed, we have that the role depth of the arguments ABoxes strictly decreases with recursion depth. ·

The space requirements of sat can now be settled.

Proposition 10. For any input A0 , sat can be executed in space polynomial in I lAo II , provided that this also holds for the function satisfiable?.

Proof We will first analyze the maximum size of the argu­ ments passed to sat in recursive calls. The argument to sat is an ABox which contains axioms a : C for a single object a. It is obvious that there can be at most as many such ax­ ioms per object as there are distinct (sub)concepts appearing in Ao. This number is bounded by IIAoll · Furthermore, the size of any axiom is at most I lAo II · It follows that the max­ imum size of arguments given in a recursive call is IIAoll 2 . Using feature-complete, the argument ABox is extended by new axioms. Combining the argument size with the result from Lemma 8, we find that the maximum size of ABoxes constructed during recursive calls is I lAo 11 4 + I lAo 11 2 . To­ gether with Lemma 9, it follows that sat can be executed in

IIAoll 5 + IIAoll 3 space. ·

This result completes the analysis of the sat algorithm. The A Box-cons algorithm performs some preprocessing on the in­ put ABox and then repeatedly calls sat. Its space require­ ments are investigated in the next Proposition.

Proposition 11. Started on input A, ABox-cons can be ex­ ecuted in space polynomial in JIAJI, provided that this also holds for the function satisfiable?.

Proof It was already proven that sat can be executed in poly­ nomial space if this also holds for satisfiable?. Thus, it re­ mains to be shown that, for an ABox A, the size of A' := preprocess(A) is polynomial in IIAIJ. We will only give a sketch of the proof, for the full version see [Lutz, 1998]. Ob­ jects are called old if they are used in A and new if they are used in A' but not in A. The proof relies on the fact that the preprocess function is identical to the feature-complete func­ tion except that preprocess does also apply the Rr'v'C rule. An upper bound for the number of Rr'v'C applications performed by preprocess can be given as follows: If Rr'v'C is applied to axioms a: 'v'kC and (a, b) : R, then both a and bare old ob­ jects. This is the case since preprocess does not apply Rr:JC, and, hence, no new axioms of the form (a, b): R, where R is a role, are generated. Furthermore, there are at most II All old objects which means that the number of Rr'v'C applications is bounded by JIAIJ 2 . Together with Lemma 8, it can be shown that I lA' II is of order O(IIAIIk). ·

The results just obtained allows us to determine the formal complexity of reasoning with concrete domains.

Theorem 12. Provided that the satis.fiability test of the con­ crete domain V is in PSPACE, the following problems are PSPACE-complete:

1. Consistency of A£C:F(V) ABoxes.
2. Satis.fiability and subsumption of A£C:F(V) concepts.
3. Satis.fiability and subsumption of A£C(V) concepts.
4. Consistency of A£C(V) and A£C:F ABoxes.

If the satis.fiability test of V is in a complexity class X with PSPACE s;:; X, then all of the above problems are PSPACE­ hard.

Proof (1) Since A£C is a proper subset of A£C:F(V) and the satisfiability problem for A£C is PSPACE-complete [Schmidt-SchauB and Smolka, 1991 ], deciding the consis­ tency of A£C:F(V) ABoxes is PSPACE-hard. It remains to be shown that it is in PSPACE if this is also the case for the concrete domain satisfiability test. This follows from Propo­ sition 11 together with the well-known fact that PSPACE = NPSPACE [Savitch, 1970]. (2) is true since satisfiability as well as subsumption can be reduced to ABox consistency, cf. Section 2. (3) and (4) hold since A£C is a proper subset of both logics A£C(V) and A£C:F which are in tum proper sub­ sets of A£C:F(V). ·

Examples of useful concrete domains for which the satisfia­ bility test is in PSPACE are given in [Lutz, 1998].

5 Conclusions and Future Work

We have presented optimal algorithms for deciding the con­ cept satisfiability and the ABox consistency problems for the logic A£C:F(V). In contrast to existing decision procedures, the devised algorithms can be executed in polynomial space provided that this does also hold for the concrete domain sat­ isfiability test. Based on this result, it was proven that reason­ ing with A£C:F(V) is a PSPACE-complete problem. The rule application strategy used by the proposed algorithm is vital for efficient implementations of description logics with con­ crete domains. An interesting new result in this context is that in the case of A£C(V) and A£C:F, satisfiability w.r.t. TBoxes is a NExPTrME-hard problem [Lutz, 1998]. As future work, we will consider the combination of concrete domains with more expressive logics for which reasoning is in PSPACE, see e.g. [Sattler, 1996]. Furthermore, the logic A£C:F(V) seems to be a promising candidate for the reduction of some tempo­ ral description logics in order to obtain complexity results for them.

Acknowledgments I would like to thank Ulrike Sattler and Franz Baader for enlightening discussions and helpful com­ ments. The work in this paper was supported by the "Founda­ tions of Data Warehouse Quality" (DWQ) European ESPRIT IV Long Term Research (LTR) Project 22469.