Matching under Side Conditions in Description Logics

1 Introduction

The traditional inference problems (like subsumption) in description logics (DLs) are now well-investigated, which means that there exist complexity results and algorithms for a great variety of DLs of differing expressive power [Donini et al., 1996] as well as optimized implementations of the algorithms for expressive DLs [Horrocks, 1998]. In contrast, matching concepts against patterns is a relatively new inference problem in DLs, which has originally been introduced in [Borgida and McGuinness, 1996; McGuinness, 1996] to help filter out the unimportant aspects of large concepts appearing in knowledge bases of the CLASSIC system [Brachmann et al., 1991]. More recently, matching (as well as the more general problem of unification) has been proposed as a tool for detecting redundancies in knowledge bases [Baader and Narendran, 1998] and to support the integration of knowledge bases by prompting possible interschema assertions [Borgida and K¨ usters, 2000].

All three applications have in common that one wants to search a large knowledge base for concepts having a certain (not completely specified) form. This "form" can be expressed with the help of so-called concept patterns, i.e., concept descriptions containing variables. For example, the pattern D := X ⊓ ∀child.(Y ⊓ Female) looks for concepts that restrict the child role to fillers that are Female, such as the concept C := (≥1 child) ⊓ ∀child.(Female ⊓ Rich). In fact, applying the substitution σ := {X ↦→ (≥1 child), Y ↦→

∗This work has been partially supported by the Deutsche Forschungsgemeinschaft, DFG Project BA 1122/4-1.

Rich} to the pattern D yields a concept equivalent to C, i.e., σ is a solution (matcher) of the matching problem C ≡? D.

This type of matching problems has been investigated in detail for sublanguages of the DLs ALN and ALE in [Baader et al., 1999] and [Baader and K¨ usters, 2000], respectively. In particular, it was shown that, for sublanguages of ALN, solvable matching problems always have a least matcher (w.r.t. subsumption), which can be computed in polynomial time. For sublanguages of ALE, deciding solvability of matching problems modulo equivalence is already NP-complete.

In [Borgida and McGuinness, 1996; McGuinness, 1996], the expressivity of matching problems was further enhanced by allowing for additional side conditions on the variables (through the as-construct): a (strict) subsumption condition is of the form X ⊑? E (X ⊏? E) where X is a variable and E a pattern, and it restricts the matchers to substitutions satisfying σ(X) ⊑ σ(E) (σ(X) ⊏ σ(E)). Using a subsumption condition, the matching problem of the above example can be written more intuitively as X ⊓ ∀child.Z ≡? (≥1child) ⊓ ∀child.(Female ⊓ Rich) under the subsumption condition Z ⊑? Female. One result of this paper is that also more complex sets of subsumption conditions do not extend the expressive power of matching problems (see below). However, they are often more convenient to state. In contrast, strict subsumption conditions cannot always be simulated by pure matching problems. They can, e.g., be used to avoid trivial matches. For example, the pattern D′ := X ⊓ ∀child.Y matches every concept since ∀child.⊤ ≡ ⊤ (where the top concept ⊤ stands for the set of all individuals). The additional strict subsumption condition Y ⊏? ⊤ ensures that we can only match concepts with a real restriction on child.

The first (rather restricted) formal results on matching under side conditions were given in [Baader et al., 1999]: it was shown that matching under strict subsumption conditions in the small DL FL0 is already NP-hard, and that matching under so-called acyclic subsumption conditions can be reduced to matching without side conditions. However, [Baader et al., 1999] does not give a complexity upper bound for matching under strict subsumption conditions and the reduction for acyclic subsumption conditions given there is exponential.

This paper investigates in detail matching under side conditions in sublanguages of ALN. We will show that matching under subsumption conditions can be reduced in polynomial time to matching without side conditions. In particular, this implies that solvable matching problems under subsumption conditions in sublanguages of ALN always have a least matcher, which can be computed in polynomial time. For acyclic strict subsumption conditions, matching is shown to be NP-complete in the sublanguages FL⊥ and FL¬ of ALN .

2 Description logics

