Unification in the Description Logic $\mathcal {ELH}_{\mathcal {R}^+}$ Without the Top Concept Modulo Cycle-Restricted Ontologies

Abstract

Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL $\mathcal{E}\mathcal{L}$ is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.

1 Introduction

Description Logics (DLs) [10] are a prominent family of logic-based knowledge representation languages, which offer their users a good compromise between expressiveness and complexity of reasoning, and constitute the formal and algorithmic foundation of the standard Web Ontology Language OWL 2.¹ The DL $\mathcal{E}\mathcal{L}$, which provides the concept constructors conjunction ($\sqcap$), existential restriction ($\exists r.C$), and top concept ($\top$), is a rather inexpressive, but nevertheless very useful member of this family. On the one hand, the important reasoning problems, such as the subsumption and the equivalence problem, in $\mathcal{E}\mathcal{L}$ and some of its extensions are decidable in polynomial time [8, 22]. On the other hand, $\mathcal{E}\mathcal{L}$ and its tractable extensions are frequently used to define biomedical ontologies, such as the large medical ontology SNOMED CT.² To illustrate the use of the top concept, whose absence plays an important rôle in this paper, consider the $\mathcal{E}\mathcal{L}$ concept descriptions $Man \sqcap \exists child .\top$ and $Man \sqcap \exists child . Female$ of the concepts Father and Father of a daughter, respectively. In the former description, the top concept is used since no further properties of the child are to be required.

Unification in DLs has been introduced in [17] as a new inference service, motivated by the need for detecting redundancies in ontologies, in a setting where different ontology engineers (OEs) constructing the ontology may model the same concepts on different levels of granularity. For example, assume that (using the style of SNOMED CT definitions) one OE models the concept of a viral infection of the lung as

$$\begin{aligned} ViralInfection \sqcap \exists findingSite . LungStructure , \end{aligned}$$

whereas another one models it as

$$\begin{aligned} LungInfection \sqcap \exists causativeAgent . Virus . \end{aligned}$$

Here $ViralInfection$ and $LungInfection$ are used as atomic concepts without further defining them, i.e., the two OEs made different decisions when to stop the modelling process. The resulting concept descriptions are not equivalent, but they are nevertheless meant to represent the same concept. They can be made equivalent by treating the concept names $ViralInfection$ and $LungInfection$ as variables, and then substituting the first one by $Infection \sqcap \exists causativeAgent . Virus$ and the second one by $Infection \sqcap \exists findingSite . LungStructure$. In this case, we say that the descriptions are unifiable, and call the substitution that makes them equivalent a unifier. Intuitively, such a unifier proposes definitions for the concept names that are used as variables. In [7], unification and its extension to disunification are used to construct new medical concepts from SNOMED CT.

Unification in $\mathcal{E}\mathcal{L}$ was first investigated in [14], where it was proved that deciding unifiability is an NP-complete problem. The NP upper bound was shown in that paper using a brute-force “guess and then test” NP algorithm. More practical algorithms for solving this problem and for computing unifiers were presented in [16] and [15], where the former describes a goal-oriented transformation-based algorithm and the latter is based on a translation to SAT. Implementations of these two algorithms are provided by the system UEL³ [13], which is also available as a plug-in for the ontology editor Protégé. At the time these algorithms were developed, SNOMED CT was an $\mathcal{E}\mathcal{L}$ ontology consisting of acyclic concept definitions. Since such definitions can be encoded into the unification problem (see Sect. 2.3 in [16]), algorithms for unification of $\mathcal{E}\mathcal{L}$ concept descriptions (without background ontology) could be applied to SNOMED CT.

There was, however, one problem with employing these algorithms in the context of SNOMED CT: the top concept is not used in SNOMED CT, but the concepts generated by $\mathcal{E}\mathcal{L}$ unification might contain $\top$, even if applied to concept descriptions not containing $\top$. Thus, the concept descriptions produced by the unifier are not necessarily in the style of SNOMED CT. For example, assume that we are looking for a unifier satisfying the two subsumption constraints⁴

$$\begin{aligned} \exists findingSite . LungStructure \sqsubseteq ^?\exists findingSite .X,\\[.3em] \exists findingSite . HeartStructure \sqsubseteq ^?\exists findingSite .X. \end{aligned}$$

It is easy to see that there is only one unifier of these two constraints, which replaces X with $\top$. Unification in $\mathcal{E}\mathcal{L}^{-\!\top }$, i.e., the fragment of $\mathcal{E}\mathcal{L}$ in which the top constructor is disallowed, was investigated in [1, 18]. Surprisingly, it turned out that the absence of $\top$ makes unification considerably harder, both from a conceptual and a computational complexity point of view. In fact, the complexity of deciding unifiability increases from NP-complete for $\mathcal{E}\mathcal{L}$ to PSpace-complete for $\mathcal{E}\mathcal{L}^{-\!\top }$. The unification algorithm for $\mathcal{E}\mathcal{L}^{-\!\top }$ introduced in [1, 18] basically proceeds as follows. It first applies the unification algorithm for $\mathcal{E}\mathcal{L}$ to compute so-called local unifiers. If none of them is an $\mathcal{E}\mathcal{L}^{-\!\top }$-unifier, then it tries to augment the images of the variables by conjoining concept descriptions called particles. The task of finding appropriate particles is reduced to solving certain systems of linear language inclusions, which can be realized in PSpace using an automata-based approach.

The current version of SNOMED CT consists not only of acyclic concept definitions, but also contains more general concept inclusions (GCIs). In addition, properties of the part-of relation are no longer encoded using the so-called SEP-triplet encoding [27], but are directly expressed via role axioms [29], which can, for instance, be used to state that the part-of relation is transitive and that proper-part-of is a subrole of part-of. Decidability of unification in $\mathcal{E}\mathcal{L}$ w.r.t. a background ontology consisting of GCIs is still an open problem. In [2], it is shown that the problem remains in NP if the ontology is cycle-restricted, which is a condition that the current version of SNOMED CT satisfies. Extensions of this result to the DL $\mathcal {ELH}_{\mathcal {R}^+}$, which additionally allows for transitive roles and role inclusion axioms, were presented in [3, 5], where the former introduces a SAT-based algorithm and the latter a transformation-based one. However, in all these algorithms, unifiers may introduce concept descriptions containing $\top$. In our example with the different finding site, however, the presence of the GCIs $LungStructure \sqsubseteq UpperBodyStructure$ and $HeartStructure \sqsubseteq UpperBodyStructure$ would yield a unifier not using $\top$, namely the one that replaces X with $UpperBodyStructure$.

The purpose of this paper is to combine the approach for unification in $\mathcal{E}\mathcal{L}^{-\!\top }$ [1, 18] with the one for unification in $\mathcal {ELH}_{\mathcal {R}^+}$ w.r.t. cycle-restricted ontologies [2, 3, 5], to obtain a unification algorithm for $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$ w.r.t. cycle-restricted ontologies. This algorithm follows the line of the one for $\mathcal{E}\mathcal{L}^{-\!\top }$ in that it basically first generates $\mathcal {ELH}_{\mathcal {R}^+}$-unifiers, which it then tries to augment with particles. Appropriate particles are found as solutions of certain linear language inclusions. However, due to the presence of GCIs and role axioms, quite a number of non-trivial changes and additions are required. In particular, the solutions of the systems of linear language inclusions as constructed in [1, 18] cannot capture particles that are appropriate due to the presence of an ontology. For instance, in our example, $UpperBodyStructure$ would be such a particle. To repair this problem, we first need to show that, in $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$, unifiability w.r.t. a cycle-restricted ontology can be characterized by the existence of a special type of unifiers. Afterwards, we exploit the properties of this kind of unifiers to define more sophisticated systems of language inclusions, which encode the semantics of GCIs and role axioms occurring in a background ontology. The solutions of such systems then yield also particles that are appropriate only due to the presence of this ontology.

