=Paper=
{{Paper
|id=Vol-1193/paper_29
|storemode=property
|title=Matching with Respect to General Concept Inclusions in the Description Logic EL
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_29.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/BaaderM14
}}
==Matching with Respect to General Concept Inclusions in the Description Logic EL==
https://ceur-ws.org/Vol-1193/paper_29.pdf
Matching with respect to General Concept
Inclusions in the Description Logic EL
Franz Baader and Barbara Morawska?
{baader,morawska}@tcs.inf.tu-dresden.de
Theoretical Computer Science, TU Dresden, Germany
Abstract. Matching concept descriptions against concept patterns was
introduced as a new inference task in Description Logics (DLs) almost
20 years ago, motivated by applications in the Classic system. For the
DL EL, it was shown in 2000 that the matching problem is NP-complete.
It then took almost 10 years before this NP-completeness result could
be extended from matching to unification in EL. The next big challenge
was then to further extend these results from matching and unification
without a TBox to matching and unification w.r.t. a general TBox, i.e.,
a finite set of general concept inclusions. For unification, we could show
some partial results for general TBoxes that satisfy a certain restriction
on cyclic dependencies between concepts, but the general case is still
open. For matching, we solve the general case in this paper: we show that
matching in EL w.r.t. general TBoxes is NP-complete by introducing a
goal-oriented matching algorithm that uses non-deterministic rules to
transform a given matching problem into a solved form by a polynomial
number of rule applications. We also investigate some tractable variants
of the matching problem.
1 Introduction
The DL EL, which offers the constructors conjunction (u), existential restric-
tion (∃r.C), and the top concept (>), has recently drawn considerable attention
since, on the one hand, important inference problems such as the subsumption
problem are polynomial in EL, even in the presence of general concept inclusions
(GCIs) [12]. On the other hand, though quite inexpressive, EL can be used to
define biomedical ontologies, such as the large medical ontology SNOMED CT.1
Matching of concept descriptions against concept patterns is a non-standard
inference task in Description Logics, which was originally motivated by appli-
cations of the Classic system [9]. In [11], Borgida and McGuinness proposed
matching as a means to filter out the unimportant aspects of large concept de-
scriptions appearing in knowledge bases of Classic. Subsequently, matching (as
well as the more general problem of unification) was also proposed as a tool for
detecting redundancies in knowledge bases [8] and to support the integration of
?
Supported by DFG under grant BA 1122/14-2
1
see http://www.ihtsdo.org/snomed-ct/
knowledge bases by prompting possible interschema assertions to the integrator
[10].
All three applications have in common that one wants to search the knowl-
edge 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 (which stand for descriptions). For example,
assume that we want to find concepts that are concerned with individuals hav-
ing a son and a daughter sharing some characteristic. This can be expressed
by the pattern D := ∃has-child.(Male u X) u ∃has-child.(Female u X), where X
is a variable standing for the common characteristic. The concept description
C := ∃has-child.(Tall u Male) u ∃has-child.(Tall u Female) matches this pattern in
the sense that, if we replace the variable X by the description Tall, the pattern be-
comes equivalent to the description. Thus, the substitution σ := {X 7→ Tall} is a
matcher modulo equivalence of the matching problem C ≡? D since C ≡ σ(D).
The original paper by Borgida and McGuinness actually considered matching
modulo subsumption rather than matching modulo equivalence: such a problem
is of the form C v? D, and a matcher is a substitution τ satisfying C v τ (D).
Obviously, any matcher modulo equivalence is also a matcher modulo subsump-
tion, but not vice versa. For example, the substitution σ> := {X 7→ >} is a
matcher modulo subsumption of the matching problem C v? D, but it is not a
matcher modulo equivalence of C ≡? D.
The first results on matching in DLs were concerned with sublanguages of
the Classic description language, which does not allow for existential restrictions
of the kind used in our example. A polynomial-time algorithm for computing
matchers modulo subsumption for a rather expressive DL was introduced in [11].
The main drawback of this algorithm was that it required the concept patterns
to be in structural normal form, and thus it was not able to handle arbitrary
matching problems. In addition, the algorithm was incomplete, i.e., it did not
always find a matcher, even if one existed. For the DL ALN , a polynomial-time
algorithm for matching modulo subsumption and equivalence was presented in
[6]. This algorithm is complete and it applies to arbitrary patterns. In [5], match-
ing in DLs with existential restrictions was investigated for the first time. In
particular, it was shown that in EL the matching problem (i.e., the problem of
deciding whether a given matching problem has a matcher or not) is polyno-
mial for matching modulo subsumption, but NP-complete for matching modulo
equivalence.
Unification is a generalization of matching where both sides of the problem
are patterns and thus the substitution needs to be applied to both sides. In
[8] it was shown that the unification problem in the DL FL0 , which offers the
constructors conjunction (u), value restriction (∀r.C), and the top concept (>),
is ExpTime-complete. In contrast, unification in EL is “only” NP-complete [7].
In the results for matching and unification mentioned until now, there was no
TBox involved, i.e., equivalence and subsumption was considered with respect
to the empty TBox. For unification in EL, first attempts were made to take gen-
eral TBoxes, i.e., finite sets of general concept inclusions (GCIs), into account.
However, the results obtained so far, which are again NP-completeness results,
are restricted to general TBoxes that satisfy a certain restriction on cyclic de-
pendencies between concepts [2,3].
For matching, we solve the general case in this paper: we show that match-
ing in EL w.r.t. general TBoxes is NP-complete by introducing a goal-oriented
matching algorithm that uses non-deterministic rules to transform a given match-
ing problem into a solved form by a polynomial number of rule applications.
The matching problems considered in this paper are actually generalizations of
matching modulo equivalence and matching modulo subsumption. For the spe-
cial case of matching modulo subsumption, we show that the problem is tractable
also in the presence of GCIs. The same is true for the dual problem where the
pattern is on the side of the subsumee rather than on the side of the subsumer.
Due to space constraints, we cannot provide complete proofs of our results.
They can be found in [1].
2 The Description Logics EL
The expressiveness of a DL is determined both by the formalism for describing
concepts (the concept description language) and the terminological formalism,
which can be used to state additional constraints on the interpretation of con-
cepts and roles in a so-called TBox.
The concept description language considered in this paper is called EL. Start-
ing with a finite set NC of concept names and a finite set NR of role names,
EL-concept descriptions are built from concept names using the constructors
conjunction (C u D), existential restriction (∃r.C for every r ∈ NR ), and top
(>). Since in this paper we only consider EL-concept descriptions, we will some-
times dispense with the prefix EL.
On the semantic side, concept descriptions are interpreted as sets. To be
more precise, an interpretation I = (∆I , ·I ) consists of a non-empty domain ∆I
and an interpretation function ·I that maps concept names to subsets of ∆I and
role names to binary relations over ∆I . This function is inductively extended to
concept descriptions as follows:
>I := ∆I , (C u D)I := C I ∩ DI , (∃r.C)I := {x | ∃y : (x, y) ∈ rI ∧ y ∈ C I }
A general concept inclusion axiom (GCI) is of the form C v D for concept
descriptions C, D. An interpretation I satisfies such an axiom C v D iff C I ⊆
DI . A general EL-TBox is a finite set of GCIs. An interpretation is a model of
a general EL-TBox if it satisfies all its GCIs.
A concept description C is subsumed by a concept description D w.r.t. a
general TBox T (written C vT D) if every model of T satisfies the GCI C v D.
We say that C is equivalent to D w.r.t. T (C ≡T D) if C vT D and D vT C.
If T is empty, we also write C v D and C ≡ D instead of C vT D and
C ≡T D, respectively. As shown in [12], subsumption w.r.t. general EL-TBoxes
is decidable in polynomial time.
An EL-concept description is an atom if it is an existential restriction or a
concept name. The atoms of an EL-concept description C are the subdescriptions
of C that are atoms, and the top-level atoms of C are the atoms occurring in
the top-level conjunction of C. Obviously, any EL-concept description is the
conjunction of its top-level atoms, where the empty conjunction corresponds
to >. The atoms of a general EL-TBox T are the atoms of all the concept
descriptions occurring in GCIs of T .
We say that a subsumption between two atoms is structural if their top-level
structure is compatible. To be more precise, following [2] we define structural
subsumption between atoms as follows: the atom C is structurally subsumed by
the atom D w.r.t. T (C vsT D) iff one of the following holds:
1. C = D is a concept name,
2. C = ∃r.C 0 , D = ∃r.D0 , and C 0 vT D0 .
It is easy to see that subsumption w.r.t. ∅ between two atoms implies structural
subsumption w.r.t. T , which in turn implies subsumption w.r.t. T . The matching
algorithms presented below crucially depend on the following characterization
of subsumption w.r.t. general EL-TBoxes first stated in [2]:
Lemma 1. Let T be an EL-ontology and C1 , . . . , Cn , D1 , . . . , Dm be atoms.
Then C1 u · · · u Cn vT D1 u · · · u Dm iff for every j ∈ {1, . . . , m}
1. there is an index i ∈ {1, . . . , n} such that Ci vsT Dj or
2. there are atoms A1 , . . . , Ak , B of T (k ≥ 0) such that
(a) A1 u · · · u Ak vT B,
(b) for every η ∈ {1, . . . , k} there is i ∈ {1, . . . , n} with Ci vsT Aη , and
(c) B vsT Dj .
3 Matching in EL
In addition to the set NC of concept names (which must not be replaced by sub-
stitutions), we introduce a set NV of concept variables (which may be replaced
by substitutions). Concept patterns are now built from concept names and con-
cept variables by applying the constructors of EL. A substitution σ maps every
concept variable to an EL-concept description. It is extended to concept patterns
in the usual way:
– σ(A) := A for all A ∈ NC ∪ {>},
– σ(C u D) := σ(C) u σ(D) and σ(∃r.C) := ∃r.σ(C).
An EL-concept pattern C is ground if it does not contain variables, i.e., if it is
a concept description. Obviously, a ground concept pattern is not modified by
applying a substitution.
Definition 2. Let T be a general EL-TBox.2 An EL-matching problem w.r.t.
T is a finite set Γ = {C1 v? D1 , . . . , Cn v? Dn } of subsumptions between EL-
concept patterns, where for each i, 1 ≤ i ≤ n, Ci or Di is ground. A substitution σ
is a matcher of Γ w.r.t. T if σ solves all the subsumptions in Γ , i.e. if σ(C1 ) vT
σ(D1 ), . . . , σ(Cn ) vT σ(Dn ). We say that Γ is matchable w.r.t. T if it has a
matcher.
Matching problems modulo equivalence and subsumption are special cases of
the matching problems introduced above:
– The EL-matching problem Γ is a matching problem modulo equivalence if
C v? D ∈ Γ implies D v? C ∈ Γ . This coincides with the notion of matching
modulo equivalence considered in [6,5], but extended to a non-empty general
TBox.
– The EL-matching problem Γ is a left-ground matching problem modulo sub-
sumption if C v? D ∈ Γ implies that C is ground. This coincides with the
notion of matching modulo subsumption considered in [6,5], but again ex-
tended to a non-empty general TBox.
– The EL-matching problem Γ is a right-ground matching problem modulo
subsumption if C v? D ∈ Γ implies that D is ground. To the best of our
knowledge, this notion of matching has not been investigated before.
We will show in the following that the general case of matching, as introduced
in Definition 2, and thus also matching modulo equivalence, is NP-complete,
whereas the two notions of matching modulo subsumption are tractable, even in
the presence of GCIs.
4 Matching Modulo Subsumption
The case of left-ground matching problems modulo subsumption can be treated
as sketched in [5] for the case without a TBox. Given a general EL-TBox T and
two substitutions σ, τ , we define
σ vT τ iff σ(X) vT τ (X) for all X ∈ NV .
Consequently, if we define σ> as the substitution satisfying σ> (X) = > for
all X ∈ NV , then σ vT σ> holds for all substitutions σ. Since the concept
constructors of EL are monotonic w.r.t. subsumption, this implies σ(D) vT
σ> (D) for all concept patterns D.
Lemma 3. Let Γ = {C1 v? D1 , . . . , Cn v? Dn } be a left-ground matching
problem modulo subsumption. Then Γ has a matcher w.r.t. T iff σ> is a matcher
of Γ w.r.t. T .
2
Note that the GCIs in T are built using concept descriptions, and thus do not contain
variables.
Proof. The “if” direction is trivial. To see the “only-if” direction, assume that σ
is a matcher of Γ w.r.t. T . Then we have, for all i, 1 ≤ i ≤ n, that σ> (Ci ) =
Ci = σ(Ci ) vT σ(Di ) vT σ> (Di ), which shows that σ> is a matcher of Γ w.r.t.
T. t
u
The lemma shows that it is sufficient to test whether the substitution σ>
is a matcher of Γ , i.e., whether σ> (Ci ) vT σ> (Di ) holds for all i, 1 ≤ i ≤
n. Since in EL subsumption w.r.t. general TBoxes is decidable in polynomial
time, this yields a polynomial-time algorithm for left-ground matching modulo
subsumption in EL.
Theorem 4. Let Γ be a left-ground EL-matching problem modulo subsumption
and T a general EL-TBox. Then we can decide in polynomial time whether Γ
has a matcher w.r.t. T or not.
The case of right-ground matching problems modulo subsumption can be
treated similarly. However, since EL does not have the bottom concept ⊥ as
a concept constructor, we cannot simply define σ⊥ as the substitution satisfying
σ⊥ (X) = ⊥ for all X ∈ NV , and then show that that the right-ground matching
problems modulo subsumption, Γ , has a matcher w.r.t. T iff σ⊥ is a matcher of
Γ w.r.t. T . Instead, we need to define σ⊥ in a more complicated manner.
Given a general EL-TBox T and a right-ground matching problems modulo
subsumption Γ = {C1 v? D1 , . . . , Cn v? Dn }, we use ⊥(Γ, T ) to denote the
EL-concept description that is the conjunction of all the atoms of T and of
D1 , . . . , Dn . We now define σ⊥(Γ,T ) as the substitution satisfying σ⊥(Γ,T ) (X) =
⊥(Γ, T ) for all X ∈ NV
Lemma 5. Let Γ = {C1 v? D1 , . . . , Cn v? Dn } be a right-ground matching
problem modulo subsumption. Then Γ has a matcher w.r.t. T iff σ⊥(Γ,T ) is a
matcher of Γ w.r.t. T .
Proof. The “if” direction is trivial. To see the “only-if” direction, assume that
σ is a matcher of Γ w.r.t. T . We need to show that this implies the σ⊥(Γ,T ) is
also a matcher of Γ w.r.t. T , i.e., that it satisfies σ⊥(Γ,T ) (C) vT σ⊥(Γ,T ) (D) for
every subsumption C v? D ∈ Γ .
More generally, we consider subsumptions C v? D where C is a subpattern
of a pattern occurring in Γ or T and D is an atom of T or D1 , . . . , Dn . We show
the following claim:
Claim: For every such subsumption C v? D, it holds that σ(C) vT σ(D) im-
plies σ⊥(Γ,T ) (C) vT σ⊥(Γ,T ) (D).
Before proving the claim, let us show that this implies that σ⊥(Γ,T ) solves Γ
w.r.t. T . In fact, any subsumption in Γ is of the form C v? E1 u . . . u Ek where
C is a subpattern of a pattern occurring in Γ , and E1 , . . . , Ek are atoms of one
of the Di . In addition, a substitution solves C v? E1 u . . . u Ek w.r.t. T iff it
solves all the subsumptions C v? Ei for i = 1, . . . , k.
We prove the claim by induction on the size |C| of the left-hand side C of the
subsumption C v? D. Since D is ground, σ(C) vT σ(D) implies σ(C) vT D.
Let C = F1 u . . . u F` , where F1 , . . . , F` are atoms. We distinguish the following
three cases:
1. If there is an index i ∈ {1, . . . , `} such that Fi is a variable, then σ⊥(Γ,T ) (Fi ) v
D since D occurs as a conjunct in ⊥(Γ, T ). This implies σ⊥(Γ,T ) (C) vT D.
2. If there is an index i ∈ {1, . . . , `} such that Fi is ground and σ(Fi ) vT D,
then σ⊥(Γ,T ) (Fi ) = Fi = σ(Fi ) vT D. This again implies σ⊥(Γ,T ) (C) vT D.
3. Assume that the above two cases do not hold. Using Lemma 1, we can
distinguish two more cases, depending on whether the first or the second
condition of the lemma applies.
(a) If the first condition applies, then there is an index i ∈ {1, . . . , `} such
that Fi vsT D. Since Fi is neither ground nor a variable, we know
that Fi is a non-ground existential restriction. Thus, Fi = ∃r.F 0 , D =
∃r.(D1 u . . . u Dm ) with D1 , . . . , Dm atoms, and σ(F 0 ) vT Di for all
i ∈ {1, . . . , m}. Since F 0 is a subpattern of C, Di are atoms of D, and
|F 0 | < |C|, we can apply the induction hypothesis to the subsumptions
F 0 v? Di . This yields σ⊥(Γ,T ) (F 0 ) vT Di for all i ∈ {1, . . . , m}, and thus
σ⊥(Γ,T ) (C) vT D.
(b) If the second condition applies, then there are atoms A1 , . . . , Ak , B of T
such that A1 u · · · u Ak vT B vT D and for each η ∈ {1, . . . , k}, there
is j ∈ {1, . . . , `} such that
i. Fj is a concept variable and σ(Fj ) vT Aη , or
ii. Fj is ground and Fj vT Aη , or
iii. Fj = ∃r.F 0 , Aη = ∃r.A0 and σ(F 0 ) vT A0 .
It is sufficient to show that the subsumption relationships in 3(b)i and
3(b)iii also hold if we replace σ by σ⊥(Γ,T ) . For 3(b)i this can be shown
as in 1 and for 3(b)iii as in 3a.
This completes the proof of the claim, and thus of the lemma. t
u
Since the size of ⊥(Γ, T ) is polynomial in the size of Γ and T , this lemma
yields a polynomial-time decision procedure for right-ground matching modulo
subsumption.
Theorem 6. Let Γ be a right-ground EL-matching problem modulo subsumption
and T a general EL-TBox. Then we can decide in polynomial time whether Γ
has a matcher w.r.t. T or not.
5 The General Case
NP-hardness for the general case follows from the known NP-hardness result
for matching modulo equivalence without a TBox [5]. In the following, we show
that matching in EL w.r.t. general TBoxes is in NP by introducing a goal-
oriented matching algorithm that uses non-deterministic rules to transform a
given matching problem into a solved form by a polynomial number of rule
applications.
Let T be a general EL-TBox and Γ0 an EL-matching problem. We can assume
without loss of generality that all the subsumptions C v? D in Γ0 are such that
either C or D is non-ground. In fact, if both C and D are ground, then the
following holds:
– If C vT D, then Γ0 has a matcher w.r.t. T iff Γ0 \ {C v? D} has a matcher
w.r.t. T .
– If C 6vT D, then Γ0 does not have a matcher w.r.t. T .
Consequently, we can either remove all the offending ground subsumptions with-
out changing the solvability status of the problem, or immediately decide non-
solvability. Using the fact that C vT D1 u D2 iff C vT D1 and C vT D2 , we
can additionally normalize Γ0 such that the right-hand side of each subsumption
in Γ0 is an atom. We call an EL-matching problem normalized if C v? D ∈ Γ0
implies that (i) either C or D is non-ground, and (ii) D is an atom.
Thus, assume that Γ0 is a normalized EL-matching problem. Our algorithm
starts with Γ := Γ0 , and then applies non-deterministic rules to Γ . A non-
failing application of a rule may add subsumptions to Γ . Note, however, that
a subsumption is only added if it is not yet present. New subsumptions that
are added are marked as “unsolved,” as are initially all the subsumptions of
Γ0 . A rule application may fail, which means that this attempt of solving the
matching problem was not successful. A non-failing rule application marks one
of the subsumptions in the matching problem as “solved.” Rules are applied until
all subsumptions are marked “solved” or an attempt to apply a rule has failed.
Our definition of the rules uses a function Dec(. . . ) on subsumptions of the
form C v? D, where C and D are atoms and D is not a variable. A call of
Dec(C v? D) returns a (possibly empty) set of subsumptions or it fails:
1. Dec(C v? D) := {C v? D}, if C is a variable.
2. If D1 , . . . , Dn are atoms, then Dec(∃r.C 0 v? ∃r.(D1 u · · · u Dn )) fails if
there is an i ∈ {1, . . . , n} such that both sides of C 0 v? Di are ground and
C 0 6vT Di . Otherwise, Dec(∃r.C 0 v? ∃r.(D1 u · · · u Dn )) := {C 0 v? Di | 1 ≤
i ≤ n and C 0 or Di is non-ground}.
3. If C = ∃r.C 0 and D = ∃s.D0 for roles s 6= r, then Dec(C v? D) fails.
4. If C = A is a concept name and D = ∃r.D0 an existential restriction, then
Dec(C v? D) fails.
5. If D = A is a concept name and C = ∃r.C 0 an existential restriction, then
Dec(C v? D) fails.
6. If both C and D are ground and C 6vO D then Dec(C v? D) fails, and
otherwise returns ∅.
Algorithm 7. Let Γ0 be a normalized EL-matching problem. Starting with
Γ := Γ0 , apply the rules of Figure 1 and Figure 2 exhaustively in the following
order:
Eager Solving – variable on the right:
Condition: An unsolved subsumption C v? X ∈ Γ where X ∈ NV .
Action:
– If there is some subsumption of the form X v? D ∈ Γ such that C 6vT D,
then the rule application fails.
– Otherwise, mark C v? X as “solved.”
Eager Solving – variable on the left:
Condition: An unsolved subsumption X v? D ∈ Γ where X ∈ NV .
Action:
– If there is some subsumption of the form C v? X ∈ Γ such that C 6vT D,
then the rule application fails.
– Otherwise, mark X v? D as “solved."
Fig. 1. Eager Rules
(1) Eager rule application: If an eager rule from Figure 1 applies, apply it
and if it fails, stop and return “failure.”
(2) Non-deterministic rule application: If no eager rule is applicable, let s
be an unsolved subsumption in Γ . Choose one of the non-deterministic rules
of Figure 2, and apply it to s. If this rule application fails, then stop and
return “failure.”
If no more rule applies and the algorithm has not stopped returning “failure,”
then return “success.”
In (2), the choice which unsolved subsumption to consider next is don’t care
non-deterministic. However, choosing which rule to apply to the chosen sub-
sumption is don’t know non-deterministic. Additionally, the application of a
non-deterministic rules may require don’t know non-deterministic choices to be
made. If a non-deterministic rule is applied to a subsumption s, then neither its
left-hand side nor its right-hand side is a variable. In fact, a subsumption that
has a variable on one of its sides is solved by one of the eager rules, which have
precedence over the non-deterministic rules.
It is easy to see that the subsumptions added by the non-deterministic rules
satisfy the normalization conditions (i) and (ii), and thus all the sets Γ generated
during a run of the algorithm are normalized EL-matching problems. The next
lemma states an important property ensured by the presence of the eager rules.
Lemma 8. If Γ is a matching problem generated during a non-failing run of
the algorithm, and both C v? X ∈ Γ and X v? D ∈ Γ are solved, then C vT D.
Proof. Obviously, one of the two subsumptions was solved after the other. This
means that, when it was solved by the application of an eager rule, the other
one was already present. Since we consider a non-failing run, the application of
the eager rule did not fail, which yields C vT D. t
u
Decomposition:
Condition: This rule applies to s = C1 u · · · u Cn v? D ∈ Γ .
Action: Its application chooses an index i ∈ {1, . . . , n} and calls Dec(Ci v? D).
If this call does not fail, then it adds the returned subsumptions to Γ , and marks
s as solved. If Dec(Ci v? D) fails, it returns “failure.”
Mutation :
Condition: This rule applies to s = C1 u · · · u Cn v? D in Γ .
Action: Its application tries to choose atoms A1 , . . . , Ak , B of T such that A1 u
· · · u Ak vT B holds. If this is not possible, then it returns “failure.” Otherwise,
it performs the following two steps:
– Choose for each η ∈ {1, . . . , k} an i ∈ {1, . . . , n} and call Dec(Ci v? Aη ). If
this call does not fail, it adds the returned subsumptions to Γ . Otherwise, if
Dec(Ci v? Aη ) fails, the rule returns “failure.”
– If it has not failed before and Dec(B v? D) does not fail, it adds the returned
subsumptions to Γ . Otherwise, if Dec(B v? D) fails, it returns "failure".
If these steps did not fail, then the rule marks s as solved.
Fig. 2. Non-deterministic rules
Any run of the algorithm terminates after a polynomial number of steps. The
main reason for this is that there are only polynomially many subsumptions that
can occur in the matching problems Γ generated during a run.
Lemma 9. Let Γ be a matching problem generated during a run of Algorithm 7.
Then any subsumption occurring in Γ is of one of the following forms:
1. A subsumption contained in the original input matching problem Γ0 .
2. A subsumption of the form C v? D where C, D are subpatterns of concept
patterns occurring in Γ0 .
3. A subsumption of the form C v? A or A v? C where A is an atom of T and
C is a subpattern of a concept pattern occurring in Γ0 .
Since any rule application either fails while trying to solve an unsolved sub-
sumption (in which case the algorithm stops immediately) or actually solves an
unsolved subsumption, there can be only polynomially many rule applications
during a run. In addition, it is easy to see that each rule application can be real-
ized in polynomial time, with a polynomial number of possible non-deterministic
choices. This shows that Algorithm 7 is indeed an NP-algorithm. It remains to
show that it is sound and complete.
To show soundness, assume that Γ is a matching problem obtained after ter-
mination of a non-failing run of the algorithm. Since the run terminated without
failure, all the subsumptions in Γ are solved. We use the subsumptions of the
form X v? C ∈ Γ to define a substitution σΓ . Note that the fact that Γ is
a normalized EL-matching problem implies that C is a ground pattern, i.e., a
concept description. For each variable X ∈ NV , we define
Γ
SX := {C | X v? C ∈ Γ },
Γ Γ
and denote the conjunction of all the elements of SX as uSX , where the empty
conjunction is >. The substitution σΓ is now defined as
Γ
σΓ (X) := uSX for all X ∈ NV .
Lemma 10. σΓ is a matcher of Γ w.r.t. T .
Since the input matching problem Γ0 is contained in Γ , this shows that σΓ
is a matcher also of Γ0 w.r.t. T . This completes the proof of soundness.
Regarding completeness, we can use a given matcher of Γ0 w.r.t. T to guide
the application of the non-deterministic rules such that a non-failing run is gen-
erated.
Lemma 11. Let σ be a matcher of Γ0 w.r.t. T . Then there is a non-failing and
terminating run of Algorithm 7 producing a matching problem Γ such that σ is
a matcher of Γ w.r.t. T .
This lemma provides the final step towards showing that Algorithm 7 is an
NP-decision procedure for matching w.r.t. general TBoxes in EL.
Theorem 12. The problem of deciding whether a given EL-matching problem
has a matcher w.r.t. a given general EL-TBox or not is NP-complete.
6 Conclusion
We have extended the known results for matching in EL [5] to the case where
subsumption and equivalence is considered w.r.t. a non-empty general TBox, i.e.,
a non-empty set of GCIs. For the DL FL0 , matching without GCIs is polynomial,
and this remains true even in the extension ALN of FL0 . It would be interesting
to see how one can solve matching problems w.r.t. general TBoxes in these DLs.
Since already subsumption in FL0 w.r.t. general TBoxes is ExpTime-complete
[4], the complexity of solving such matching problems is at least ExpTime-hard.
Another interesting open problem is unification in EL w.r.t. general TBoxes.
References
1. Baader, F., , Morawska, B.: Matching with respect to general concept inclusions
in the description logic EL. LTCS-Report 14-03, Chair of Automata Theory, Insti-
tute of Theoretical Computer Science, Technische Universität Dresden, Dresden,
Germany (2014), see http://lat.inf.tu-dresden.de/research/reports.html.
2. Baader, F., Borgwardt, S., Morawska, B.: Extending unification in EL towards
general TBoxes. In: Proc. of the 13th Int. Conf. on Principles of Knowledge Rep-
resentation and Reasoning (KR 2012). pp. 568–572. AAAI Press/The MIT Press
(2012)
3. Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification
in ELHR+ w.r.t. cycle-restricted ontologies. In: Thielscher, M., Zhang, D. (eds.)
Pro. of 25th Australasian Joint Conf. on Artificial Intelligence (AI’12). Lecture
Notes in Artificial Intelligence, vol. 7691, pp. 493–504. Springer-Verlag (2012)
4. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Kaelbling, L.P.,
Saffiotti, A. (eds.) Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJ-
CAI 2005). pp. 364–369. Morgan Kaufmann, Los Altos, Edinburgh (UK) (2005)
5. Baader, F., Küsters, R.: Matching in description logics with existential restrictions.
In: Proc. of the 7th Int. Conf. on Principles of Knowledge Representation and
Reasoning (KR 2000). pp. 261–272 (2000)
6. Baader, F., Küsters, R., Borgida, A., McGuinness, D.L.: Matching in description
logics. J. of Logic and Computation 9(3), 411–447 (1999)
7. Baader, F., Morawska, B.: Unification in the description logic EL. Logical Methods
in Computer Science 6(3) (2010)
8. Baader, F., Narendran, P.: Unification of concept terms in description logics. J. of
Symbolic Computation 31(3), 277–305 (2001)
9. Borgida, A., Brachman, R.J., McGuinness, D.L., Alperin Resnick, L.: CLASSIC:
A structural data model for objects. In: Proc. of the ACM SIGMOD Int. Conf. on
Management of Data. pp. 59–67 (1989)
10. Borgida, A., Küsters, R.: What’s not in a name? Initial explorations of a structural
approach to integrating large concept knowledge-bases. Tech. Rep. DCS-TR-391,
Rutgers University (1999)
11. Borgida, A., McGuinness, D.L.: Asking queries about frames. In: Proc. of the 5th
Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’96).
pp. 340–349 (1996)
12. Brandt, S.: Polynomial time reasoning in a description logic with existential re-
strictions, GCI axioms, and—what else? In: de Mántaras, R.L., Saitta, L. (eds.)
Proc. of the 16th Eur. Conf. on Artificial Intelligence (ECAI 2004). pp. 298–302
(2004)