Concept descriptions are inductively defined with the help of a set of concept constructors, starting with a set NC of concept names and a set NR of role names. In this paper, we consider concept descriptions built from the constructors shown in Table 1. In the description logic FL0, concept descriptions are formed using the constructors top-concept (⊤), conjunction (C ⊓ D), and value restriction (∀r.C). The description logic FL⊥ additionally provides us with the bottom concept (⊥), and FL¬ also allows for primitive negation (¬P). Finally, ALN extends FL¬ with number restrictions (≥ n r) and (≤ n r) (see Table 1).

As usual, the semantics of concept descriptions is defined in terms of an interpretation I = (∆I , ·I ). The domain ∆I of I is a non-empty set and the interpretation function ·I maps each concept name P ∈ NC to a set P I ⊆ ∆I and each role name r ∈ NR to a binary relation rI ⊆ ∆I ×∆I . The extension of ·I to arbitrary concept descriptions is defined inductively, as shown in the second column of Table 1.

One of the most important traditional inference services provided by DL systems is computing the subsumption hierarchy. The concept description C is subsumed by the description D (C ⊑ D) iff CI ⊆ DI holds for all interpretations I; C and D are equivalent (C ≡ D) iff they subsume each other; C is strictly subsumed by D (C ⊏ D) iff C ⊑ D and C ̸≡ D. For all DLs listed in Table 1, subsumption can be decided in polynomial time using a structural subsumption algorithm [Borgida and Patel-Schneider, 1994].

Matching in description logics

In order to define concept patterns, we additionally need a set NX of concept variables, which we assume to be disjoint from NC ∪ NR. Informally, an ALN-concept pattern is an ALN-concept description over the concept names NC ∪NX and the role names NR, with the only exception that primitive negation must not be applied to variables. More formally, concept patterns (denoted D,D′ ) are defined using the following syntax rules:

where X ∈ NX, r ∈ NR, and C is an ALN-concept description. For example, if X, Y are concept variables, r a role name, and A, B concept names, then D := A ⊓ X ⊓ ∀r.(B ⊓ Y ) is an ALN-concept pattern, but ¬X is not. The notion of a pattern (and also the notions "substitution" and "matching problem" introduced below) can be restricted to sublanguages of ALN in the obvious way.

A substitution σ is a mapping from NX into the set of all ALN-concept descriptions. This mapping is extended to concept patterns in the usual way by replacing the occurrences of the variables X in the pattern by the corresponding concept description σ(X). For example, if we apply the substitution σ := {X ↦→ A ⊓ B, Y ↦→ A} to the pattern D from above, we obtain the description σ(D) = A ⊓ A ⊓ B ⊓ ∀r.(B ⊓ A). The result of applying a substitution to an ALN-concept pattern is always an ALN-concept description. Note that this would no longer be the case if negation were allowed in front of concept variables.

Subsumption can be extended to substitutions as follows: the substitution σ is subsumed by the substitution τ (σ ⊑ τ) iff σ(X) ⊑ τ(X) for all variables X ∈ NX.

Definition 1 Let C be an ALN-concept description and D an ALN-concept pattern. Then, C ≡? D is an ALNmatching problem. The substitution σ is a solution (matcher) of C ≡? D iff C ≡ σ(D).

In the following, we will abbreviate a matching problem of the form C ≡? C ⊓ D as C ⊑? D. This notation is justified by the fact that σ solves C ≡? C ⊓ D iff C ⊑ σ(D).

A matching problem can either be viewed as a decision problem, where one asks whether the problem is solvable, or as a computation problem, where one asks for actual matchers of this problem (if any). Although the computation problem is usually the more interesting one, the decision problem can serve as a starting point for the complexity analysis. In general, matching problems may have several (even an infinite number of) solutions, and thus the question arises which matcher to compute. Following [Borgida and McGuinness, 1996; Baader et al., 1999] we will here concentrate on the problem of computing a least matcher (w.r.t. the ordering ⊑ on substitutions).

Instead of a single matching problem, we may also consider finite systems {C1 ≡? D1, . . . ,Cm ≡? Dm} of such problems, which must be solved simultaneously. As shown in [Baader et al., 1999], solving such a system can, however, be reduced to solving the single matching problem

where the ri are pairwise distinct role names.

The following theorem summarizes the results obtained in [Baader and Narendran, 1998; Baader et al., 1999] for matching in (sublanguages of) ALN:

Theorem 2 Let L ∈ {FL0,FL⊥,FL¬,ALN}. Then there exists a polynomial time matching algorithm that computes the least matcher of a given system of L-matching problems, if this system has a solution, and returns "fail" otherwise.