While the unification problem investigated in this paper is motivated by an application in ontology engineering, it is also of interest for unification theory [19], which is concerned with unification-related properties of equational theories. In fact, unification in DLs can be seen as a special case of unification modulo equational theories, where the respective equational theory axiomatizes equivalence in the DL under consideration. For $\mathcal{E}\mathcal{L}$ and $\mathcal {ELH}_{\mathcal {R}^+}$, the corresponding equational theories can be found in [28]. The ones for the case without top can be obtained from them by removing the constant 1 from the signature, and all identities containing it from the axiomatization. The results in [1, 18] and in the present paper show that the seemingly harmless removal of a constant from the equational theory may increase the complexity of the unification problem considerably. Considering unification w.r.t. a background ontology corresponds to adding a finite set of ground identities to the corresponding equational theory. For the word problem, it was shown that decidability is stable under adding finite sets of ground identities to theories such as commutativity or associativity-commutativity [11, 20, 24, 25]. For unification, it was shown in [12] that adding finite sets of ground identities to the theory $ACUI$ of an associativity-commutativity-idempotent symbol with a unit leaves the unification problem decidable. The results in [2, 3, 5] can be seen as such transfer results, but they require a restriction on the ground identities corresponding to cycle-restrictedness.

Due to space constraints, we cannot give detailed proof of our results here. They can be found in [9].

2 Subsumption and Unification in $\mathcal {ELH}_{\mathcal {R}^+}$ and $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$

First, we briefly introduce syntax and semantics of the DLs investigated in this paper. Then, we recall a useful characterization of subsumption for these logics, and finally define the unification problem.

2.1 The DLs $\mathcal {ELH}_{\mathcal {R}^+}$ and $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$

Starting with countably infinite sets $\mathsf {N_C}$ and $\mathsf {N_R}$ of concept names and role names, $\mathcal {ELH}_{\mathcal {R}^+}$-concept descriptions (for short, concepts) are built using the concept constructors conjunction ($\sqcap$), existential restriction ($\exists r.C$), and top ($\top$). When building $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-concepts, the constructor $\top$ is not available. An $\mathcal {ELH}_{\mathcal {R}^+}$-ontology $\mathcal {O}$ is a finite set of general concept inclusions (GCIs) $C \sqsubseteq D$, role hierarchy axioms $r \sqsubseteq s$, and transitivity axioms $r \circ r \sqsubseteq r$, where C, D are $\mathcal {ELH}_{\mathcal {R}^+}$-concepts and r, s are role names. In an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology, the concepts occurring in GCIs must be $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-concepts.

The following two notions will play an important rôle in our unification algorithm. An atom is either a concept name or an existential restriction, and a particle is an atom of the form $\exists r_1.\exists r_2.\cdots \exists r_n.A$ for a concept name A, which we write as $\exists w.A$, where $w= r_1\ldots r_n$ is viewed as a word over the alphabet $\mathsf {N_R}$. Every $\mathcal {ELH}_{\mathcal {R}^+}$-concept C is a conjunction of atoms, where the empty conjunction represents $\top$. These atoms are called the top-level atoms of C. The set $Ats (C)$ consists of all atoms (not just top-level ones) occurring in C, and $Ats (\mathcal {O})$ for an ontology $\mathcal {O}$ consists of the atoms of all concepts occurring in $\mathcal {O}$. The set of particles of an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-concept is defined inductively: $Part (A) := \{A\}$ for each concept name A, $Part (\exists r.C) := \{\exists r.P \mid P \in Part (C)\}$, and $Part (C\sqcap D) := Part (C) \cup Part (D)$. For example, if $C = \exists r.(\exists s.A\sqcap \exists r.B)$, then $Part (C) = \{\exists rs.A,\exists rr.B\}$ and $Ats (C) = \{C, \exists s.A,\exists r.B, A, B\}$, where C is the only top-level atom.

The semantics of $\mathcal {ELH}_{\mathcal {R}^+}$-concepts and ontologies is defined using the notion of an interpretation $\mathcal {I}= (\varDelta ^\mathcal {I}, .^\mathcal {I})$, which has a set $\varDelta ^\mathcal {I}\ne \emptyset$ as interpretation domain, and assigns a subset $A^\mathcal {I}\subseteq \varDelta ^\mathcal {I}$ to each concept name A and a binary relation $r^\mathcal {I}\subseteq \varDelta ^\mathcal {I}\times \varDelta ^\mathcal {I}$ to each role name r. The interpretation function $.^\mathcal {I}$ is extended to $\mathcal {ELH}_{\mathcal {R}^+}$-concepts as usual: $\top ^\mathcal {I}:= \varDelta ^\mathcal {I}$, $(C \sqcap D)^\mathcal {I}:= C^\mathcal {I}\cap D^\mathcal {I}$, and $(\exists r.C)^\mathcal {I}:= \{d \in \varDelta ^\mathcal {I}\mid \exists e.((d,e) \in r^\mathcal {I}\wedge e \in C^\mathcal {I})\}$. The interpretation $\mathcal {I}$ is a model of the $\mathcal {ELH}_{\mathcal {R}^+}$-ontology $\mathcal {O}$ if ${C \sqsubseteq D}\in \mathcal {O}$ implies $C^\mathcal {I}\subseteq D^\mathcal {I}$, ${r \sqsubseteq s}\in \mathcal {O}$ implies $r^\mathcal {I}\subseteq s^\mathcal {I}$, and ${r \circ r \sqsubseteq r}\in \mathcal {O}$ implies that $r^\mathcal {I}$ is transitive.

2.2 Subsumption in $\mathcal {ELH}_{\mathcal {R}^+}$ and $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$

Given an $\mathcal {ELH}_{\mathcal {R}^+}$-ontology $\mathcal {O}$ and $\mathcal {ELH}_{\mathcal {R}^+}$-concepts C, D, we say that C is subsumed by D w.r.t. $\mathcal {O}$ (written $C\sqsubseteq _\mathcal {O}D$) if $C^\mathcal {I}\subseteq D^\mathcal {I}$ for all models $\mathcal {I}$ of $\mathcal {O}$. They are equivalent w.r.t. $\mathcal {O}$ (written $C \equiv _\mathcal {O}D$) if $C\sqsubseteq _\mathcal {O}D$ and $D\sqsubseteq _\mathcal {O}C$.

Subsumption (and thus also equivalence) between $\mathcal {ELH}_{\mathcal {R}^+}$-concepts w.r.t. arbitrary $\mathcal {ELH}_{\mathcal {R}^+}$-ontologies can be decided in polynomial time [8]. In the context of unification, a recursive characterization of subsumption turns out to be useful, which for $\mathcal {ELH}_{\mathcal {R}^+}$ was first given in [5], and later reformulated in [3]. In this paper we use the one given in [3], but before we can formulate this characterization, we must introduce the role hierarchy induced by an $\mathcal {ELH}_{\mathcal {R}^+}$-ontology $\mathcal {O}$: given role names r, s, we say that r is a subrole of s (written $r \trianglelefteq _\mathcal {O}s$) if $r^\mathcal {I}\subseteq s^\mathcal {I}$ holds for all models $\mathcal {I}$ of $\mathcal {O}$. It is easy to see that the relation $\trianglelefteq _\mathcal {O}$ is the reflexive-transitive closure of the explicitly stated subrole relationships $\{(r,s) \mid r\sqsubseteq s \in \mathcal {O}\}$. We call a role name r transitive if ${r \circ r \sqsubseteq r}\in \mathcal {O}$.

