Matching is the special case of uni cation where one of the expressions to be uni ed has no variables and thus remains unchanged under substitutions. In Description Logic (DL), matching of concept descriptions against concept patterns was originally introduced in [12] as a non-standard inference task that can be used to lter out the unimportant aspects of large concept descriptions appearing in knowledge bases of the system Classic [10]. Subsequently, matching (as well as the more general problem of uni cation) was also proposed as a tool for detecting redundancies in knowledge bases [9] and to support the integration of knowledge bases by prompting interschema assertions to the integrator [11]. All three applications have in common that one wants to search the knowledge base for concepts having a certain (not completely speci ed) form. This \form" can be expressed with the help of so-called concept patterns, i.e., concept descriptions containing variables (which stand for concept descriptions). For example, assume that we want to nd concepts that are concerned with humans that share some characteristic with all their children. This can be expressed by the pattern D := Human u X u 8has-child:X where X is a variable standing for the common characteristic. The concept description C := Human u Tall u 8has-child:Tall matches this pattern in the sense that, if we replace the variable X by the concept description Tall, the pattern becomes equivalent to the concept description C. Thus, the substitution := fX 7! Tallg is a matcher of the matching problem C ? D since C (D). Both matching and uni cation have been investigated in detail for the inexpressive DLs F L0 (with concept constructors top >, conjunction C u D, value restriction 8r:C) and E L (with concept constructors >, C uD, existential restriction 9r:C). Whereas in E L both matching [6] and uni cation [7] are NP-complete problems, the complexity of these problems di ers signi cantly for F L0: matching is polynomial, but uni cation is ExpTime-complete [9]. These results were shown for the case without a background TBox, i.e., a nite set of general concept inclusions (GCIs). For the DL E L it was proved in [8] that the presence of TBoxes does not change the complexity of the matching problem: it stays in NP. For uni cation in E L w.r.t. TBoxes, an NP upper bound could until now only be shown for a restricted form of TBoxes [2].
Matching in F L0 in the presence of TBoxes has not been investigated
until now. In this paper, we close this gap by showing that it is an
ExpTimecomplete problem. Since already subsumption in F L0 w.r.t. TBoxes is
ExpTime-complete [
the matching problem can be lowered from ExpTime to PSpace if one considers TBoxes of a restricted form. Namely, we consider TBoxes containing GCIs where the role depth on the left-hand side of a GCI is not larger than the role depth on the right-hand side. We rst introduce an algorithm for checking subsumption in the presence of such TBoxes. The main idea is the following: C is subsumed by D if D \syntactically" occurs in C, or if there exists an intermediate concept E that subsumes C and we can prove it is subsumed by D in a single step using one GCI. This way, a sequence of GCIs is constructed that proves subsumption between C and D. Even though this sequence may be of exponential length, choosing the intermediate concept in a clever way (which is possible because of the special form of the TBox) ensures that the concept to be checked is always of polynomial size, and hence it is possible to perform the check in PSpace. We then derive the matching algorithm in a similar fashion: again, we are looking for the sequence of GCIs proving subsumption, but at every point we check whether it is possible to extend the substitution in order to shorten the search.