Obviously, this implies that the existence of a solution can be decided in polynomial time. In the sequel, let MATCHL denote an algorithm according to Theorem 2.

Matching under side conditions

In this paper, we focus on more general matching problems, those that allow for additional side conditions.

Definition 3 A subsumption condition is of the formX ⊑? E where X is a concept variable and E is a pattern; a strict subsumption condition is of the form X ⊏ E where X and E are as above. A side condition is either a subsumption condition or a strict subsumption condition. The substitution σ satisfies the side condition X ρ E for ρ ∈ {⊑, ⊏} iff σ(X) ρ σ(E).

A matching problem under side conditions is a tuple M := 〈C ≡? D, S〉, where C ≡? D is a matching problem and S

is a finite set of side conditions. If the set S contains only subsumption conditions, then M is called matching problem under subsumption conditions. The substitution σ is a solution (matcher) of M iff it is a matcher of C ≡? D that satisfies every side condition in S.

In the next section, we will restrict the attention to matching problems under subsumption conditions. Section 4 then treats matching problems under acyclic side conditions.

In order to define matching problems under acyclic side conditions, we say that a variable X directly depends on a variable Y in S iff S contains a side condition X ρ E such that Y occurs in E. If there are n ≥ 1 variables X1, . . . ,Xn such that Xi directly depends on Xi+1 in S (1 ≤ i ≤ n - 1), then we say that X1 depends on Xn in S. The set of side conditions S is cyclic iff there is a variable X that depends on itself in S; otherwise, S is acyclic.

3 Matching under subsumption conditions

Let L be one of the DLs FL⊥,FL¬,ALN. We present a polynomial time algorithm that, given an L-matching problems under subsumption conditions, returns a least matcher (w.r.t. the ordering ⊑ on substitutions) if the problem is solvable, and "fail" otherwise. In principle, the algorithm iterates the application of MATCHL until a fixpoint is reached. However, the matcher computed in one step is used to modify the matching problem to be solved in the next step. Given an L-matching problem under subsumption conditions M := 〈C ≡? D, S〉 and a substitution σ, we define

Recall that σ(X) ⊑? E abbreviates the matching problem σ(X) ≡? σ(X) ⊓ E. Thus Mσ is a system of L-matching problems without side conditions, to which MATCHL can be applied.

Algorithm 4 Let M := 〈C ≡? D, S〉 be an L-matching problem under subsumption conditions. Then, the algorithm MATCH⊑L (M) works as follows:

1. σ(X) := ⊥ for all variables X;
2. If MATCHL(Mσ) returns "fail", then return "fail"; else if σ ≡ MATCHL(Mσ), then return σ; else σ := MATCHL(Mσ); continue with 2.

Let σ0 denote the substitution defined in step 1 of the algorithm, and σt (t ≥ 1) the matcher computed in the t-th iteration of Step 2. Note that σt is undefined if MATCHL returns

"fail" in the t-th iteration or if the algorithm has stopped before the t-th iteration.

To show that the algorithm is correct, we must show soundness, completeness, and termination, i.e., i) if the algorithm terminates and returns a substitution, then this substitution in fact solves the problem; ii) if the algorithm terminates and returns "fail", then there indeed is no solution; and iii) the algorithm halts on every input. The following lemma proves soundness and completeness of the algorithm. The first two items establish a loop invariant.

Lemma 5 Let M := 〈C ≡? D, S〉 be an L-matching problem under subsumption conditions.