The characterization of subsumption in [3] uses the notion of structural subsumption: given atoms C, D, we say that C is structurally subsumed by D w.r.t. an $\mathcal {ELH}_{\mathcal {R}^+}$-ontology $\mathcal {O}$ (written $C \mathbin {\sqsubseteq ^s_{\mathcal {O}}} D$) if one of the following cases applies:

• 1. $C = D$ is a concept name.

• 2. $C= \exists r.C'$, $D = \exists s.D'$, $r \trianglelefteq _\mathcal {O}s$, and $C' \sqsubseteq _\mathcal {O}D'$.

• 3. $C = \exists r.C'$, $D = \exists s.D'$, and $C' \sqsubseteq _\mathcal {O}\exists t.D'$ for some transitive role name t satisfying $r \trianglelefteq _\mathcal {O}t \trianglelefteq _\mathcal {O}s$.

Lemma 1

[3]. Let $\mathcal {O}$ be an $\mathcal {ELH}_{\mathcal {R}^+}$-ontology and $C_1,\ldots ,C_n,D_1,\ldots ,D_m$ atoms. Then, $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq _\mathcal {O}D_1 \sqcap \cdots \sqcap D_m$ iff for every $j \in \{1,\ldots ,m\}$:

• 1. there is an index $i \in \{1,\ldots ,n\}$ such that $C_i \mathbin {\sqsubseteq ^s_{\mathcal {O}}} D_j$, or

• 2. there are atoms $At _1,\ldots , At _k, At '$ of $\mathcal {O}$ ($k \ge 0$) such that:

  • (a) $At _1 \sqcap \cdots \sqcap At _k \sqsubseteq _\mathcal {O} At '$,

  • (b) for every $\ell \in \{1,\ldots ,k\}$ there exists $i \in \{1,\ldots ,n\}$ with $C_i \mathbin {\sqsubseteq ^s_{\mathcal {O}}} At _\ell$, and

  • (c) $At ' \mathbin {\sqsubseteq ^s_{\mathcal {O}}} D_j$.

If $\mathcal {O}$ is empty, then the second case in the definition of structural subsumption can be modified to require that $r=s$ and $C' \sqsubseteq _\emptyset D'$, whereas the third case in the same definition as well as the second case in Lemma 1 can be removed. This then yields the characterization of subsumption in $\mathcal{E}\mathcal{L}$ of [16]. Since $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$ is a fragment of $\mathcal {ELH}_{\mathcal {R}^+}$, this characterization also applies to subsumption between $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-concepts w.r.t. $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontologies. However, in this setting, the case $k=0$ in cannot occur. This is a direct consequence of the following result.

Lemma 2

If $\mathcal {O}$ is an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology and $At$ an atom of $\mathcal {O}$, then $\top \not \sqsubseteq _\mathcal {O} At$.

2.3 Unification in $\mathcal {ELH}_{\mathcal {R}^+}$ and $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$

When defining unification, we assume that the set of concept names is partitioned into a set $\mathsf {N_C}$ of concept constants and a set $\mathsf {N_V}$ of concept variables. Given a DL $\mathcal {L}\in \{\mathcal {ELH}_{\mathcal {R}^+},\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}\}$, an $\mathcal {L}$-substitution $\sigma$ is a mapping from a finite subset of $\mathsf {N_V}$ to the set of $\mathcal {L}$-concepts. The application of $\sigma$ to an arbitrary $\mathcal {L}$-concept is defined inductively in the usual way. A concept (ontology) is ground if it does not contain variables. A substitution $\sigma$ is ground if $\sigma (X)$ is ground for all variables X that have an image under $\sigma$.

Definition 1

Let $\mathcal {O}$ be a ground ontology. An $\mathcal {L}$-unification problem w.r.t. $\mathcal {O}$ is of the form $\varGamma = \{C_1 \sqsubseteq ^? D_1,\ldots ,C_n \sqsubseteq ^? D_n\}$, where $C_1,D_1,\ldots ,C_n, D_n$ are $\mathcal {L}$-concepts. An $\mathcal {L}$-substitution $\sigma$ is an $\mathcal {L}$-unifier of $\varGamma$ w.r.t. $\mathcal {O}$ if $\sigma (C_i)\sqsubseteq _\mathcal {O}\sigma (D_i)$ for all $i \in \{1,\ldots ,n\}$. The unification problem $\varGamma$ is called $\mathcal {L}$-unifiable w.r.t. $\mathcal {O}$ if it has an $\mathcal {L}$-unifier w.r.t. $\mathcal {O}$.

The following example illustrates that unifiability of a given unification problem may depend on the considered DL $\mathcal {L}$ and on the presence of a non-empty ontology.

Example 1

Let $\mathcal {O}= \emptyset$ and consider the following unification problem:

$$\begin{aligned} \varGamma _1 := \{\exists r.A \sqsubseteq ^? X,\ \ \exists u.B \sqsubseteq ^? Y,\ \ \exists s.X \sqcap A \sqsubseteq ^? Y\}. \end{aligned}$$

Viewed as an $\mathcal {ELH}_{\mathcal {R}^+}$-unification problem, it has the unifier $\sigma$ with $\sigma (X) = \sigma (Y) = \top$. However, $\varGamma _1$ does not have an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}= \emptyset$. To see this, suppose that $\delta$ is such a unifier. Using Lemma 1 for the special case of an empty ontology, we can deduce from $\exists u.B \sqsubseteq _\emptyset \delta (Y)$ that every top-level atom of $\delta (Y)$ is an existential restriction for the role u. However, we can also deduce from $\exists s.\delta (X) \sqcap A \sqsubseteq _\emptyset \delta (Y)$ that every top-level atom of $\delta (Y)$ is either A or an existential restriction for the role s. Since not both is possible, $\delta (Y)$ cannot have any top-level atoms, and thus must be $\top$, contradicting our assumption that $\delta$ is an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier. If we define $\mathcal {O}' := \{B \sqsubseteq \exists r.A,\ u \sqsubseteq s\}$, then the $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifiability status of $\varGamma _1$ changes to unifiable since $\delta$ with $\delta (X) = \exists r.A$ and $\delta (Y) = \exists s.\exists r.A$ is an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier of $\varGamma _1$ w.r.t. $\mathcal {O}'$.

In the next section we will show how to decide unifiability of an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problem w.r.t. a cycle-restricted $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology.

Definition 2

An $\mathcal {ELH}_{\mathcal {R}^+}$-ontology $\mathcal {O}$ is called cycle-restricted if there is no sequence of $n > 0$ role names $r_1,\ldots ,r_n \in \mathsf {N_R}$ and $\mathcal {ELH}_{\mathcal {R}^+}$-concept C such that $C \sqsubseteq _\mathcal {O}\exists r_1.\exists r_2.\cdots \exists r_n.C$.

As stated in [5] (and proved in [6]), one can test in polynomial time whether a given $\mathcal {ELH}_{\mathcal {R}^+}$-ontology is cycle-restricted or not.

According to [5, 18], we can without loss of generality assume that the given ontology and the unification problem are flat. An $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-atom is flat if it is a concept name or of the form $\exists r.A$ for a concept name A. A GCI $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq D$ or subsumption constraint $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq ^? D$ is flat if $C_1,\ldots ,C_n$ and D are flat $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-atoms. Finally, an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology or $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problem is flat if all it elements are flat.

The following result for flat, cycle-restricted $\mathcal {ELH}_{\mathcal {R}^+}$-ontologies will turn out to be quite useful in the next section. It basically follows from the proof of Lemma 8 in [4].

Lemma 3

Let $\mathcal {O}$ be a flat, cycle-restricted $\mathcal {ELH}_{\mathcal {R}^+}$-ontology, $A \in \mathsf {N_C}$ and $\exists r.C$ an $\mathcal {ELH}_{\mathcal {R}^+}$-atom. Then, $A \sqsubseteq _\mathcal {O}\exists r.C$ iff there exists $\exists u.B \in Ats (\mathcal {O})$ such that $B \sqsubseteq _\mathcal {O}C$, and

