Computing Least Common Subsumers in ALEN

1 Introduction

Computing the least common subsumer (lcs) in description logics (DLs) is an inference task first introduced by Cohen, Borgida, and Hirsh [Cohen et al., 1992] for sublanguages of CLASSIC. Since then it has found several applications: as a key operation in inductive learning algorithms [Cohen and Hirsh, 1994], as a means to measure the similarity of concepts for information retrieval [M¨oller et al., 1998], and as an operation to support the bottom-up construction of DL-knowledge bases [Baader and K¨usters, 1998; Baader et al., 1999]. Roughly speaking, the lcs of a set of concepts is the most specific concept description (among a possibly infinite number of concept descriptions) that subsumes all of the input descriptions, and as such allows to extract the commonalities from given concept descriptions, a task essential for all the mentioned applications.

The first lcs algorithms proposed in the literature were applicable to sublanguages of CLASSIC, more precisely, DLs that in particular allow for number restrictions [Cohen et al., 1992; Cohen and Hirsh, 1994]. More recently, motivated by the bottom-up construction of knowledge bases in a chemical engineering application [Sattler, 1998; von Wedel and Marquardt, 2000], the lcs has been investigated for the DL BTBX [Baader et al., 1999], which allows for existential restrictions instead of number restrictions. Although first empirical results are encouraging [Baader and Molitor, 2000], they also show that this application asks for a more expressive DL, one

A3 This work was carried out while the author was still at the LuFG Theoretical Computer Science, RWTH Aachen.

Ralf Molitor A3

Swiss Life IT Research and Development Group Switzerland ralf.molitor@swisslife.ch

that allows to combine number restrictions and existential restrictions. Such a logic can, for example, be used to describe a reactor with cooling jacket and exactly two inlet valves by Reactor D9 BLis-coupled-to.Cooling-Jacket D9 (=2 has-inlet) D9 BKhas-inlet.Valve.

In this work, we propose an algorithm for computing the lcs of BTBX-concept descriptions. The DL BTBX allows for conjunction, a restricted form of negation, value restrictions, existential restrictions, and number restrictions. Similar to previous approaches [Cohen et al., 1992; Baader and K¨usters, 1998; Baader et al., 1999], our lcs algorithm builds on a structural characterization of subsumption.

Typically, such a characterization works in two steps. First, concept descriptions are turned into a structural normal form, which makes all facts implicitly represented in the description explicit. Second, the subsumer and the subsumee, given in structural normal form, are compared syntactically. A sound and complete characterization then ensures that the structural normal form indeed contains all implied facts.

Now, given that the structural normal form of concept descriptions can be computed effectively, the lcs of concept descriptions can be obtained by first computing their structural normal forms and then extracting the "common facts" present in these normal forms.

For BTBX , however, computing the structural normal form already requires to (inductively) compute the lcs (see our running example in Section 3). Consequently, the proof of correctness of the lcs algorithm needs to be interleaved with the proof of soundness and completeness of the characterization of subsumption, making the proofs quite involved. In [Mantay, 1999], this approach is in fact pursued. However, in an attempt to avoid these interleaving proofs, Mantay made unproved assumptions concerning the existence and other properties of the lcs. Moreover, the lcs algorithm presented there is incorrect in that the computed concept description not necessarily subsumes the input descriptions.

In this work, we devise a more relaxed notion of structural normal form, which does not involve the lcs computation and therefore allows to decouple the characterization of subsumption from the lcs computation. Instead of a single BTBX-concept description, our normal form consists of a set of BTBX-concept descriptions, where some of the implicit facts are not made explicit.

The outline of our paper is as follows: In Section 2, we formally introduce the language BTBX and the lcs operation. Section 3 contains a running example and a discussion of the main difficulties that occur when computing the lcs. In subsequent sections, this example is used to illustrate the notions introduced. Section 4 then covers the characterization of subsumption and Section 5 the lcs algorithm. Finally, in Section 6, we briefly discuss the results obtained. Due to space limitations, we cannot give all technical details. These details as well as complete proofs can be found in [K¨usters and Molitor, 2000].

2 Preliminaries

Concept descriptions are inductively defined with the help of a set of constructors, starting with a set  BV of concept names and a set  CA of role names. In this work, we consider the DL BTBX, i.e., concept descriptions built from the constructors shown in Table 1, subsequently called BTBX -concept descriptions.