1. If σt is defined and τ is a solution of M, then σt ⊑ τ.
2. If σt, σt+1 are defined, then σt ⊑ σt+1.
3. If MATCH⊑L (M) returns the substitution σ, then σ solves M (soundness).
4. If MATCH⊑L (M) returns "fail", then M has no solution (completeness).
5. PROOF. 1. Obviously, the claim is true for σ0. Assume that σt ⊑ τ, and that σt+1 is defined. To prove σt+1 ⊑ τ, it is sufficient to show that τ solvesMσt since σt+1 is the least solution of Mσt . Since τ solves M, we know that it solves C ≡? D and that τ(X) ⊑ τ(E) for all X ⊑? E ∈ S. The induction assumption σt ⊑ τ implies σt(X) ⊑ τ(X), and thus σt(X) ⊑ τ(E), which shows that τ solves Mσt .
6. Obviously, σ0 ⊑ σ1. Now assume that σt-1 ⊑ σt. Together with the fact that σt solves Mσt-1 , this implies that σt+1 solves the systemMσt-1 . Since σt is the least solution of Mσt-1 , we can conclude σt ⊑ σt+1.
7. Assume that σ = σt. By definition of MATCH⊑L , C ≡ σt(D). It remains to show that σt solves the side conditions. We know that σt ≡ σt+1 and σt+1 solves Mσt . Thus, σt(X) ⊑ σt+1(E) ≡ σt(E) for every X ⊑? E ∈ S.
8. Assume that MATCH⊑L (M) returns "fail," and that σt is the last substitution computed by the algorithm. Now assume that τ solves M. As in the proof of 1. we can show that τ solves Mσt . Consequently, Mσt is solvable, and thus MATCH(Mσt ) returns the least matcher of this system, in contradiction to the assumption that MATCH⊑L (M) returns "fail" in this step of the iteration.

Proving termination of Algorithm 4 is more involved, and the exact argument depends on the DL L under consideration. Due to the space limitations, in this paper we sketch the proof for the DL FL⊥ (see [Baader et al., 2000] for complete proofs). The proof depends on the so-called reduced normal form of FL⊥-concept descriptions, to be introduced next.

It is easy to see that any FL⊥-concept description can be transformed into an equivalent description that is either ⊤ or a (nonempty) conjunction of descriptions of the form ∀r1. · · · ∀rm.A, where r1, . . . , rm are m ≥ 0 (not necessarily distinct) roles, and A is the bottom concept ⊥ or a concept name. We abbreviate ∀r1. · · · ∀rm.A by ∀r1 . . . rm.A, where r1 . . . rm is viewed as a word over the alphabet NR of all role names. If m = 0, then this is the empty word ε, and thus ∀ε.A is our "abbreviation" for A. In addition, instead of ∀w1.A ⊓ . . . ⊓ ∀wℓ.A we write ∀L.A where L := {w1, . . . , wℓ} is a finite set of words over NR; we define ∀∅.A ≡ ⊤. Using these abbreviations, any FL⊥-concept description C containing only concept names in the finite set C ⊆ NC can be written as

where UH for H ∈ C ∪ {⊥} are finite sets of words over NR (called role languages). This representation of C will subsequently be called its U-labeled normal form.

As an example, consider the FL⊥-concept description Cex := ∀r.(⊥ ⊓ ∀r.⊥) ⊓ ∀r.∀s.A ⊓ ∀s.A. Its FL0-normal form C′ex is ∀{r, rr}.⊥ ⊓ ∀{rs, s}.A.

The role languages may contain redundant words, i.e., words that, when removed, yield equivalent concept descriptions: i) since ∀w.⊥ ⊑ ∀wv.⊥ for every w, v ∈ N ∗R, we can require U⊥ to be prefix-free, i.e., w,wv ∈ U⊥ implies v = ε; and ii) since ∀w.⊥ ⊑ ∀wv.A, we can require UA ∩ (U⊥ · N ∗R) = ∅. A normal form satisfying these conditions is called reduced normal form.

Obviously, any FL⊥-concept description can be turned into such a reduced normal form (in polynomial time). In our example, the reduced normal form of Cex is ∀{r}.⊥ ⊓ ∀{s}.A, which is obtained from C′ex by removing rr from U⊥ = {r, rr} and rs from UA = {rs, s}. Reduced normal forms can be used to characterize equivalence of FL⊥- concept descriptions:

Lemma 6 Assume that the FL⊥-concept descriptions C,D are given in their U- and V -labeled reduced normal forms, respectively. Then C ≡ D iff UH = VH for all H ∈ C ∪{⊥}.

Termination of Algorithm 4 for L = FL⊥ L = FL⊥ L = FL⊥

Let the substitutions σt be defined as above. We assume that every σt(X) is given in U t,X -labeled reduced normal form, and that C (as defined in Algorithm 4) is in U-labeled reduced normal form. Then, termination follows from the fact that every solvable matching problem under subsumption conditions has a matcher that only uses concept names already contained in the matching problemM, denoted by the set C ⊆ NC, and the following three properties of the languages U t,X H and UH for H ∈ C ∪ {⊥}. In the formulation of these properties we implicitly assume that the substitution σt is defined whenever we talk about one of the languages U t,X H .