• $A \sqsubseteq _\mathcal {O}\exists u.B$ and $u \trianglelefteq _\mathcal {O}r$, or

• $A \sqsubseteq _\mathcal {O}\exists t.B$ for a transitive role t with $u \trianglelefteq _\mathcal {O}t \trianglelefteq _\mathcal {O}r$.

3 The Unification Algorithm for $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$

In the following, we assume that $\mathcal {O}$ is a flat and cycle-restricted $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology and $\varGamma$ is a flat $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problem. We introduce an algorithm that can test whether $\varGamma$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier and needs only polynomial space for this task. This algorithm follows the approach developed in [18] for unification in $\mathcal{E}\mathcal{L}^{-\!\top }$, but must take the ontology into account, which means that it must deal with a considerably more complex characterization of subsumption (see Lemma 1 and our remarks on how the characterization can be simplified if $\mathcal {O}= \emptyset$).

Before presenting our new approach, we briefly sketch the one employed in [18]. The original NP procedure for unification in $\mathcal{E}\mathcal{L}$ [16] is based on the (non-trivial) observation that an $\mathcal{E}\mathcal{L}$-unification problem $\varGamma$ has a unifier iff it has a local unifier, i.e., one that is built using only atoms occurring in the unification problem. The procedure guesses an appropriate representation of a local substitution, and then checks by $\mathcal{E}\mathcal{L}$ reasoning whether it really is a unifier. Basically, to guess a local substitution $\sigma$, one must guess for every variable X and non-variable atom C of $\varGamma$ whether $\sigma (X)\sqsubseteq _\emptyset \sigma (C)$ is supposed to hold. A subsumption mapping $\tau$ describing a local unifier $\sigma$ more generally guesses for every pair C, D of atoms whether $\sigma (C)\sqsubseteq _\emptyset \sigma (D)$ is supposed to hold. The restrictions imposed on such subsumption mappings ensure that the local substitution induced by such a mapping is indeed an $\mathcal{E}\mathcal{L}$-unifier of $\varGamma$ [18], i.e., the subsequent $\mathcal{E}\mathcal{L}$ reasoning testing this can be dispensed with. The local unifier obtained from a subsumption mapping $\tau$ need not be an $\mathcal{E}\mathcal{L}^{-\!\top }$-unifier. To test for the existence of an $\mathcal{E}\mathcal{L}^{-\!\top }$-unifier related to $\tau$, the subsumption mapping $\tau$ together with the original unification problem $\varGamma$ is then used to construct a new unification problem $\varDelta _{\varGamma ,\tau }$, in which only variables can occur on the right-hand side of subsumption constraints. Existence of an $\mathcal{E}\mathcal{L}^{-\!\top }$-unifier of $\varDelta _{\varGamma ,\tau }$ that is compatible with $\tau$ is then reduced in [18] to the existence of an admissible solution of a corresponding set $\mathfrak {I}_{\varGamma ,\tau }$ of linear language inclusions. The latter problem can in turn be reduced in polynomial time to checking emptiness of alternating finite automata with $\varepsilon$-transitions [18], which is a PSpace-complete problem [23].

In this section we show how this approach can be extended from $\mathcal{E}\mathcal{L}^{-\!\top }$ to $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$ w.r.t. cycle-restricted ontologies. We start by introducing subsumption mappings and the induced unification problems of the form $\varDelta _{\varGamma ,\tau }$.

3.1 The Subsumption Mapping

Let $Ats (\varGamma ,\mathcal {O})$ be the set of atoms occurring in $\varGamma$ or $\mathcal {O}$. Due to the third case in the definition of structural subsumption, we also need to consider certain atoms that are not explicitly present in the input:

$$\begin{aligned} Ats_{tr} (\varGamma ,\mathcal {O}) := Ats (\varGamma ,\mathcal {O}) \cup \{\exists t.C \mid \exists s.C \in Ats (\varGamma ,\mathcal {O}),\ t \trianglelefteq _\mathcal {O}s,\ t \text { is transitive}\}. \end{aligned}$$

A non-variable atom is an atom in $Ats_{tr} (\varGamma ,\mathcal {O})$ that is not a variable. We denote the set of all such atoms as $At_{nv} (\varGamma ,\mathcal {O})$. A mapping of the form $\tau : Ats_{tr} (\varGamma ,\mathcal {O}) \times Ats_{tr} (\varGamma ,\mathcal {O}) \rightarrow \{0,1\}$ induces an assignment $S^\tau$ that maps variables in $\varGamma$ to sets of non-variable atoms in $Ats_{tr} (\varGamma ,\mathcal {O})$:

$$\begin{aligned} S^\tau (X) := \{D \in At_{nv} (\varGamma ,\mathcal {O}) \mid \tau (X,D)=1\}. \end{aligned}$$

This assignment induces the relation

$$\begin{aligned} >_{S^\tau }:= \{(X,Y) \in Vars (\varGamma )\times Vars (\varGamma ) \mid Y \text { occurs in an atom of }S^\tau (X)\}. \end{aligned}$$

We say that $S^\tau$ is acyclic if the transitive closure of $>_{S^\tau }$ is irreflexive, and thus a strict partial order, which we denote as $>_{\tau }$. If $S^\tau$ is acyclic, then it induces a substitution $\sigma _\tau$, defined by induction on $>_{\tau }$:

• If X is minimal w.r.t. $>_{\tau }$, then $\sigma _\tau (X) := \sqcap _{D \in S^\tau (X)} D$.

• Otherwise, assuming that $\sigma _\tau (Y)$ has already been defined for all Y such that $X >_{\tau } Y$, one defines $\sigma _\tau (X):=\sqcap _{D\in S^\tau (X)} \sigma _\tau (D)$.

The conditions imposed on a subsumption mapping $\tau$ ensure that the induced substitution $\sigma _\tau$ is an $\mathcal {ELH}_{\mathcal {R}^+}$-unifier of $\varGamma$. In order to simplify the definition of these conditions, we introduce the following notation (for atoms $\exists r.C, \exists s.D$):

$$\begin{aligned} \mathcal {F}(\exists r.C,\exists s.D) := \{D \mid \text {if } r\trianglelefteq _\mathcal {O}s\} \cup \{\exists t.D \mid r \trianglelefteq _\mathcal {O}t \trianglelefteq _\mathcal {O}s,\ t \text { transitive}\}. \end{aligned}$$

Basically, this set collects all concepts F such that $C \sqsubseteq _\mathcal {O}F$ implies $\exists r.C \mathbin {\sqsubseteq ^s_{\mathcal {O}}} \exists s.D$ (see the second and third case in the definition of $\mathbin {\sqsubseteq ^s_{\mathcal {O}}}$).

Definition 3

The mapping $\tau : Ats_{tr} (\varGamma , \mathcal {O}) \times Ats_{tr} (\varGamma ,\mathcal {O}) \rightarrow \{0,1\}$ is called a subsumption mapping for $\varGamma$ w.r.t. $\mathcal {O}$ if it satisfies the following conditions:

• 1. It respects the properties of subsumption w.r.t. $\mathcal {O}$:

  • (a) $\tau (D,D) = 1$, for each $D \in Ats_{tr} (\varGamma , \mathcal {O})$.

  • (b) For all $D_1,D_2,D_3 \in Ats_{tr} (\varGamma ,\mathcal {O})$, if $\tau (D_1,D_2)= \tau (D_2,D_3)=1$ then $\tau (D_1,D_3)=1$.

  • (c) $\tau (C,D) = 1$ iff $C \sqsubseteq _\mathcal {O}D$, for all ground atoms $C, D \in Ats_{tr} (\varGamma , \mathcal {O})$.

  • (d) For each concept constant $A \in Ats (\varGamma ,\mathcal {O})$, role name r, and variable X with $\exists r.X \in Ats_{tr} (\varGamma )$:

    • i. $\tau (A,\exists r.X)=1$ iff ⁵ there is an atom $\exists u.B$ of $\mathcal {O}$ such that $\tau (B,X)=1$, and

      • $A \sqsubseteq _\mathcal {O}\exists u.B$ and $u \trianglelefteq _\mathcal {O}r$, or

      • $A \sqsubseteq _\mathcal {O}\exists t.B$ for a transitive role t with $u \trianglelefteq _\mathcal {O}t \trianglelefteq _\mathcal {O}r$.

    • ii. $\tau (\exists r.X,A)=1$ iff

      • there are atoms $\exists r_1.A_1,\ldots ,\exists r_k.A_k$ of $\mathcal {O}$ ($k \ge 0$) and atoms $F_\ell \in \mathcal {F}(\exists r.X,\exists r_\ell .A_\ell )$ ($1 \le \ell \le k$) such that: $\tau (X,F_\ell )=1 \, (1 \le \ell \le k)\ \text { and }\ \exists r_1.A_1 \sqcap \cdots \sqcap \exists r_k.A_k \sqsubseteq _\mathcal {O}A.$

  • (e) For all role names $r, s \in \mathsf {N_R}$, variables X, and atoms $\exists r.C, \exists s.D \in Ats_{tr} (\varGamma )$ with $C=X$ or $D=X$: $\tau (\exists r.C,\exists s.D)=1$ iff

    • there exists $F\in \mathcal {F}(\exists r.C,\exists s.D)$ such that $\tau (C,F)=1$, or

    • there are atoms $\exists r_1.A_1,\ldots ,\exists r_k.A_k, \exists u.B$ of $\mathcal {O}$ ($k \ge 0$), atoms $F_\ell \in \mathcal {F}(\exists r.C,\exists r_\ell .A_\ell )$ ($1 \le \ell \le k$), and an atom $F \in \mathcal {F}(\exists u.B,\exists s.D)$, such that: $\tau (C,F_\ell )=1 \, (1 \le \ell \le k),\ \ \exists r_1.A_1 \sqcap \cdots \sqcap \exists r_k.A_k \sqsubseteq _\mathcal {O}\exists u.B,\ \ \tau (B,F)=1.$

• 2. The assignment $S^\tau$ is acyclic. Note that this means that $\tau$ induces the $\mathcal {ELH}_{\mathcal {R}^+}$-substitution $\sigma ^\tau$.

• 3. The substitution $\sigma ^\tau$ is an $\mathcal {ELH}_{\mathcal {R}^+}$-unifier of $\varGamma$ w.r.t. $\mathcal {O}$. In combination with the conditions already introduced, this is expressed by the following conditions for each subsumption constraint $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq ^? D \in \varGamma$:

  • (a) If D is a non-variable atom, then either $\tau (C_i,D)=1$ for some $i \in \{1,\ldots ,n\}$, or there are atoms $At _1,\ldots , At _k, At '$ of $\mathcal {O}$ ($k \ge 0$) such that:

    • $At _1 \sqcap \cdots \sqcap At _k \sqsubseteq _\mathcal {O} At '$,

    • for each $\ell \in \{1,\ldots ,k\}$ there is $i \in \{1,\ldots ,n\}$ s.t. $\tau (C_i, At _\ell )=1$, and

    • $\tau ( At ',D)=1$.

  • (b) If D is a variable and $\tau (D,C)=1$ for a non-variable atom $C\in At_{nv} (\varGamma ,\mathcal {O})$, then $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq ^? C$ must satisfy the previous case.

By using the close relationship between this definition and the characterization of subsumption in Lemma 1, one can show that $\varGamma$ has an $\mathcal {ELH}_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}$ iff there is a subsumption mapping for $\varGamma$ w.r.t. $\mathcal {O}$. In the proof of the if-direction, one shows that the substitution induced by the subsumption mapping is indeed a unifier. For the other direction, one takes a unifier $\sigma$ and shows that the mapping $\tau$ satisfying $\tau (C,D) = 1$ iff $\sigma (C)\sqsubseteq _\mathcal {O}\sigma (D)$ is a subsumption mapping for $\varGamma$ w.r.t. $\mathcal {O}$.

However, using subsumption mappings to characterize unifiability in $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$ requires more effort. Together with the unification problem $\varGamma$, a subsumption mapping $\tau$ yields a simpler unification problem $\varDelta _{\varGamma ,\tau }:=\varDelta _{\varGamma }\cup \varDelta _{\tau }$, where

$$ \varDelta _{\varGamma }:= \{C_1 \sqcap \cdots \sqcap C_n \sqsubseteq ^? X \in \varGamma \mid X\in \mathsf {N_V}\}\ \ \text { and } \ \ \varDelta _{\tau }:= \{C \sqsubseteq ^? X \mid \tau (C,X)=1\}. $$

In addition, any substitution $\sigma$ induces an assignment $S^\sigma$ of the form:

$$\begin{aligned} S^\sigma (X) := \{D \in At_{nv} (\varGamma ,\mathcal {O}) \mid \sigma (X) \sqsubseteq _\mathcal {O}\sigma (D)\}. \end{aligned}$$

We write $S^\tau \le S^\sigma$ if $S^\tau (X) \subseteq S^\sigma (X)$ holds for all variables X. In this case we say that $\sigma$ is compatible with $\tau$.

The following result gives a characterization of the existence of an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology.

Proposition 1

Let $\mathcal {O}$ be a flat and cycle-restricted $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology and $\varGamma$ a flat $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problem. Then, $\varGamma$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}$ iff there exists a subsumption mapping $\tau$ for $\varGamma$ w.r.t. $\mathcal {O}$ such that $\varDelta _{\varGamma ,\tau }$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier $\gamma$ w.r.t. $\mathcal {O}$ that is compatible with $\tau$.

Example 2

Let $\mathcal {O}= \emptyset$ and consider the following unification problem:

$$\begin{aligned} \varGamma _2 := \{\exists r.B \sqsubseteq ^? \exists r.Y,\ \ \exists s.X \sqcap \exists r.A \sqsubseteq ^? Y\}. \end{aligned}$$

Due to Condition 3 in Definition 3 and the fact that $\mathcal {O}$ is empty, any subsumption mapping $\tau$ must satisfy $\tau (\exists r.B,\exists r.Y) = 1$. Condition 1e then implies that $\tau (B,Y) = 1$ must hold as well. We can conclude that, for any subsumption mapping $\tau$, the set $\varDelta _{\varGamma _2,\tau }$ contains at least the subsumption constraints $B\sqsubseteq ^? Y$ and $\exists s.X \sqcap \exists r.A \sqsubseteq ^? Y$. Using an argument similar to the one employed in Example 1, one can show that such a set $\varDelta _{\varGamma _2,\tau }$ cannot have an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\emptyset$.

Definition 3 also tells us that Condition 3b does not apply to the constraints $B\sqsubseteq ^? Y$ and $\exists s.X \sqcap \exists r.A \sqsubseteq ^? Y$ as long as there is no non-variable atom C with $\tau (Y,C) = 1$. Hence, it is easy to see that there also is a subsumption mapping $\tau$ that has only these two constraints in $\varDelta _{\varGamma _2,\tau }$ since the only other mandatory values 1 are the ones required by 1a. For the ontology $\mathcal {O}'' = \{B \sqsubseteq \exists r.A\}$, the set $\varDelta _{\varGamma _2,\tau }$ then has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}''$, which maps Y to $\exists r.A$. This unifier is compatible with $\tau$ since the subsumption mapping $\tau$ that yields value 1 only if required satisfies $S^\tau (X) = S^\tau (Y) = \emptyset$. Thus, by Lemma 1, $\varGamma _2$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}''$. Note that this unifier is not $\sigma _\tau$ since $\sigma _\tau$ in this case assigns $\top$ to X and Y.