The semantics of a concept description is defined in terms of an interpretation
BP B4A1
BN A1
B5. The domain A1
of
is a non-empty set of individuals and the interpretation function A1
maps each concept name  BE  BV to a set 
AI A1
and each role name D6 BE  CA to a binary relation D6
AI A1
A2 A1
. The extension of A1
to arbitrary concept descriptions is inductively defined, as shown in the third column of Table 1.

One of the most important traditional inference services provided by DL systems is computing the subsumption hierarchy. The concept description BV is subsumed by the description BW (BV DA BW) iff BV
AI BW
holds for all interpretations
. The concept descriptions BV and BW are equivalent (BV AH BW) iff they subsume each other.

In this paper, we are interested in the computation of least common subsumers.

Definition 1 Given BTBX-concept descriptions BV BD BN BM BM BM BN BV D2 , D2 AL BE, the BTBX-concept description BV is the least common subsumer (lcs) of BV BD BN BM BM BM BN BV D2 (BV BP D0CRD7B4BV BD BN BM BM BM BN BV D2 B5 for short) iff (i) BV CX DA BV for all BD AK CX AK D2, and (ii) BV is the least concept description with this property, i.e., if BV BC satisfies BV CX DA BV BC for all BD AK CX AK D2, then BV DA BV BC .

Depending on the DL under consideration, the lcs of two or more descriptions need not always exist, but if it exists, then it is unique up to equivalence. The main contribution of this paper is to show that in BTBX the lcs always exists and that it can be computed effectively.

For the sake of simplicity, we consider BTBX-concept descriptions over a set  BV of concept names and assume  CA to be the singleton CUD6CV. However, all definitions and results can easily be generalized to arbitrary sets of role names. Furthermore, w.l.o.g., we assume all BTBX -concept descriptions to be in the following normal form: Each conjunction in an BTBX -concept description contains