1. For every variable X and every H ∈ C ∪ {⊥}, the set U t,X H contains only suffixes of UH.
2. For every word w, if w ∈ U t,X H \ U t+1,X H , then w ̸∈ U t′ ,X H for any t′ > t.
3. If σt and σt+1 are defined and σt ̸≡ σt+1, then there exists an H ∈ C ∪{⊥}, a variable X, and a word w such that w ∈ U t,X H \ U t+1,X H .

A complete proof of these properties can be found in [Baader et al., 2000]. It also depends on details of the algorithm MATCHL, which we have here introduced only as a black box. Note that these properties would not hold if we did not use reduced normal forms.

Given these properties, it is now easy to show that the algorithm halts after a polynomial number of steps. In fact, Property 1 yields a polynomial upper bound on the size of the role languages U t,X H . Property 3 shows that in every step of the iteration at least one word is removed from one of these languages, and Property 2 ensures that words that have been removed cannot reappear.

To sum up, we have shown the following theorem.

Theorem 7 Let L ∈ {FL⊥,FL¬,ALN}. The algorithm MATCH⊑L is a polynomial time algorithm that, given an Lmatching problem with subsumption conditions, returns a least matcher of this problem if it is solvable, and "fail" otherwise.

It should be noted that the algorithm MATCH⊑L does not work for L = FL0 since this language does not allow for the bottom concept, and thus the initialization step (Step 1) is not possible. However, instead of starting with σ(X) := ⊥, the algorithm can also start from the least matcher of C ≡? D. In case the side conditions do not introduce new variables (i.e., variables not contained in D), this modification works and yields a polynomial time matching algorithm. In contrast, if new variables are introduced, then we can show [Baader et al., 2000] that the size of the least matcher may grow exponentially in the size of the matching problem, and that there exists an exponential time algorithm for computing such matchers. Nevertheless, the size of the substitutions for variables in D can still be bounded polynomially, and if one is only interested in substitutions for these variables, then these can still be computed in polynomial time.

4 Matching under acyclic side conditions

Matching under acyclic side conditions (i.e., strict and nonstrict acyclic subsumption conditions) is more complex than matching under subsumption conditions for two reasons.

First, as already shown in [Baader et al., 1999], deciding the solvability of an FL0-matching problem under strict (and acyclic) subsumption conditions is NP-hard. It is easy to see that the same reduction works for the DLs FL⊥, FL¬, and ALN. Thus, assuming that P ̸= NP, there cannot exist a polynomial time algorithm computing matchers of matching problems under general side conditions.

Second, as shown by the following example, solvable matching problems under strict subsumption conditions no longer need to have a least matcher (but rather finitely many minimal matchers).

Example 8 Consider the FL⊥-matching problem A1 ⊓ . . . ⊓ An ≡? X1 ⊓ . . . ⊓Xn under the strict acyclic subsumption conditions {Xi+1 ⊏? Xi | 1 ≤ i ≤ n - 1} ∪ {X1 ⊏? ⊤}.

The pure matching problem enforces that each Xi must be replaced by a (possibly empty) conjunction of concept names from {A1, . . . , An}. Thus, the strict subsumption conditions can only be satisfied if X1 is replaced by one of these names, X2 by a conjunction of this name with an additional one, etc. From this it is easy to derive that the matchers of the problem are of the following form: given a permutation P := (p1, . . . , pn) of (1, . . . , n), the substitution σP is defined by σP (Xi) := Ap1 ⊓. . .⊓Api (1 ≤ i ≤ n). Thus, there are n! non-equivalent matchers, and it is easy to see that each of them is minimal.

The new contribution of this section is a (nondeterministic) algorithm, MATCH⊏L , that computes matchers of L-matching problems under acyclic side conditions for L ∈ {FL⊥,FL¬}. This non-deterministic algorithm matches the lower complexity bound (NP-hard) for the decision problem in the following sense. The length of every computation path of this algorithm is polynomially bounded in the size of the given matching problem. In case the problem is not solvable, every computation returns "fail". Otherwise, the successful computation paths yield all minimal matchers.

The algorithm handling acyclic side conditions