3.2 Translation into Language Inclusions

Linear language inclusions are a special case of the linear language equations considered in [17] in the context of unification in the DL $\mathcal{F}\mathcal{L}_0$. In contrast to the general case, where solvability is an ExpTime-complete problem [17], the linear language inclusions introduced in [18] in the context of unification in $\mathcal{E}\mathcal{L}^{-\!\top }$ have a PSpace-complete solvability problem [18].

Definition 4

Let $X_1,\ldots ,X_n$ be a finite set of indeterminates. A linear language inclusion over this set of indeterminates and the alphabet $\mathsf {N_R}$ is an expression of the form

$$\begin{aligned} X_i \subseteq L_0 \cup L_1X_1 \cup \cdots \cup L_n X_n, \end{aligned}$$

where $i \in \{1,\ldots ,n\}$ and each $L_j \subseteq \{\varepsilon \} \cup \mathsf {N_R}$ ($0 \le j \le n$). As usual, the symbol $\varepsilon$ denotes the empty word. A solution $\theta$ of such an inclusion assigns sets of words $\theta (X_i) \subseteq \mathsf {N_R}^*$ to each indeterminate $X_i$ such that $\theta (X_i) \subseteq L_0 \cup L_1{\cdot }\theta (X_1) \cup \cdots \cup L_n {\cdot }\theta (X_n),$ where “${\cdot }$” denotes concatenation of languages. The solution $\theta$ is finite if $\theta (X_i)$ is a finite set for all $i \in \{1,\ldots ,n\}$.

Checking whether $\varDelta _{\varGamma ,\tau }$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}$ that is compatible with a given subsumption mapping $\tau$ can be reduced to solving a system $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ of such linear language inclusion. The basic idea is that, for each concept variable X and concept constant A, we introduce an indeterminate $X_A$. Intuitively, the system $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ is constructed such that the following holds:

• if $\gamma$ is an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier of $\varDelta _{\varGamma ,\tau }$ compatible with $\tau$, then there is an assignment $\theta _\gamma$ satisfying $\theta _\gamma (X_A) = \{w \mid \exists w.A \in Part (\gamma (X))\}$ that is a finite solution of the system $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$.

Since $\gamma$ is an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier, of which we can assume without loss of generality that it is ground [19], the solution $\theta _\gamma$ satisfies an additional property: for every variable X there is a concept constant A such that $\theta _\gamma (X_A)\ne \emptyset$. We call a solution of $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ satisfying this property admissible. Conversely, finite, admissible solutions of $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ yield an appropriate unifier of $\varDelta _{\varGamma ,\tau }$:

• if $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ has a finite, admissible solution, then it has such a solution $\theta$ that yields an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier $\gamma _\theta$ of $\varDelta _{\varGamma ,\tau }$ that is compatible with $\tau$. This unifier is defined similarly to $\sigma _\tau$, but using particles provided by $\theta$ for padding:

  • if X is minimal w.r.t. $>_{\tau }$, then

    $$\begin{aligned} \gamma _\theta (X) := \sqcap _{D \in S^\tau (X)} D \sqcap \sqcap _{A \in \mathsf {N_C}}\sqcap _{w \in \theta (X_A)} \exists w.A, \end{aligned}$$

  • if $\gamma _\theta (Y)$ has already been defined for all Y such that $X >_{\tau } Y$, then

    $$\begin{aligned} \gamma _\theta (X) := \sqcap _{D\in S^\tau (X)} \gamma _\theta (D) \sqcap \sqcap _{A \in \mathsf {N_C}} \sqcap _{w \in \theta (X_A)} \exists w.A. \end{aligned}$$

Basically, to define the linear language inclusions in $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$, we consider the following situation: given a particle $\exists w.A\in Part (\gamma (X))$ and a constraint $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq ^? X \in \varDelta _{\varGamma ,\tau }$, we know (by Lemma 2 in [18]) that $\gamma (C_1) \sqcap \cdots \sqcap \gamma (C_n) \sqsubseteq _\mathcal {O}\exists w.A$ holds. Hence, the idea is to encode, within the inclusions in $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$, whether a conjunction of atoms and a particle satisfy the characterization of subsumption in Lemma 1.

For the case of an empty ontology, the construction of the system $\mathfrak {I}_{\varGamma ,\tau }^{\emptyset }$ is relatively straightforward since the characterization of subsumption is quite simple in this case. As described in [18], for each concept constant $A \in \mathsf {N_C}$ and each subsumption constraint $\mathfrak {s}= C_1\sqcap \cdots \sqcap C_n \sqsubseteq ^? X$ in $\varDelta _{\varGamma ,\tau }$, a linear inclusion $\mathfrak {i}_{A}(\mathfrak {s})$ of the following form is added to $\mathfrak {I}_{\varGamma ,\tau }^{\emptyset }$:

$$ X_A \subseteq f_{A}(C_1) \cup \cdots \cup f_{A}(C_n),\ \text { where } f_{A}(C) := {\left\{ \begin{array}{ll} \{r\} f_{A}(C') &{} \text {if } C = \exists r.C',\\[.3em] Y_A &{} \text {if } C = Y \in \mathsf {N_V},\\[.3em] \{\varepsilon \} &{} \text {if } C=A,\\[.3em] \emptyset &{} \text {if } C \in \mathsf {N_C}\setminus \{A\}. \end{array}\right. } $$

Example 3

Consider the system $\varDelta _{\varGamma _2,\tau } = \{B\sqsubseteq ^? Y, \exists s.X \sqcap \exists r.A \sqsubseteq ^? Y, \ldots \}$ from Example 2. The first subsumption constraint yields the language inclusions $Y_A \subseteq \emptyset$ and $Y_B\subseteq \{\varepsilon \}$, and the second yields $Y_A \subseteq \{s\}X_A\cup \{r\}\{\varepsilon \}$ and $Y_B\subseteq \{s\}X_B\cup \{r\}\emptyset$. There are no language inclusions constraining $X_A$ or $X_B$. Any solution $\theta$ of $\mathfrak {I}_{\varGamma _2,\tau }^\emptyset$ thus must satisfy $\theta (Y_A) = \emptyset$. If $\theta$ is admissible, then $\theta (Y_B)$ must be non-empty. The first inclusion for $Y_B$ says that $\theta (Y_B)$ consists of the empty word, whereas the second says that every element of $\theta (Y_B)$ must start with the letter s. Thus, $\mathfrak {I}_{\varGamma _2,\tau }^\emptyset$ cannot have an admissible solution.

To take a non-empty ontology into account, the right-hand sides of the language inclusions must be extended. Our new translation yields linear language inclusions $\mathfrak {i}^*_{A}(\mathfrak {s})$ of the form

$$\begin{aligned} X_A \subseteq f^*_{A}(C_1) \cup \cdots \cup f^*_{A}(C_n) \cup \, \mathcal {U}_{A}(\mathfrak {s}), \end{aligned}$$

(1)

where $f^*_{A}(C)$ differs from $f_{A}(C)$ in the way existential restrictions are treated:

$$\begin{aligned} f^*_{A}(\exists r.C') := L_r f_{A}(C') \text { where } L_r:=\{s \in \mathsf {N_R}\mid r \trianglelefteq _\mathcal {O}s\}. \end{aligned}$$

This modification of $f_{A}$ to $f^*_{A}$ takes care of the role hierarchy.

Example 4

For instance, if in the system of Example 3 we replace $B\sqsubseteq ^? Y$ with $\exists u.X\sqsubseteq ^? Y$, then the language inclusions corresponding to this constraint are $Y_A \subseteq \{u\}X_A$ and $Y_B \subseteq \{u\}X_B$. The new system again does not have an admissible solution. However, if we consider an ontology $\mathcal {O}$ containing $u\sqsubseteq s$, then the new translation yields the language inclusions $Y_A \subseteq \{u,s\}X_A$ and $Y_B \subseteq \{u,s\}X_B$ for this constraint. Consequently, the new system of language inclusions has a finite, admissible solution, which reflects the fact that the system of subsumption constraints has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}$.

The GCIs and transitivity axioms of the ontology are taken care of by the additional term $\mathcal {U}_{A}(\mathfrak {s})$ in (1). This term uses additional types of indeterminates whose meaning is encoded using additional language inclusions. Indeterminates of the form $Z_{B \rightarrow A}$, where A, B are concept constants occurring in $\varGamma$ or $\mathcal {O}$, are supposed to represent languages containing only words w such that $B \sqsubseteq _\mathcal {O}\exists w.A$. This intuition is formalized by the set of linear inclusions $\mathfrak {I}_{\mathcal {O}}$, which consists of one language inclusion for each indeterminate $Z_{B \rightarrow A}$ having the following form:

$$\begin{aligned} Z_{B \rightarrow A} \subseteq L\cup \bigcup \limits _{(r,B') \in I(B)} \{r\}Z_{B' \rightarrow A},\ \ \end{aligned}$$

(2)

where $I(B) := \{(r,B') \in \mathsf {N_R}\times ( Ats (\mathcal {O}) \cap \mathsf {N_C}) \mid B \sqsubseteq _\mathcal {O}\exists r.B'\}$ and $L:= \{\varepsilon \}$ if $B \sqsubseteq _\mathcal {O}A$, and $L:= \emptyset$ otherwise. The set of linear inclusions $\mathfrak {I}_{\mathcal {O}}$ captures subsumptions of the form $B \sqsubseteq _\mathcal {O}\exists w.A$ in the following sense.

Lemma 4

Let $\mathcal {O}$ be a flat, cycle-restricted $\mathcal {ELH}_{\mathcal {R}^+}$-ontology.

• 1. If $\theta$ is a solution of $\mathfrak {I}_{\mathcal {O}}$, then $w \in \theta (Z_{B \rightarrow A})$ implies $B \sqsubseteq _\mathcal {O}\exists w.A$.

• 2. If we define $\theta (Z_{B \rightarrow A}) := \{w \in \mathsf {N_R}^* \mid B \sqsubseteq _\mathcal {O}\exists w.A\}$, then $\theta$ is a finite solution of $\mathfrak {I}_{\mathcal {O}}$.

Example 5

Consider again the system $\varDelta _{\varGamma _2,\tau }$ of Example 3, but replace $B\sqsubseteq ^? Y$ with $\exists r.B\sqsubseteq ^? Y$. The language inclusions corresponding to this constraint are $Y_A \subseteq \{r\}\emptyset$ and $Y_B \subseteq \{r\}\{\varepsilon \}$. The new system again does not have an admissible solution. However, if we consider the ontology $\mathcal {O}=\{B \sqsubseteq A\}$, then there are solutions $\theta$ of $\mathfrak {I}_{\mathcal {O}}$ that satisfy $\varepsilon \in \theta (Z_{B \rightarrow A})$. Thus, if we extend the inclusion $Y_A \subseteq \{r\}\emptyset$ obtained from $\exists r.B\sqsubseteq ^? Y$ to $Y_A \subseteq \{r\}\emptyset \cup \{r\}Z_{B \rightarrow A}$, then the new system has a solution $\theta$ such that $r\in \theta (Y_A)$ since the other inclusion for $Y_A$ is $Y_A \subseteq \{s\}X_A\cup \{r\}\{\varepsilon \}$. This implies that there is an admissible solution since there are no language inclusions constraining $X_A$ or $X_B$.

To deal with transitivity axioms, we introduce additional indeterminates of the form $X_{A,t}$, which are constrained by the following linear language inclusions: $\mathfrak {i}_{A,t}(\mathfrak {s}) = X_{A,t} \subseteq f_{A,t}(C_1) \cup \cdots \cup f_{A,t}(C_n) \cup \, \mathcal {U}_{A,t}(\mathfrak {s})$ where

$$ f_{A,t}(C) := {\left\{ \begin{array}{ll} f_{A}(C') &{} \text {if } C = \exists r.C' \wedge r \trianglelefteq _\mathcal {O}t,\\[.3em] Y_{A,t} &{} \text {if } C = Y \in \mathsf {N_V},\\[.3em] \emptyset &{} \text {otherwise}. \end{array}\right. } $$

Intuitively, the difference between $\mathfrak {i}^*_{A}(\mathfrak {s})$ and $\mathfrak {i}_{A,t}(\mathfrak {s})$ is that, given a particle $\exists t.\exists w.A$ satisfying $\sigma (C_1) \sqcap \cdots \sqcap \sigma (C_n) \sqsubseteq _\mathcal {O}\exists t.\exists w.A$, the right-hand side of $\mathfrak {i}_{A,t}(\mathfrak {s})$ is designed to recognize w instead of $t w$.

Example 6

Assume that

$$\begin{aligned} \varDelta _{\varGamma ,\tau } = \{\exists r.B\sqsubseteq ^? Y, \exists s.X \sqcap \exists r.A \sqsubseteq ^? Y, \exists t.B \sqsubseteq ^? X\}. \end{aligned}$$

In addition, consider the ontology $\mathcal {O}=\{s \sqsubseteq t, t \sqsubseteq r\}$. Since $\exists r.B \sqsubseteq ^? Y$ yields the language inclusion $Y_A \subseteq \{r\}\emptyset$, any solution $\theta$ of $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ must satisfy $\theta (Y_A) = \emptyset$. Hence, if $\theta$ is admissible, then $\theta (Y_B) \ne \emptyset$. In the presence of $\mathcal {O}$, the new translation also yields the inclusions:

$$\begin{aligned} Y_B \subseteq \{r\}\{\varepsilon \},\ Y_B \subseteq \{s,t,r\} X_B \cup \{r\}\emptyset \ \text { and }\ X_B \subseteq \{t,r\}\{\varepsilon \}. \end{aligned}$$

Together with $\theta (Y_B) \ne \emptyset$, the first of these inclusions yields $\theta (Y_B) = \{r\}$. Thus, the second inclusion implies that $\varepsilon \in \theta (X_B)$, and thus $\theta$ does not solve the third inclusion. Thus, $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ cannot have an admissible solution, corresponding to the fact that $\varDelta _{\varGamma ,\tau }$ does not have an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier w.r.t. $\mathcal {O}$.

However, if we add the transitivity axiom $t \circ t \sqsubseteq t$ to $\mathcal {O}$, then $\varDelta _{\varGamma ,\tau }$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier $\gamma$ with $\gamma (X) = \exists t.B$ and $\gamma (Y) = \exists r.B$ w.r.t. this ontology. The inclusion $\mathfrak {i}_{B,t}(\mathfrak {s}) = X_{B,t}\subseteq \{\varepsilon \}$, obtained from $\mathfrak {s}=\exists t.B \sqsubseteq ^? X$, admits solutions $\theta$ with $\theta (X_{B,t})=\{\varepsilon \}$. Hence, if we extend the language inclusion $Y_B \subseteq \{s,t,r\} X_B \cup \{r\}\emptyset$ to the new one

$$\begin{aligned} Y_B \subseteq \{s,t,r\} X_B \cup \{r\}\emptyset \cup \{r\}X_{B,t} \end{aligned}$$

that takes transitivity of t into account, then the new system of language inclusions has an admissible solution with $\theta (Y_B)=\{r\}$ and $\theta (X_B)=\{t\}$, which corresponds to the unifier $\gamma$.

Since the definitions of the terms $\mathcal {U}_{A}(\mathfrak {s})$ and $\mathcal {U}_{A,t}(\mathfrak {s})$ are quite long and technical, we refer to [9] for exact definitions and detailed explanations motivating them. Let $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ be the system of linear language inclusions consisting of $\mathfrak {I}_{\mathcal {O}}$ and the inclusions $\mathfrak {i}^*_{A}(\mathfrak {s})$ and $\mathfrak {i}_{A,t}(\mathfrak {s})$ for every subsumption constraint $\mathfrak {s}$ in $\varDelta _{\varGamma ,\tau }$. Note that the definition of these language inclusions does not only depend on $\varDelta _{\varGamma ,\tau }$, but also on $\tau$ itself (see Definition 4.17 in [9] for the exact definition).

Proposition 2

Let $\tau$ be a subsumption mapping for $\varGamma$ w.r.t. $\mathcal {O}$. The unification problem $\varDelta _{\varGamma ,\tau }$ has an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier $\gamma$ w.r.t. $\mathcal {O}$ that is compatible with $\tau$ iff the system of linear language inclusions $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ has a finite, admissible solution.

The proof of the only-if direction of this proposition makes use of the fact that we can assume without loss of generality that $\gamma$ is a simple unifier. In fact, this is already taken into account in the definition of $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ (see [9]).

Definition 5

The $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier $\gamma$ of $\varDelta _{\varGamma ,\tau }$ w.r.t. $\mathcal {O}$ is called simple if, for all $C_1 \sqcap \cdots \sqcap C_n \sqsubseteq ^? X \in \varDelta _{\varGamma ,\tau }$ and $\exists w.A \in Part (\gamma (X))$, the following holds:

• 1. there exists $i, 1 \le i \le n$ such that

  • (a) $C_i$ is a ground atom and $C_i \mathbin {\sqsubseteq ^s_{\mathcal {O}}} \exists w.A$, or

  • (b) $C_i=Y$ is a variable and $\exists w.A \in Part (\gamma (C_i))$, or

  • (c) $C_i=\exists r.Y$ for a variable Y, $w=sw'$ for some $s \in \mathsf {N_R}$ and $w' \in \mathsf {N_R}^*$, and

    • $\exists w'.A \in Part (\gamma (Y))$ and $r \trianglelefteq _\mathcal {O}s$, or

    • $\exists t.\exists w'.A \in Part (\gamma (Y))$ for a transitive role t s.t. $r \trianglelefteq _\mathcal {O}t \trianglelefteq _\mathcal {O}s$; or

• 2. There are atoms $At _1,\ldots , At _k, At '$ of $\mathcal {O}$ ($k \ge 0$) such that:

  • (a) $At _1\sqcap \cdots \sqcap At _k \sqsubseteq _\mathcal {O} At '$,

  • (b) for all $\ell \in \{1,\ldots ,k\}$, there exists $i \in \{1,\ldots ,n\}$ s.t. $\tau (C_i, At _\ell )=1$, and

  • (c) $At ' \mathbin {\sqsubseteq ^s_{\mathcal {O}}} \exists w.A$.

Lemma 5

If $\varGamma$ is an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problem that is unifiable w.r.t. $\mathcal {O}$, then there exists a subsumption mapping $\tau$ for $\varGamma$ w.r.t. $\mathcal {O}$ such that $\varDelta _{\varGamma ,\tau }$ has a simple $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unifier $\sigma$ w.r.t. $\mathcal {O}$ that is compatible with $\tau$.

3.3 The PSpace Algorithm

Using the results described in the previous two subsections, we can construct an NPSpace decision procedure for unification in $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$ w.r.t. cycle-restricted $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontologies. Due to Savitch’s theorem [26], this implies that the problem is also in PSpace.

Given an input consisting of an $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problem and a cycle-restricted $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontology, the algorithm transforms the ontology and the unification problem into flat ones, which we denote as $\varGamma$ and $\mathcal {O}$. It then proceeds as follows:

• 1. It guesses a subsumption mapping $\tau$ for $\varGamma$ w.r.t. $\mathcal {O}$. If no such mapping exists, then it fails.

• 2. It transforms $\varGamma$ into $\varDelta _{\varGamma ,\tau }$, and then translates the latter into the set of linear language inclusions $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$.

• 3. Finally, the algorithm answers “yes” iff $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ has a finite, admissible solution.

Flattening can be done in polynomial time and preserves unifiability [5, 18]. A mapping $\tau : Ats_{tr} (\varGamma ,\mathcal {O}) \times Ats_{tr} (\varGamma ,\mathcal {O}) \rightarrow \{0,1\}$ can be guessed in non-deterministic polynomial time, and checking whether it satisfies the properties of a subsumption mapping (see Definition 3) can clearly also be realized within polynomial space, as can the translations into $\varDelta _{\varGamma ,\tau }$ and $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$. Finally, as shown in [18], testing for the existence of a finite, admissible solution of $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$ can be reduced in polynomial time to checking emptiness of alternating finite automata with $\varepsilon$-transitions, which is a PSpace-complete problem [23]. This shows that the introduced algorithm really is an NPSpace algorithm. Its correctness is an immediate consequence of Propositions 1 and 2. Since PSpace-hardness already holds for the special case of an empty ontology, we thus have shown the following main result of this paper.

Theorem 1

Deciding unifiability of $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-unification problems w.r.t. cycle-restricted $\mathcal {ELH}^{-\!\top }_{\mathcal {R}^+}$-ontologies is PSpace-complete.

4 Conclusion

We have shown that the approach for obtaining a PSpace decision procedure for $\mathcal{E}\mathcal{L}^{-\!\top }$-unification without a background ontology [18] can be extended to unification w.r.t. a cycle-restricted $\mathcal {ELH}_{\mathcal {R}^+}$-ontology, i.e., an ontology that may contain general concept inclusions (GCIs) formulated in $\mathcal{E}\mathcal{L}^{-\!\top }$ as well as role inclusion and transitivity axioms, but does not entail a cyclic subsumption of the form $C \sqsubseteq _\mathcal {O}\exists r_1.\exists r_2.\cdots \exists r_n.C$ ($n\ge 1$). As explained in the introduction, both considering concept descriptions not containing the top concept $\top$ and considering GCIs and role axioms is motivated by the expressivity employed in the medical ontology SNOMED CT. Dealing with such a background ontology not only makes the approach more complicated due to the more involved characterization of subsumption (see Lemma 1 and Definition 3, compared to the much simpler versions in [18]). It also requires the development of new notions, such as simple unifiers and the extension of the system of linear language inclusions with new indeterminates and corresponding inclusions.

With SNOMED CT in mind, it would be interesting to see whether results on unification (with or without top) can be further extended to ontologies additionally containing so-called right-identity rules, i.e., role axioms of the form $r\circ s\sqsubseteq r$, since they are also needed to get rid of the SEP-triplet encoding mentioned in the introduction. However, extending the characterization of subsumption to this setting is probably a non-trivial problem. From a theoretical point of view, the big open problem is whether one can dispense with the requirement that the ontology must be cycle-restricted. Even for pure $\mathcal{E}\mathcal{L}$, decidability of unification w.r.t. unrestricted ontologies is an open problem.

From a practical point of view, the next step is to develop an algorithm that replaces non-deterministic guessing by a more intelligent search procedure. Since the unification problem is PSpace-complete, a polynomial translation of the whole problem into SAT is not possible (unless NP = PSpace). However, one could try to delegate the search for a subsumption mapping to a SAT solver, which interacts with a solver for the additional condition on such a mapping (existence of a finite, admissible solution of $\mathfrak {I}_{\varGamma ,\tau }^{\mathcal {O}}$) in an SMT-like fashion [21].