Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. However, the unification algorithms for EL developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the developed unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fixpoint and descriptive semantics. We show that hybrid unification in EL is NP-complete.
The DL E L, which offers the constructors conjunction (u), existential restriction
(9r: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 E L, even in the presence of GCIs [
(1)
In a DL ontology, one can use concept definitions to introduce abbreviations for concept descriptions. For example, we could use the definition Head_injury Injury u 9 nding_site:Head to define Head_injury as an injury that is located at ? Supported by DFG under grant BA 1122/14-2 1 see http://www.ihtsdo.org/snomed-ct/ the head. More generally, GCIs can be used to require that certain inclusions hold in all models of the ontology. For example,
(2) is a GCI that says that a severe finding entails an emergency status.
Knowledge representation systems based on DLs provide their users with various inference services that allow them to deduce implicit knowledge from the explicitly represented knowledge. For instance, the subsumption algorithm allows one to determine subconcept-superconcept relationships. For example, the concept description (1) is subsumed by (i.e., is a subconcept of) the concept description 9 nding:9status:Severe. With respect to the GCI (2), it is thus also subsumed by 9status:Emergency, i.e., in all models of this GCI, patients with severe head injury have an emergency status.
Unification in DLs has been proposed in [
(3) These two concept descriptions are not equivalent, but they are nevertheless meant to represent the same concept. They can obviously be made equivalent by introducing definitions for the concept names Head_injury and Severe_injury: if we define Head_injury Injury u 9 nding_site:Head and Severe_injury Injury u 9status:Severe, then the two concept descriptions (1) and (3) are equivalent w.r.t. these definitions. If such definitions exist, we say that the descriptions are unifiable, and call the TBox consisting of these definitions a unifier. In the standard definition of unification in DLs, it is required that this TBox is acyclic, i.e., there are no cyclic dependencies between the definitions.
To motivate our interest in unification w.r.t. GCIs, assume that the second developer uses the description
instead of (3). The descriptions (1) and (4) are not unifiable without additional GCIs, but they are unifiable, with the same unifier as above, if the GCI (2) is present in a background ontology.
In [
In [
In this paper, we follow another line of attack on this problem. Instead of
restricting the input ontology, we allow cyclic TBoxes to be used as unifiers.
Subsumption w.r.t. cyclic TBoxes in E L has been investigated in detail in [
(5)
there is no least concept description (w.r.t. subsumption) that subsumes both
Human and Horse. What elements of these two concepts have in common is that
they are the origin of an infinite parent-chain, and thus the concept X with
definition X 9parent:X is their lcs, if we interpret this definition with
gfpsemantics, but the GCIs (5) still with descriptive semantics. A hybrid unifier is
a cyclic TBox that, together with the background ontology consisting of GCIs,
entails the unification problem w.r.t. hybrid semantics. We will show that hybrid
unification in E L, i.e., the problem of testing whether a hybrid unifier exists, is
NP-complete. The proofs, which can be found in [
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 concepts in a so-called ontology.
The concept description language The concept description language considered in this paper is called E L. Starting with a finite set NC of concept names and a finite set NR of role names, E L-concept descriptions are built from concept names using the constructors conjunction (C u D), existential restriction (9r:C for every r 2 NR), and top (>). Since in this paper we only consider E L-concept descriptions, we will usually dispense with the prefix E L.
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 := CI \ DI ; (9r:C)I := fx j 9y : (x; y) 2 rI ^ y 2 CI g Classical ontologies and subsumption A concept definition is an expression of the form X C where X is a concept name and C is a concept description, and a general concept inclusion (GCI) is an expression of the form C v D, where C; D are concept descriptions. An interpretation I is a model of this concept definition (this GCI) if it satisfies XI = CI (CI DI ). This semantics for GCIs and concept definitions is usually called descriptive semantics.
A TBox is a finite set T of concept definitions that does not contain multiple definitions, i.e., fX C; X Dg T implies C = D. Note that we do not prohibit cyclic dependencies among the concept definitions in a TBox, i.e., when defining a concept X we may (directly or indirectly) refer to X. An acyclic TBox is a TBox without cyclic dependencies. An ontology is a finite set of GCIs. The interpretation I is a model of a TBox (ontology) iff it is a model of all concept definitions (GCIs) contained in it.
A concept description C is subsumed by a concept description D w.r.t. an
ontology O (written C vO D) if every model of O is also a model of the GCI
C v D. We say that C is equivalent to D w.r.t. O (C O D) if C vO D
and D vO C. As shown in [
Note that TBoxes can be seen as special kinds of ontologies since concept definitions X C can of course be expressed by GCIs X v C; C v X. Thus, the above definition of subsumption also applies to TBoxes. However, in our hybrid ontologies we will interpret concept definitions using greatest fixpoint semantics rather than descriptive semantics.
Hybrid ontologies We assume in the following that the set of concept names NC is partitioned into the set of primitive concepts Nprim and the set of defined concepts Ndef . In a hybrid TBox, concept names occurring on the left-hand side of a concept definition are required to come from the set Ndef , whereas GCIs may not contain concept names from Ndef .
Definition 1 (Hybrid E L-ontologies). A hybrid E L-ontology is a pair (O; T ), where O is an E L-ontology containing only concept names from Nprim , and T is a (possibly cyclic) E L-TBox such that X C iff X 2 Ndef .
C 2 T for some concept description The idea underlying the definition of hybrid ontologies is the following: O can be used to constrain the interpretation of the primitive concepts and roles, whereas T tells us how to interpret the defined concepts occurring in it, once the interpretation of the primitive concepts and roles is fixed.
A primitive interpretation J is defined like an interpretation, with the only difference that it does not provide an interpretation for the defined concepts. A primitive interpretation can thus interpret concept descriptions built over Nprim and NR, but it cannot interpret concept descriptions containing elements of Ndef . Given a primitive interpretation J , we say that the (full) interpretation I is based on J if it has the same domain as J and its interpretation function coincides with J on Nprim and NR.
Given two interpretations I1 and I2 based on the same primitive interpretation J , we define I1 J I2 iff XI1 XI2 for all X 2 Ndef :
It is easy to see that the relation J is a partial order on the set of
interpretations based on J . In [
We call such a model I a gfp-model of T .
Definition 2 (Semantics of hybrid E L-ontologies). The interpretation I is a hybrid model of the hybrid E L-ontology (O; T ) iff I is a gfp-model of T and the primitive interpretation J it is based on is a model of O.
It is well-known that gfp-semantics coincides with descriptive semantics for acyclic TBoxes. Thus, if T is actually acyclic, then I is a hybrid model of (O; T ) according to the semantics introduced in Definition 2 iff it is a model of T [ O w.r.t. descriptive semantics, i.e., iff I is a model of every GCI in O and of every concept definition in T .
Subsumption w.r.t. hybrid EL-ontologies Let (O; T ) be a hybrid E
Lontology and C; D E L-concept descriptions. Then C is subsumed by D w.r.t.
(O; T ) (written C vgfp;O;T D) iff every hybrid model of (O; T ) is also a model
of the GCI C v D. As shown in [
Here, we sketch the proof-theoretic approach for deciding subsumption from
[
C vn C
C vn E C u D vn E (Refl)
C vn > (Top)
D vn E (AndL1) C u D vn E (AndL2)
C vn D C vn E
C vn D u E C vn D X vn D for X
C 2 T (DefL)
C vn D 9r:C vn 9r:D (Ex)
D vn C D vn+1 X for X
C 2 T (DefR)
C vn E F vn D
C vn D for E v F 2 O (Start) (AndR) (GCI)
The rules of the Hybrid E L-ontology Calculus HC(O; T ; ) are depicted in Fig. 1. Again, if (O; T ) and are clear from the context, we will sometimes dispense with specifying them explicitly and just talk about the calculus HC. The rules of this calculus can be used to derive new sequents from sequents that have already been derived. For example, the sequents in the first row of the figure can always be derived without any prerequisites, using the rules (Refl), (Top), and (Start), respectively. Using the rule (AndR), the sequent C vn D u E can be derived in case both C vn D and C vn E have already been derived. Note that the rule Start applies only for n = 0. Also note that, in the rule (DefR), the index is incremented when going from the prerequisite to the consequent.
A derivation in HC(O; T ; ) can be represented in an obvious way by a proof
tree whose nodes are sequents: a proof tree for C vn D has this sequent as its
root, instances of the rules Refl, Top, and Start as leaves, and each parent-child
relation corresponds to an instance of a rule of HC other than Refl, Top, and
Start (see [
Theorem 4 (Soundness and Completeness of HC). Let (O; T ) be a hybrid E L-TBox, a finite set of GCIs, and C; D sub-descriptions of concept descriptions occurring in O; T , and . Then C vgfp;O;T D iff C v1 D can be derived in HC(O; T ; ).
In [
For n 2 N[f1g, we collect the GCIs C v D such that C vn D is derivable in
HC(O; T ; ) in the set Dn(O; T ; ). Obviously, D0(O; T ; ) consists of all GCIs
built from sub-descriptions of concept descriptions occurring in O; T , and , and
it is not hard to show that Dn+1(O; T ; ) Dn(O; T ; ) holds for all n 0 [
We will first introduce the new notion of hybrid unification and then relate it to
the notion of unification in E L w.r.t. background ontologies considered in [
It is easy to see that the notion of a classical unifier indeed corresponds to
the notion of a unifier introduced in [
Obviously, any classical unifier is a hybrid unifier, but the converse need
not hold. The following is an example of an E L-unification problem w.r.t. a
background ontology that has a hybrid unifier, but no classical unifier.
Example 6. Let O be the ontology consisting of the GCIs (5), and
:= fHuman v X; Horse v X; X v 9parent:Xg;
where X 2 Ndef and Human; Horse 2 Nprim . Intuitively, this unification problem
asks for a concept such that all horses and humans belong to this concept and
every element of it has a parent also belonging to it. It is easy to see that
T := fX 9parent:Xg is a hybrid unifier of w.r.t. O. In fact, we have already
mentioned in the introduction that X is then the lcs of Human and Horse, and
obviously the hybrid ontology (O; T ) also entails the third GCI in . It is also
not hard to show that this unification problem does not have a classical unifier,
basically for the same reasons that Human and Horse do not have an E L-concept
description as lcs (see [
Flat unification problems To simplify the technical development, it is convenient to normalize the unification problem appropriately. To introduce this normal form, we need the notion of an atom. An atom is a concept name or an existential restriction. Obviously, every E L-concept description C is a finite conjunction of atoms, where > is considered to be the empty conjunction. An atom is called flat if it is a concept name or an existential restriction of the form 9r:A for a concept name A.
The GCI C v D is called flat if C is a conjunction of n 0 flat atoms and D is a flat atom. The unification problem w.r.t. the ontology O is called flat if both and O consist of flat GCIs.
Given a unification problem w.r.t. an ontology O, we can compute in
polynomial time (see [
Local unifiers The main reason why E L-unification without background ontologies is in NP is that any unification problem that has a unifier also has a local unifier. For classical unification w.r.t. background ontologies this is only true if the background ontology is cycle-restricted.
Given a flat unification problem w.r.t. an ontology O, we denote by At the set of atoms occurring as sub-descriptions in GCIs in or O. The set of non-variable atoms is defined as by Atnv := At n Ndef . Though the elements of Atnv cannot be defined concepts, they may contain defined concepts if they are of the form 9r:X for some role r and a concept name X 2 Ndef .
In order to define local unifiers, we consider assignments of subsets X of Atnv to defined concepts X 2 Ndef . Such an assignment induces a TBox T := fX
l D2 X
D j X 2 Ndef g: We call such a TBox local. The (hybrid or classical) unifier T of w.r.t. O is called local unifier if T is local, i.e., there is an assignment such that T = T .
As shown in [
Example 7. Let O = fB v 9s:D; D v Bg and consider the unification problem := fA1 u B v Y1; Y1 v A1 u B; A2 u B v Y2; Y2 v A2 u B;
9s:Y1 v X; 9s:Y2 v X; X v 9s:Xg;
where A1; A2; B 2 Nprim and X; Y1; Y2 2 Ndef . This problem has the classical
unifier T := fY1 A1 u B; Y2 A2 u B; X 9s:Bg, which is not local since it
uses the atom 9s:B. As shown in [
To overcome the problem of missing local unifiers, the notion of a
cyclerestricted ontology was introduced in [
The main technical result shown in [
The fact that hybrid E L-unification w.r.t. arbitrary E L-ontologies is in NP is an easy consequence of the following proposition.
Proposition 8. Consider a flat E L-unification problem w.r.t. an E L-ontology O. If has a hybrid unifier w.r.t. O then it has a local hybrid unifier w.r.t. O. In fact, the NP-algorithm simply guesses a local TBox and then checks (using the polynomial-time algorithm for hybrid subsumption) whether it is a hybrid unifier.
To prove the proposition, we assume that T is a hybrid unifier of w.r.t. O. We use this unifier to define an assignment T as follows:
XT := fD 2 Atnv j X vgfp;O;T Dg: Let T 0 be the TBox induced by this assignment. To show that T 0 is indeed a hybrid unifier of w.r.t. O, we consider the set of GCIs
:= fC1 u : : : u Cm v D j C1; : : : ; Cm; D 2 Atg; and prove that, for any GCI C1 u : : : u Cm v D 2 , derivability of C1 u : : : u Cm v1 D in HC(O; T ; ) implies derivability of C1 u : : : u Cm v1 D also in HC(O; T 0; ). Soundness and completeness of HC, together with the facts that and T is a hybrid unifier of w.r.t. O, then imply that T 0 is also a hybrid unifier of w.r.t. O. Thus, to complete the proof of Proposition 8, it is enough to prove the following lemma.
Lemma 9. Let C1 u : : : u Cm v D 2 . If C1 u : : : u Cm v1 D is derivable in HC(O; T ; ), then C1 u : : : u Cm vn D is derivable in HC(O; T 0; ) for all n 0.
Proof. We prove derivability of C1 u: : :uCm vn D in HC(O; T 0; ) by induction on n. The base case is trivial due to the rule (Start).
Induction Step: We assume that the statement of the lemma holds for n
1, and show that it then also holds for n. Let ` be such that D`(O; T ; ) =
D1(O; T ; ). We know that there exists a proof tree P for C1 u : : : u Cm v` D
in HC(O; T ; ). Consider the subtree of P that is obtained from it by cutting
branches at the nodes obtained by an application of one of the rules (DefL) or
(DefR). The tree obtained this way contains only sequents with index ` and has
as its leaves
– instances of the rules (Refl), (Top), or (Start),
– consequences E1 v` E2 of instances of the rules (DefL) or (DefR).
In order to show that C1 u : : : u Cm vn D is derivable in HC(O; T 0; ), it is
sufficient to show that, for leaves E1 v` E2 of the second kind, E1 vn E2 is
derivable in HC(O; T 0; ) (see [
First, assume that E1 v` E2 was obtained by an application of (DefR). Then E2 2 Ndef . Assume that ET2 = fF1; : : : ; Fqg. By the definition of T , we have E2 vgfp;O;T Fi for all i; 1 i q. In addition, by our choice of `, derivability of E1 v` E2 in HC(O; T ; ) (using the subtree of P with this node as root) yields E1 vgfp;O;T E2, and thus E1 vgfp;O;T Fi for all i; 1 i q. Consequently, E1 v1 Fi is derivable in HC(O; T ; ) for all i; 1 i q. Since E1 is a conjunction of elements of At and F1; : : : ; Fq 2 At, induction yields that E1 vn 1 Fi is derivable in HC(O; T 0; ) for all i; 1 i q. Performing q 1 applications of (AndR) thus allows us to derive E1 vn 1 F1 u : : : u Fq in HC(O; T 0; ). Since T 0 contains the definition E2 F1 u : : : u Fq, an application of (DefR) shows that E1 vn E2 is derivable in HC(O; T 0; ).
Second, assume that E1 v` E2 was obtained by an application of (DefL). Then E1 2 Ndef and E2 = F1 u : : : u Fq for elements F1; : : : ; Fq of At. By our choice of ` we have E1 vgfp;O;T E2, and thus E1 vgfp;O;T Fi for all i; 1 i q. It is sufficient to show, for all i; 1 i q, that E1 vn Fi is derivable in HC(O; T 0; ) since q 1 applications of (AndR) then yield derivability of E1 vn E2 in HC(O; T 0; ).
If Fi does not belong to Ndef , then it is an element of Atnv. The definition of T thus yields Fi 2 ET1 . Consequently, Fi occurs as a conjunct on the righthand side of the definition of E1 in T 0. This implies E1 vgfp;O;T 0 Fi, and thus E1 vn Fi is derivable in HC(O; T 0; ).
If Fi 2 Ndef , then E1 vgfp;O;T Fi implies that FTi ET1 . Consequently, every conjunct on the right-hand side of the definition of Fi in T 0 is also a conjunct on the right-hand side of the definition of E1 in T 0. This implies E1 vgfp;O;T 0 Fi, and thus E1 vn Fi is derivable in HC(O; T 0; ). tu
This finishes the proof of Proposition 8, and thus shows that hybrid E Lunification w.r.t. arbitrary E L-ontologies is in NP. NP-hardness does not follow directly from NP-hardness of classical E L-unification. In fact, as we have seen in Example 6, an E L-unification problem that does not have a classical unifier may well have a hybrid unifier. Instead, we reduce E L-matching modulo equivalence to hybrid E L-unification.
Using the notions introduced in this paper, E L-matching modulo equivalence
can be defined as follows. An E L-matching problem modulo equivalence is an E
Lunification problem of the form fC v D; D v Cg such that D does not contain
elements of Ndef . A matcher of such a problem is a classical unifier of it. As
shown in [
Lemma 10. If an E L-matching problem modulo equivalence has a hybrid unifier w.r.t. the empty ontology, then it also has a matcher.
To sum up, we have thus determine the exact worst-case complexity of hybrid E L-unification.
Theorem 11. The problem of testing whether an E L-unification problem w.r.t. an arbitrary E L-ontology has a hybrid unifier or not is NP-complete. 5
In this paper, we have proved that hybrid E L-unification w.r.t. arbitrary E
Lontologies is in NP. The proof of NP-hardness of this problem as well as a more
practical goal-oriented algorithm for hybrid E L-unification that is better than
the brute-force “guess and then test” algorithm sketched above can be found in
[