In the following, let M = 〈C ≡? D, S〉 be an L-matching problem (L ∈ {FL⊥,FL¬}) under acyclic side conditions. We assume that S = {X1 ρ?1 E1, . . . ,Xℓ ρ?ℓ Eℓ} for distinct variables X1, . . . ,Xℓ and patterns E1, . . . ,Eℓ such that Ei does not contain the variables Xi, . . . ,Xℓ. (The case where not all the left-hand side variables are distinct can be treated similarly.) We denote by S⊑ the set of side conditions obtained from S by replacing every ρi by ⊑.

Applied to input M, the algorithm MATCH⊏L first calls MATCH⊑L (〈C ≡? D, S⊑〉). If this yields "fail", thenM is also unsolvable. Otherwise, the computed substitution σ solves C ≡? D, but may still violate some of the strict subsumption conditions. Starting with the violated side condition with the largest index, the algorithm tries to modify σ such that this side condition is satisfied.

Assume that Xk ⊏? Ek is this side condition. Since σ solves Xk ⊑? Ek, we know that σ(Xk) ≡ σ(Ek). Thus, we must either make σ(Xk) more specific or σ(Ek) more general. Since MATCH⊑L computes the least solution, the first option cannot lead to a solution of the overall system. Hence, we must try the second one. The idea (which will be explained in more detail later) is that we consider the reduced normal form of σ(Ek). We try to make σ(Ek) more general by (non-deterministically) choosing one word from one of its role languages and by removing this word by appropriately modifying the role languages of the variables occurring in Ek. Since we want to compute minimal matchers, we make as little changes as possible in order to keep the substitution as specific as possible.

The new substitution σ′ obtained this way solves Xk ⊏? Ek, and since we only modified variables occurring in Ek, the side conditions with larger index are still satisfied. However, the side conditions with smaller index (even the nonstrict ones) as well as the matching problem need no longer be solved by σ′ . To overcome this problem, MATCH⊑L is used to compute the least substitution that (i) solves 〈C ≡? D, S⊑〉, and (ii) subsumes σ′ . It can be shown that the second condition (which can be expressed by a system of matching problems) makes sure that the computed substitution still solves the strict subsumption conditions from index k to ℓ. We can now continue the modification process with this substitution.

Algorithm 9 Let M = 〈C ≡? D, S〉 be an L-matching problem under acyclic side conditions. Then, MATCH⊏L works as follows:

1. If MATCH⊑L (〈C ≡? D, S⊑〉) returns "fail", then return "fail";
2. k := ℓ; σ := MATCH⊑L 〈{C ≡? D}, S⊑〉;
3. If k = 0, then return σ;
4. If σ(Xk) ρk σ(Ek), then continue with 5.
5. Guess modification σ′ of σ for Xk ⊏? Ek; If σ′ (Ek) ≡ σ(Ek), then return "fail"; M ′ := 〈{C ≡? D}∪{σ′ (Xj) ⊑? Xj|1 ≤ j ≤ ℓ}, S⊑〉; If MATCH⊑L (M ′ ) returns "fail", then return "fail"; σ := MATCH⊑L (M ′ )
6. k := k -1; continue with 3.

How to guess modifications

Here we sketch the modifications for FL⊥. (A formal definition for FL⊥ and FL¬ can be found in [Baader et al., 2000].) Recall that the goal is to make σ(Ek) more general by (nondeterministically) choosing one word w from one of its role languages and by removing this word by appropriately modifying the role languages of the variables occurring in Ek.

We call this a C-modification if w is picked from a role language corresponding to some atomic concept A. In this case, removing certain words from role languages of the variables in E suffices to obtain a minimal modification.

In case of a ⊥-modification, where w is picked from the role language corresponding to the ⊥-concept, the removal of some word v in the role language of a variable implicitly removes every continuation vv′ of v. To correct this effect, every word in {v}·NR is put back whenever some v is removed. In addition, since v is also implicitly removed from role languages corresponding to atomic concepts, it is also transferred to such role languages. This ensures that the computed substitution is as specific as possible. This is vital both for the proof of correctness and to obtain all minimal solutions.

The following example illustrates in more detail how the modifications work.