1. at most one number restriction of the form B4AL D2 D6B5 (this is w.l.o.g. due to B4AL D1 D6B5 D9 B4AL D2 D6B5 AH B4AL D2 D6B5 if D2 AL D1);
2. at most one number restriction of the form B4AK D2 D6B5 (this is w.l.o.g. due to B4AK D1 D6B5 D9 B4AK D2 D6B5 AH B4AK D2 D6B5 if D2 AK D1);
3. at most one value restriction of the formBKD6BMBV (this is w.l.o.g. due to BKD6BMBV D9 BKD6BMBW AH BKD6BMB4BV D9 BWB5.

3 Running example

In order to highlight the main problems to be solved in the structural characterization of subsumption and the computation of the lcs in BTBX, we will use the following BTBX- concept descriptions:

The key point in the characterization of subsumption and the lcs computation is to describe the "non-trivial" concept descriptions, say BV BC , subsuming a given concept description, say BV, where "non-trivial" means that BV BC does not occur as a conjunct on the top-level of BV. Subsequently, these concept descriptions are called induced. It suffices to only consider induced concept descriptions that are minimal w.r.t. subsumption.

In what follows, we describe the concept descriptions induced by BV CTDC and BW CTDC . It turns out that some of the concept descriptions induced by BV CTDC correspond to the lcs of certain subdescriptions in BV CTDC . As we will see, given the induced concept descriptions of BV CTDC and BW CTDC , it is easy to determine the lcs of BV CTDC and BW CTDC . We start with the concept descriptions induced by BV CTDC .

Number restrictions: Because of the existential restrictions on the top-level of BV CTDC , e.g. BLD6BMB4 D9 BT BD B5 and BLD6BMB4BM D9 BT BD B5, we knowBV CTDC DA B4ALBE D6B5, i.e., B4ALBE D6B5 is induced by BV CTDC . Conversely, there is no induced AK-restriction, i.e., the most specific AK-restriction subsuming BV CTDC is the AK-restriction explicitly present on the top-level of BV CTDC .

Existential restrictions: Due to the AK-restriction B4AKBE D6B5 on the top-level of BV CTDC , each instance of BV CTDC has at most two D6-successors. Consequently, some existential restrictions have to be "merged" to a single existential restriction, where "merging" means conjoining the concept descriptions occurring in the existential restrictions. For BV CTDC , there are several ways to merge the five existential restrictions on the top-level of BV CTDC into two existential restrictions. The merging process gives rise to new (derived) concept descriptions, where the only consistent ones are:

It is clear that BV CTDC AH BV BD CTDC D8 BV BE CTDC . The existential restrictions BLD6BMB4 D9BT BD D9BT BE D9BT BF B5, BLD6BMB4BM D9BT BD D9BT BF B5, BLD6BMB4 D9BT BD D9BT BF B5, and BLD6BMB4BM D9 BT BD D9 BT BF B5 subsume both BV BD CTDC and BV BE CTDC . From this it can be concluded that these restrictions are induced by BV CTDC .

As we will see, the induced existential restrictions can be obtained by picking one existential restriction from each of the (consistent) derived concept descriptions and applying the lcs operation to them. In our example, we have, for instance, D9BT BD D9BT BE D9BT BF AH D0CRD7B4D9 D9BT BD D9BT BE D9BT BF BN D9BM D9BT BD D9 BT BE D9BT BF B5. However, as explained below, our characterization of subsumption avoids to explicitly use the lcs by employing the fact that

Value restrictions: In view of BV CTDC AH BV BD CTDC D8 BV BE CTDC , it not only follows that every instance of BV CTDC has exactly two D6successors but that these D6-successors must satisfy the existential restrictions given in BV BD CTDC and BV BE CTDC . In either case, all D6-successors belong to BT BD D9 BT BF , and thus, the value restriction BKD6BMB4BT BD D9 BT BF B5 is induced by BV CTDC .

There are two things that should be pointed out here: First, note that there is an induced value restriction only if the number of successors induced by existential restrictions coincides with the number in the AK-restriction, because only in this case, we have "full" information about all D6-successors of an instance of BV. For example, if we consider the concept description BX CTDC BMBP B4AK BED6B5 D9 BLD6BMB4BT BD D9 BT BE B5 D9 BLD6BMB4BT BD D9 BT BF B5, no value restriction is induced. 1

Second, if BKD6BMBV BC is the most specific value restriction induced by BV, then BV BC corresponds to the lcs of all concept descriptions occurring in the merged existential restrictions. In

1 The structural subsumption algorithm introduced in [Mantay, 1999], however, computes BKD6BMBT BD as a value restriction induced by BX CTDC and thus, is incorrect. For the same reason, the lcs-algorithm presented in [Mantay, 1999] is incorrect: although the lcs of BX CTDC and BKD6BMBT BD is BQ, the algorithm returns BKD6BMBT BD .

the example, BT BD D9BT BF AH D0CRD7B4D9 D9BT BD D9BT BE D9BT BF BN BMD9BM D9 BT BD D9BT BE D9BT BF BN D9BM D9BT BD D9BT BE D9BT BF BN BMD9 D9BT BD D9BT BE D9BT BF B5. Again, using the equivalence (1), we avoid to explicitly compute the lcs in the characterization of subsumption.

It is easy to see that the only (minimal) concept description induced by BW CTDC is BLD6BMB4BT BD D9 BT BE D9 BT BF B5.

Now, given the concept descriptions induced by BV CTDC and BW CTDC it is not hard to verify that the lcs of BV CTDC and BW CTDC can be stated as

4 Structural characterization of subsumption

In what follows, let BV, BW be BTBX-concept descriptions in the normal form introduced in Section 2. Since both BV AH BR and BW AH BQ trivially imply BV DA BW, our characterization of subsumption explicitly checks these equivalences. Otherwise, roughly speaking, each conjunct in BW, i.e., each (negated) concept name, number restriction, existential restriction, and value restriction occurring on the top-level of BW, is compared with the corresponding conjuncts in BV. For the existential restrictions and value restrictions, however, it will be necessary to resort to the concept descriptions derived from BV by merging existential restrictions (BV BD CTDC and BV BE CTDC in the example). If all the comparisons have succeeded, it follows BV DA BW. In the remainder of this section, the structural comparison between BV and BW is further explained. Finally, Theorem 2 establishes the complete characterization of subsumption.

We first need some notation to access the different parts of the concept descriptions:

• AF D4D6CXD1B4BVB5 denotes the set of all (negated) concept names occurring on the top-level of BV;
• AF D1CXD2 D6 B4BVB5 BMBPD1CPDCCUCZ CY BV DA B4ALCZ D6B5CV;
• AF D1CPDC D6 B4BVB5 BMBPD1CXD2CUCZ CY BV DA B4AKCZ D6B5CV;
• AF if there exists a value restriction of the form BKD6BMBV BC on the top-level of BV, then DACPD0 D6 B4BVB5 BMBP BV BC ; otherwise, DACPD0 D6 B4BVB5 BMBPBQ;
• AF CTDCD6 D6 B4BVB5 BMBP CUBV BC CY there exists BLD6BMBV BC on the top-level of BVCV.

Note that D1CXD2 D6 B4BVB5 is always finite, whereas D1CPDC D6 B4BVB5 may be BD, namely if there exists no positive integer CZ such that BV DA B4AKCZ D6B5. Although these values need not be explicitly present in number restrictions of BV, they can be computed in polynomial time in the size of BV using an oracle for subsumption of BTBX-concept descriptions [K¨usters and Molitor, 2000]. In our example, we get D1CXD2 D6 B4BV CTDC B5 BP BE, D1CPDC D6 B4BV CTDC B5 BP BE, D1CXD2 D6 B4BW CTDC B5 BP BF, and D1CPDC D6 B4BW CTDC B5 BP BD.

The structural comparison between the different parts of BV and BW can now be stated as follows (assuming BV BIAH BR and BW BIAH BQ):

(Negated) concept names and number restrictions: (cf. Theorem 2, 1.-3.) In order for BV DA BW to hold, it is obvious that the following conditions need to be satisfied: D4D6CXD1B4BWB5 AI D4D6CXD1B4BVB5, D1CPDC D6 B4BVB5 AK D1CPDC D6 B4BWB5, D1CXD2 D6 B4BVB5 AL D1CXD2 D6 B4BWB5. Otherwise, it is easy to construct a counter-model for BV DA BW.

Existential restrictions: (cf. Theorem 2, 4.) Given BW BC BE CTDCD6 D6 B4BWB5, then for BV DA BW to hold one at first might expect that there need to exist a BV BC BE CTDCD6 D6 B4BVB5 with DACPD0 D6 B4BVB5 D9 BV BC DA BW BC . Although this works for BTBX-concept descriptions, it fails for BTBX, as BV CTDC DA BLD6BMB4 D9 BT BD D9 BT BE D9 BT BF B5 shows (see Section 3). The reason is that in BTBX AK-restrictions may require to merge existential restrictions, yielding new (implicit) existential restrictions. To deal with this phenomenon, sets of derived concept descriptions are considered with certain existential restrictions merged (see BV BD CTDC and BV BE CTDC in our running example).

The result of merging existential restrictions is described by so-called existential mappings

where D2 BMBP D1CXD2CUD1CPDC D6 B4BVB5BN CYCTDCD6 D6 B4BVB5CYCV and D1 BMBP CYCTDCD6 D6 B4BVB5CY. We require AB to obey the following conditions:

1. ABB4CXB5 BIBP BN for all BD AK CX AK D2;
2. CB BDAKCXAKD2 ABB4CXB5 BP CUBDBN BM BM BM BN D1CV and ABB4CXB5 CK ABB4CYB5 BP BN for all BD AK CX BO CY AK D2.
3. D9 CYBEABB4CXB5 BV CY D9 DACPD0 D6 B4BVB5 BIAH BR for all BD AK CX AK D2.

Although the first two conditions are not essential for soundness and completeness of the characterization of subsumption, they reduce the number of existential mappings that need to be considered.

Given CTDCD6 D6 B4BVB5 BP CUBV BD BN BM BM BM BNBV D1 CV, AB yields an BTBX- concept description BV AB obtained from BV by substituting all existential restrictions on the top-level of BV with

The set of all existential mappings on BV satisfying the conditions B4BDB5-B4BFB5 is denoted by A0 D6 B4BVB5, where A0 D6 B4BVB5 BMBP BN if CTDCD6 D6 B4BVB5 BP BN. It is in fact sufficient to consider A0 D6 B4BVB5 modulo permutations, i.e., modulo the equivalence

In the sequel, for the sake of simplicity, we stay with AB BE A0 D6 B4BVB5 instead of CJABCL AO BP BE A0 D6 B4BVB5BP AO BP , though.

In our running example, let CTDCD6 D6 B4BV CTDC B5 BP CUBV CTDC BNBD BN BM BM BM BN BV CTDC BNBH CV with BV CTDC BNBD BP  D9 BT BD , BV CTDC BNBE BP  D9 BT BE , etc. Then, A0 D6 B4BV CTDC B5 consists of the two mappings

and it is BV AB CX CTDC BP BV CX CTDC , CX BP BDBN BE (see Section 3).

For the characterization of subsumption, we will use the following notation:

Now, in case CTDCD6 D6 B4BVB5 BIBP BN, BV DA BW implies that for each BW BC BE CTDCD6 D6 B4BWB5 the following holds: for each AB BE A0 D6 B4BVB5, there exists BV BC AB BE CTDCD6 D6 B4BVB5 AB such that BV BC AB D9 DACPD0 D6 B4BVB5 DA BW BC . This is what is stated in Theorem 2, 4. Note that, using the equivalence (1), and provided that the lcs of BTBX-concept descriptions always exists, this condition could be rewritten as: there exists a set  BMBP CUBV BC AB BE CTDCD6 D6 B4BVB5 AB CY AB BE A0 D6 B4BVB5CV with D0CRD7B4CUBV BC D9 DACPD0 D6 B4BVB5 CY BV BC BE CVB5 DA BW BC . However, since the existence of the lcs is not guaranteed a priori, the lcs cannot be used in the structural characterization of subsumption, unless the characterization and the lcs computation are interleaved.

If CTDCD6 D6 B4BVB5 BP BN, then for all BW BC BE CTDCD6 D6 B4BWB5 it must hold, D1CXD2 D6 B4BVB5 AL BD and DACPD0 D6 B4BVB5 DA BW BC .

In our running example, BV CTDC DA BLD6BMB4 D9 BT BD D9 BT BE D9 BT BF B5 illustrates the case where CTDCD6 D6 B4BVB5 BIBP BN and BW CTDC DA BLD6BMB4BT BD D9 BT BE D9 BT BF B5 illustrates CTDCD6 D6 B4BVB5 BP BN.

Value restrictions: (cf. Theorem 2, 5.) Value restrictions can only be induced for two reasons. First, if D1CPDC D6 B4BVB5 BP BC, then BV DA BKD6BMBR, and thus, BV DA BKD6BMBV BC for all concept descriptions BV BC .

Second, the merging of existential restrictions may induce value restrictions. In contrast to induced existential restrictions, however, one further needs to take care of ALrestrictions induced by "incompatible" existential restrictions:

If CTDCD6 D6 B4BVB5 BP BN, we define AK D6 B4BVB5 BMBP BC. In our example, AK D6 B4BV CTDC B5 BP BE, AK D6 B4BW CTDC B5 BP BC, and AK D6 B4BX CTDC B5 BP BD.

Now, only if AK D6 B4BVB5 BP D1CPDC D6 B4BVB5, value restrictions can be induced, since only then we "know" all the D6-successors of instances of BV. In our example, AK D6 B4BV CTDC B5 BP D1CPDC D6 B4BV CTDC B5 BP BE, which accounts for BV CTDC DA BKD6BMB4BT BD D9 BT BF B5. Conversely, BX CTDC BIDA BKD6BMBT BD since BD BP AK D6 B4BX CTDC B5 BO D1CPDC D6 B4BX CTDC B5 BP BE.

To formally state the comparison between value restrictions of BV and BW, we use the following notation:

One can show that BV DA BW implies DACPD0 D6 B4BVB5 DA DACPD0 D6 B4BWB5 provided that AK D6 B4BVB5 BO D1CPDC D6 B4BVB5. In case BC BO AKB4BVB5 BP D1CPDC D6 B4BVB5, however, it suffices if the value restriction of BW satisfies DACPD0 D6 B4BVB5 D9 BV BC DA DACPD0 D6 B4BWB5 for all BV BC BE CTDCD6 D6 B4BVB5 A3 . Again, using the equivalence (1), and provided that the lcs of BTBX-concept descriptions always exists, this condition can be restated as DACPD0 D6 B4BVB5 D9 D0CRD7B4CTDCD6 D6 B4BVB5 A3 B5 DA BW BC . For reasons already mentioned, we have not employed this variant.

We are now ready to state the structural characterization of subsumption in BTBX .

Theorem 2 [K¨usters and Molitor, 2000] Let BVBNBW be two BTBX-concept descriptions with CTDCD6 D6 B4BVB5 BP CUBV BD BN BM BM BM BN BV D1 CV. Then BV DA BW iff BV AH BR, BW AH BQ, or the following holds:

1. D4D6CXD1B4BWB5 AI D4D6CXD1B4BVB5;
2. D1CPDC D6 B4BVB5 AKD1CPDC D6 B4BWB5;
3. D1CXD2 D6 B4BVB5 AL D1CXD2 D6 B4BWB5;
4. for all BW BC BE CTDCD6 D6 B4BWB5 it holds that
5. (a) CTDCD6 D6 B4BVB5 BP BN, D1CXD2 D6 B4BVB5 AL BD, and DACPD0 D6 B4BVB5 DA BW BC ; or
6. (b) CTDCD6 D6 B4BVB5 BIBP BN and for each AB BE A0 D6 B4BVB5, there exists BV BC BE CTDCD6 D6 B4BVB5 AB such that BV BC D9 DACPD0 D6 B4BVB5 DA BW BC ; and

• Let BVBN BW be two BTBX -concept descriptions. If BV DABW, then c-lcsB4BVBNBWB5 BMBPBW, and if BW DA BV, then c-lcsB4BVBNBWB5 BMBP BV. Otherwise, let A0 D6 B4BVB5 BP CUAB BV BD BN BM BM BM BN AB BV D2B4BVB5 CV and A0 D6 B4BWB5 BP CUAB BW BD BN BM BM BM BN AB BW D2B4BWB5 CV, and define for BX BE CUBVBN BWCV BV D6 B4BXB5 BMBP BK BO BM CUc-lcsB4CUBX BD D9 DACPD0 D6 B4BXB5BN BM BM BM BN BX D2B4BXB5 D9 DACPD0 D6 B4BXB5CVB5 CY BX CX BE CTDCD6 D6 B4BXB5 AB BX CX BN BD AK CX AK D2B4BXB5CVBN A0 D6 B4BXB5 BIBP BNBN CUDACPD0 D6 B4BXB5CVBN A0 D6 B4BXB5 BP BN CM D1CXD2 D6 B4BXB5 AL BDBN BNBN D1CXD2 D6 B4BXB5 BP BCBN BX A3 D6 BMBP B4 DACPD0 D6 B4BXB5BN BC AK AK D6 B4BXB5 BO D1CPDC D6 B4BXB5BN BRBN D1CPDC D6 B4BXB5 BP BCBN c-lcsB4CUDACPD0 D6 B4BXB5 D9BX BC CY BX BC BE CTDCD6 D6 B4BXB5 A3 CVB5BN BC BO AK D6 B4BXB5 BP D1CPDC D6 B4BXB5BM Define c-lcsB4BVBNBWB5 BMBP D9 BED4D6CXD1B4BVB5CKD4D6CXD1B4BWB5 D9 B4AK D1CPDCCUD1CPDC D6 B4BVB5BN D1CPDC D6 B4BWB5CV D6B5 D9 B4AL D1CXD2CUD1CXD2 D6 B4BVB5BN D1CXD2 D6 B4BWB5CV D6B5 D9 D9 BV BC BEBV D6 B4BVB5BNBW BC BEBV D6 B4BWB5 BLD6BMc-lcsB4BV BC BNBW BC B5 D9 BKD6BMc-lcsB4BV A3 D6 BN BW A3 D6 B5BN where AF B4AKD1CPDCCUD1CPDC D6 B4BVB5BND1CPDC D6 B4BWB5CV D6B5 is omitted if D1CPDC D6 B4BVB5 BPBDor D1CPDC D6 B4BWB5 BPBD, and AF D9 BV BC BEBV D6 B4BVB5BNBW BC BEBV D6 B4BWB5 BLD6BMc-lcsB4BV BC BN BW BC B5 BMBP BQ if BV D6 B4BVB5 BP BN or BV D6 B4BWB5 BP BN.

Figure 1: The recursive computation of the lcs in BTBX.

In the remainder of this section, we illustrate the definition of c-lcsB4BVBNBWB5 in case that BV BIDA BW and BW BIDA BV (since the special cases BV DA BW, BW DA BV are trivial), using our running example introduced in Section 3. The conjuncts occurring on the top-level of c-lcsB4BVBNBWB5 can, as before, be divided into three parts, namely (1) (negated) concept names and number restrictions, (2) the existential restrictions, and (3) the value restriction. These conjuncts are defined in such a way that

• (a) the conditions 1.-5. in Theorem 2 for BV DA c-lcsB4BVBNBWB5 and BW DA c-lcsB4BVBN BWB5 are satisfied, and
• (b) c-lcsB4BVBNBWB5 is the least concept description (w.r.t. DA) satisfying (a).

For the conditions 1.-3., this is quite obvious, since, for BX BE CUBVBN BWCV, we obtain

• AF D4D6CXD1B4c-lcsB4BVBN BWB5B5 BP D4D6CXD1B4BVB5 CK D4D6CXD1B4BWB5 AI D4D6CXD1B4BXB5,
• AF D1CXD2 D6 B4c-lcsB4BVBNBWB5B5 BP D1CXD2CUD1CXD2 D6 B4BVB5BND1CXD2 D6 B4BWB5CV AK D1CXD2 D6 B4BXB5, and

In our running example, D4D6CXD1B4c-lcsB4BV CTDC BNBW CTDC B5B5 BP BN, D1CXD2 D6 B4c-lcsB4BV CTDC BNBW CTDC B5B5 BP BE, and D1CPDC D6 B4c-lcsB4BV CTDC BNBW CTDC B5B5 BP BD.

For existential and value restrictions things are more complicated. Let us first consider the definition of CTDCD6 D6 B4c-lcsB4BVBNBWB5B5, i.e., the existential restrictions obtained from the sets BV D6 B4BVB5 and BV D6 B4BWB5. Roughly speaking, if A0 D6 B4BXB5 BIBP BN, then BV D6 B4BXB5 contains all (minimal) concept descriptions occurring in an existential restriction induced by BX for BX BE CUBVBNBWCV. Each such concept description is obtained

1. if DACPD0 D6 B4BWB5 BIAH BQ, then
2. (a) D1CPDC D6 B4BVB5 BP BC; or
3. (b) AK D6 B4BVB5 BO D1CPDC D6 B4BVB5 and DACPD0 D6 B4BVB5 DA DACPD0 D6 B4BWB5; or
4. (c) BC BO AK D6 B4BVB5 BP D1CPDC D6 B4BVB5 and DACPD0 D6 B4BVB5 D9 BV BC DA DACPD0 D6 B4BWB5 for all BV BC BE CTDCD6 D6 B4BVB5 A3 .

As known from the literature, [Hemaspaandra, 1999], testing subsumption of BTBX-concept descriptions is PSPACEcomplete. However, our characterization is not intended to serve as a basis for a polynomial-space subsumption algorithm. It rather yields the formal basis for the lcs algorithm presented in the next section.

5 Computing the lcs in BTBX

The recursive algorithm computing the lcs of two BTBX- concept descriptions BV and BW is depicted in Figure 1. For a set BV of BTBX-concept descriptions, c-lcsB4BVB5 is computed by iteratively applying the binary c-lcsoperation, i.e., c-lcsB4CUBV BD BN BM BM BM BNBV D2 CVB5 BMBP c-lcsB4BV BD BN c-lcsB4BV BE BN A1 A1 A1 BN c-lcsB4BV D2A0BD BN BV D2 B5 A1 A1 A1B5B5 for D2 BQ BE.

Since the role depth of BV and BW is finite, the recursive computation of c-lcsB4BVBNBWB5 always terminates. The following theorem states correctness of the lcs algorithm depicted in Figure 1. As an immediate consequence, we obtain that the lcs of two BTBX -concept descriptions always exists. The theorem is proved by induction on the role depth of c-lcsB4BVBN BWB5 and makes heavy use of the structural characterization of subsumption given in Theorem 2.

Theorem 3 [K¨usters and Molitor, 2000] Let BVBN BW be BTBX- concept descriptions. Then, c-lcsB4BVBNBWB5 AH D0CRD7B4BVBNBWB5.

as the recursively computed lcs of a set of concept descriptions consisting of one concept description from CTDCD6 D6 B4BXB5 AB (conjoined with DACPD0 D6 B4BXB5) for each AB BE A0 D6 B4BXB5. In our running example, each pair of concept descriptions occurring in the existential restrictions on the top-level of BV BD CTDC and BV BE CTDC , respectively, yields such an lcs, and thus BV D6 B4BV CTDC B5 BP CUD9BT BD D9BT BE D9BT BF BN D9BT BD D9BT BF BN BM D9BT BD D9BT BF BN BMD9BT BD D9BT BF CV (see Section 3).

If D1CXD2 D6 B4BXB5 BP BD and A0 D6 B4BXB5 BP BN, we set BV D6 B4BXB5 BP CUDACPD0 D6 B4BXB5CV since then CTDCD6 D6 B4BXB5 BP BN, and BLD6BMDACPD0 D6 B4BXB5 is the unique minimal existential restriction induced by BX. This case is illustrated by BW CTDC in our running example, where D1CXD2 D6 B4BW CTDC B5 BP BF, CTDCD6 D6 B4BW CTDC B5 BP BN, and BV D6 B4BW CTDC B5 BP CUBT BD D9 BT BE D9 BT BF CV.

Finally, if D1CXD2 D6 B4BXB5 BP BC, i.e., there exists no existential restriction subsuming BX, then obviously, no existential restriction can occur on the top-level of a common subsumer of BV and BW. Therefore, we set BV D6 B4BXB5 BMBP BN.

Given BV D6 B4BVB5 and BV D6 B4BWB5, the lcs of each pair BV BC BE BV D6 B4BVB5 and BW BC BE BV D6 B4BWB5 gives rise to an existential restriction on the top-level of the lcs of BV and BW. In our example, we obtain CTDCD6 D6 B4c-lcsB4BV CTDC BNBW CTDC B5B5 BP CUBT BD D9 BT BE D9 BT BF BNBT BD D9 BT BF CV, giving rise to the existential restrictions BLD6BMB4BT BD D9 BT BE D9 BT BF B5 and BLD6BMB4BT BD D9 BT BF B5 (where the latter one can be omitted).

It remains to comment on BKD6BMc-lcsB4BV A3 D6 BN BW A3 D6 B5. Intuitively, BKD6BMBX A3 D6 is the most specific value restriction subsuming BX for BX BE CUBVBNBWCV. (Thus, BKD6BMc-lcsB4BV A3 D6 BN BW A3 D6 B5 is the most specific value restriction subsuming both BV and BW.) If BX has no induced value restriction, BX A3 D6 coincides with DACPD0 D6 B4BXB5. This is the case for BW CTDC , where B4BW CTDC B5 A3 D6 BP DACPD0 D6 B4BW CTDC B5 BP BT BD D9BT BE D9BT BF . If D1CPDC D6 B4BXB5 BP BC, the fact that BX DA BKD6BMBR is made explicit by defining BX A3 D6 BMBP BR. Finally, if BC BO AK D6 B4BXB5 BP D1CPDC D6 B4BXB5, then the induced value restriction is again made explicit by recursively computing the lcs of the merged existential restrictions (each conjoined with DACPD0 D6 B4BXB5). In our running example, this case is illustrated by BV CTDC : there, DACPD0 D6 B4BV CTDC B5 BP BQ, but since AK D6 B4BV CTDC B5 BP D1CPDC D6 B4BV CTDC B5 BP BE, we obtain B4BV CTDC B5 A3 D6 BP BT BD D9 BT BF which is the recursively computed lcs of CTDCD6 D6 B4BV CTDC B5 A3 BP CTDCD6 D6 B4BV BD CTDC B5 CJ CTDCD6 D6 B4BV BE CTDC B5 (see Section 3).

6 Conclusion and future work

We have presented an algorithm for computing the lcs in BTBX . Its proof of correctness is based on the structural characterization of subsumption introduced in Section 4. In this characterization, we avoided to explicitly use the lcs in order to be able to decouple the characterization of subsumption and the lcs computation. Interleaving these two tasks caused previous work on the lcs in BTBX to be incorrect.

Due to the interaction between number restrictions and existential restrictions the characterization of subsumption and the lcs computation became much more involved than for the sublanguages BTBX [Baader et al., 1999] and BT [Cohen and Hirsh, 1994; Baader and K¨usters, 1998]. As an immediate consequence of results shown in [Baader et al., 1999] for BTBX, we obtain an exponential lower bound for the size of the lcs of two BTBX-concept descriptions. It is, however, not known whether this bound is tight. The lcs algorithm presented in Section 5 takes double exponential time [K¨usters and Molitor, 2000]. Nevertheless, since a prototype implementation of the exponential-time lcs algorithm for BTBX behaves quite well in the chemical process engineering application [Baader and Molitor, 2000], the hope is that the lcs algorithm for BTBX proposed here will also work in realistic application situations. For evaluation, continuing the work on BTBX, a prototype of the algorithm for BTBXwill be implemented using the DL-system FaCT [Horrocks, 1998] for deciding subsumption in BTBX, which then is to be applied to the chemical engineering knowledge base.