Example 10 Consider the FL⊥-matching problem A ⊓ ∀{r, s}.⊥ ≡? X1 ⊓∀r.X2 ⊓∀r.X3 under the strict subsumption conditions X2 ⊏? X1, X3 ⊏? X2.

Executing the above algorithm, we obtain in Step 2 as initial solution σ the following substitution:

The iteration begins in Step 3 by checking the second side condition, which is violated. Choosing a ⊥-modification in Step 4, we must choose a word from the role language {ε} corresponding to ⊥ in σ(X2) = σ(X3). In this case, we can only pick ε. To keep the change minimal, we do not simply remove it, but rather replace it by {r, s} in the role language corresponding to ⊥ in σ(X2). In addition, we transfer ε to the role language corresponding to A. This yields σ′ (X2) = ∀{r, s}.⊥ ⊓ ∀{ε}.A. The other variables remain unchanged.

In this case, the substitution σ′ itself solves the matching problemM ′ considered in Step 4, and thus MATCH⊑FL⊥ (M ′ ) returns σ′ .

In the second iteration, we find in Step 3 that the first side condition X2 ⊏? X1 no longer holds. In Step 4, we again choose a ⊥-modification, and choose the word r from the role language {r, s} corresponding to ⊥ in σ(X1). The modification replaces r by rr, rs and adds r to the role language corresponding to A. This yields σ′ (X1) := ∀{rr, rs, s}.⊥ ⊓ ∀{ε, r}.A. Again, this substitution solves M ′ , and thus the new value of σ is σ′ .

In the next iteration we have k = 0, ending the iteration in Step 3. The algorithm finally returns the substitution {X1 ↦→ ∀{rr, rs, s}.⊥ ⊓ ∀{ε, r}.A, X2 ↦→ ∀{r, s}.⊥ ⊓ ∀{ε}.A,X3 ↦→ ∀{ε}.⊥}.

Note that, in the first iteration step, it was not possible to apply a C-modification since the role language corresponding to A was empty. In the second step, we could have applied a C-modification, removing ε from the role language corresponding to A in σ(X1). Then, however, the systemM ′ obtained this way would not have been solvable. In fact, it is easy to see that the two matching problems A⊓∀{r, s}.⊥ ≡? X1 ⊓ ∀r.X2 ⊓ ∀r.X3 and ∀{r, s}.⊥ ⊑? X1 occurring in M ′ cannot be solved simultaneously.

Soundness and completeness for FL⊥ and FL¬ is proved in [Baader et al., 2000]. It is easy to see that the length of each computation branch of the nondeterminstic algorithm MATCH⊏L is polynomially bounded. Because matching under strict acyclic subsumption conditions in FL⊥ and FL¬ is known to be NP-hard, we obtain the following theorem.

Theorem 11 Let L ∈ {FL⊥, FL¬}. Deciding the solvability of L-matching problems under acyclic side conditions is an NP-complete problem.

The algorithm described above not only decides solvability of matching problems under acyclic side conditions. It also computes matchers in case the problem is solvable. To be more precise, all minimal matchers (w.r.t. subsumption of substitutions) are computed.

5 Future work

In contrast to the algorithm for matching under subsumption conditions, the algorithm MATCH⊏L presently is restricted to (i) L ∈ {FL⊥,FL¬} and (ii) acyclic side conditions. Naturally, the next step is to overcome the first restriction by extending the result for acyclic side conditions to ALN. We strongly conjecture that an algorithm similar to MATCH⊏L can be devised for this purpose.

In [Baader et al., 1999], FL0-matching problems with cyclic subsumption conditions are transformed into equivalent ones with acyclic subsumption conditions. Unfortunately, this approach cannot be extended to FL⊥ in a straightforward way. Instead, in order to overcome the second restriction, one might try to adapt the general idea of the algorithm MATCH⊏L to cyclic side conditions. Hence, one would first compute the solution to the analogous non-strict matching problem and then proceed by iteratively modifying the solution to satisfy the strict side conditions. Proving termination of this approach appears to be the main problem.

Apart from ALN and its sublanguages, it also seems promising to consider matching problems under side conditions in ALE, which extends FL¬ by existential restrictions. Since the algorithm MATCH⊑L proposed here is defined on top of an existing algorithm for pure matching problems (with certain properties), one might similarly take advantage of the matching algorithm proposed in [Baader and K¨ usters, 2000] for ALE-matching problems.