On the Complexity of Semantic Integration of OWL Ontologies Yevgeny Kazakov1 , Denis Ponomaryov2 1 Institute of Artificial Intelligence, University of Ulm, Germany 2 Institute of Informatics Systems, Novosibirsk State University, Russia yevgeny.kazakov@uni-ulm.de, ponom@iis.nsk.su Abstract. We propose a new mechanism for integration of OWL ontologies us- ing semantic import relations. In contrast to the standard OWL importing, we do not require all axioms of the imported ontologies to be taken into account for reasoning tasks, but only their logical implications over a chosen signature. This property comes natural in many ontology integration scenarios. In this paper, we study the complexity of reasoning over ontologies with semantic import relations and establish a range of tight complexity bounds for various fragments of OWL. 1 Introduction and Motivation Ontology integration is a research topic which, in particular, aims at organizing in- formation on different domains in a modular way so that information from one ontology can be reused in other ontologies. There is a number of approaches known in the liter- ature [1–5, 8], which address this problem from the point of view of ontology linking and importing, see, e.g., an overview in [6]. Integration of multiple ontologies in OWL is organized via importing: an OWL ontology can refer to one or several other OWL ontologies, whose axioms must be implicitly present in the ontology. The importing mechanism is simple in that reasoning over an ontology with an import declaration is reduced to reasoning over the import closure consisting of the axioms of the ontology plus the axioms of the ontologies that are imported (possibly indirectly). For example, if ontology O1 imports ontologies O2 and O3 , each of which, in turn, imports ontology O4 , then the import closure of O1 consists of all axioms of O1 − O4 . Although the OWL importing mechanism may work well for simple ontology inte- gration scenarios, it may cause some undesirable side effects if used in complex import situations. To illustrate the problem, suppose that in the above example, O4 is an ontol- ogy describing a typical university. It may include concepts such as Professor, Course, and axioms stating, e.g., that each professor must teach some course: Professor v ∃teaches.Course. Now suppose that O2 and O3 are ontologies describing respectively, Oxford and Cambridge universities that use O4 as a prototype. For example, O2 may include mapping axioms OxfordProfessor ≡ Professor, OxfordCourse ≡ Course, from which, due to the axiom in O4 , it is now possible to conclude that OxfordProfessor v ∃teaches.OxfordCourse. Likewise, using similar mapping axioms in O3 , it is possi- ble to obtain that CambridgeProfessor v ∃teaches.CambridgeCourse. Finally, sup- pose that O1 is an ontology aggregating information about UK universities, importing, among others, the ontologies O2 and O3 for Oxford and Cambridge universities. Al- though the described scenario seems plausible, there will be some undesirable conse- quences in O1 due to the mapping axioms of O2 and O3 occurring in the import clo- sure: OxfordProfessor ≡ CambridgeProfessor, OxfordCourse ≡ CambridgeCourse. The main reason for these consequences is that the ontologies O2 and O3 happen to reuse the same ontology O4 in two different and incompatible ways. Had they instead used two different ‘copies’ of O4 as prototypes (with concepts renamed apart), no such problem would take place. Arguably, the primary purpose of O2 and O3 is to provide semantic description of the vocabulary for Oxford and Cambridge universities, and the means of how it is achieved—either by writing the axioms directly or reusing third party ontologies such as O4 —should be an internal matter of these two ontologies and should not be exposed to the ontologies that import them. Motivated by these observations, in this paper we consider a refined mechanism for importing of OWL ontologies called semantic importing. The main difference with the standard OWL importing is that each import is limited only to a subset of symbols. Intuitively, only logical properties of these symbols entailed by the imported ontology should be imported. These symbols can be regarded as the public (or external) vocabulary of the imported ontologies. For example, ontology O2 may declare the symbols OxfordProfessor, OxfordCourse, and teaches public, leaving the remaining symbols only for the internal use. Importantly, in our approach every ontology has its own view on ontologies it imports and the views are independent between ontologies unless coordinated by the ‘topology’ of import re- lations. The main results of this paper are tight complexity bounds for reasoning over on- tologies with semantic imports. We consider ontologies formulated in different frag- ments of OWL starting from the Description Logic (DL) EL and concluding with the DL SROIQ, which corresponds to OWL 2. We also distinguish the case of acyclic im- ports, when ontologies cannot (possibly indirectly) import themselves. Our complete- ness results for ranges of DLs are summarized in the following table, where a and c denote the case of acyclic/cyclic imports: DLs Completeness Theorems EL – EL++ ExpTime a 1, 8 containing EL RE (undecidable) c 2, 9 ALC – SHIQ 2ExpTime a 3, 8 R – SRIQ 3ExpTime a 4, 8 ALCHOIF – SHOIQ coN2ExpTime a 5, 8 ROIF – SROIQ coN3ExpTime a 6, 8 An extended version of the paper containing all proofs and additional results is available at https://arxiv.org/abs/1705.04719 2 Preliminaries We assume that the reader is familiar with the family of Description Logics from EL to SROIQ, for which the syntax is defined using a recursively enumerable al- phabet consisting of infinite disjoint sets NC , NR , Ni of concept names (or primitive concepts), roles, and nominals, respectively. The semantics of DLs is given by means of (first-order) interpretations. An ontology is a set of concept inclusions which are called ontology axioms. A signature is a subset of NC ∪ NR ∪ Ni . Interpretations I and J are said to agree on a signature Σ, written as I =Σ J , if the domains of I and J coincide and the interpretation of Σ-symbols in I is the same as in J . We denote the reduct of an interpretation I onto a signature Σ as I|Σ . The signature of a concept C, denoted as sig (C), is the set of all concept names, roles, and nominals occurring in C. The signature of a concept inclusion or an ontology is defined identically. Given a signature Σ, suppose one wants to import into an ontology O1 the seman- tics of Σ-symbols defined by some other ontology O2 , while ignoring the rest of the symbols from O2 . Intuitively, importing the semantics of Σ-symbols means reducing the class of models of O1 by removing those models that violate the restrictions on interpretation of these symbols, which are imposed by the axioms of O2 : Definition 1. A (semantic) import relation is a tuple π = hO1 , Σ, O2 i, where O1 and O2 are ontologies and Σ a signature. In this case, we say that O1 imports Σ from O2 . We say that a model I |= O1 satisfies the import relation π if there exists a model J |= O2 such that I =Σ J . Example 1. Consider the import relation π = hO1 , Σ, O2 i, with O1 = {B v C}, O2 = {A v ∃r.B, ∃r.C v D}, and Σ = {A, B, C, D}. It can be easily shown using Definition 1 that a model I |= O1 satisfies π if and only if I |= A v D. Note that if Σ contains all symbols in O2 then I |= O1 satisfies π = hO1 , Σ, O2 i if and only if I |= O1 ∪ O2 . That is, the standard OWL import relation is a special case of the semantic import relation, when the signature contains all the symbols from the imported ontology. If O has several import relations φi = hO, Σi , Oi i, (1 ≤ i ≤ n), one can define the entailment from O by considering only those models of O that satisfy all imports: O |= α if I |= α for every I |= O which satisfies all π1 , . . . , πn . In practice, however, import relations can be nested: imported ontologies can themselves import other ontologies and so on. The following definition generalizes entailment to such situations. Definition 2. An ontology network is a finite set N of import relations between on- tologies. For a DL L, a L-ontology network is a network, in which every ontology is a set of L-axioms. A model agreement for N (over a domain ∆) is a mapping µ that assigns to every ontology O occurring in N a class µ(O) of models of O with domain ∆ such that for every hO1 , Σ, O2 i ∈ N and every I1 ∈ µ(O1 ) there exists I2 ∈ µ(O2 ) such that I1 =Σ I2 . An interpretation I is a model of O in the network N (notation I |=N O) if there exists a model agreement µ for N such that I ∈ µ(O). An ontol- ogy O entails a concept inclusion ϕ in the network N (notation O |=N ϕ) if I |= ϕ, whenever I |=N O. An ontology network can be seen as a labeled directed multigraph in which nodes are labeled by ontologies and edges are labeled by sets of signature symbols. Note that Definition 2 also allows for cyclic networks if this graph is cyclic. Note that if O |= ϕ then O |=N ϕ, for every network N . In this paper, we are concerned with the complexity of entailment in ontology net- works, that is, given a network N , an ontology O and an axiom ϕ, decide whether O |=N ϕ. We study the complexity of this problem wrt the size of an ontology network N , which is defined as the total length of axioms (considered as strings) occurring in ontologies from N . 3 Expressiveness of Ontology Networks First, we illustrate the expressiveness of ontology networks by showing that acyclic networks allow for succinctly representing axioms with nested concepts and role chains of exponential size, while cyclic ones allow for succinctly representing infinite sets of axioms of a special form. The lemmas given in this Section are used as building blocks in the proofs of our hardness results in Section 4. For a natural number n > 0, let ∃(r, C)n .D be a shortcut for the nested concept ∃r.(C u ∃r.(C u . . . n times . . . u ∃r.(C u D) . . .)), where C, D are DL concepts and r a role (in case n = 0 the above concept is set to be D). For n > 1, let (r)n denote the role chain r ◦ . . . n times . . . ◦ r. For a given n > 0, let 1exp(n) be the notation for 2n and for k > 1, let (k + 1)exp(n) = 2kexp(n) . Then ∃(r, C)kexp(n) .D (respec- tively, (r)kexp(n) ) stands for a nested concept (role chain) of the form above having size exponential in n. In the following, we use abbreviations ∃(r, C)n := ∃(r, C)n .> and ∃rn .C := ∃(r, >)n .C. For n > 1, the expression ∀rn .C will be used as a shortcut for ¬∃r.∃rn−1 .¬C and for n > 2, ∀r 1, let us denote by ϕ[C1 7→ D1 , . . . , Cn 7→ Dn ] the axiom obtained by substituting every concept Ci S Di in ϕ. For an ontology O, let O[C1 7→ D1 , . . . , Cn 7→ Dn ] be a with a concept notation for ϕ∈O ϕ[C1 7→ D1 , . . . , Cn 7→ Dn ]. Lemma 2. Let L be a DL and O an ontology, which is expressible by a L-ontology network N . Let C1 , . . . , Cn be L-concepts and {A1 , . . . , An } a set of concept names such that Ai ∈ sig (O), for i = 1, . . . , n and n > 1. Then ontology Õ = O[A1 7→ C1 , . . . , An 7→ Cn ] is expressible by a L-ontology network, which is acyclic if so is N and has size polynomial in the size of N and Ci , i = 1, . . . , n. Proof Sketch. Denote Σ = {A1 , . . . , An } and let Σ 0 = {A01 , . . . , A0n } be a set of fresh concept names. Consider ontology O0 = O ∪ {Ai ≡ A0i }i=1,...,n . By Lemma 1, O0 is (N 0 , ON 0 )-expressible, for an ontology ON 0 and an acyclic L-ontology net- work N 0 having a linear size (in the size of N ). Consider ontology network N 00 = hON 00 , (sig (O0 ) \ Σ) ∪ Σ 0 , ON 0 i, where ON 00 = ∅. Then obviously, ontology O00 = O[A1 7→ A01 , . . . , An 7→ A0n ] is (N 00 , ON 00 )-expressible. Similarly, by Lemma 1, on- 00 tology OC = O00 ∪ {A0i ≡ Ci }i=1,...,n is (Ñ , OÑ )-expressible, for an ontology OÑ and an acyclic L-ontology network Ñ having a linear size (in the size of N and Ci , for i = 1, . . . , n). Clearly, it holds OÑ |=Ñ Õ and it is easy to show that Õ is (Ñ , OÑ )- expressible. Now we formulate the results on the expressiveness of acyclic EL-, ALC-, and R- ontology networks. 1 Note that the size of N is linear in the sizes of N1 and N2 . Lemma 3. An axiom ϕ of the form Z ≡ ∃(r, A)1exp(n) .B, where Z, A, B ∈ NC , and n > 0, is expressible by an acyclic EL-ontology network of size polynomial in n. Proof Sketch. We show by induction on n that there exists an acyclic EL-ontology network Nn and ontology On such that ϕ is (Nn , On )-expressible. For n = 0, we define N0 = {hO0 , ∅, ∅i} and O0 = {Z ≡ ∃r.(A u B)}. In the induction step, let {Z ≡ ∃(r, A)1exp(n−1) .B} be (Nn−1 , On−1 )-expressible, for n > 1. Consider 1 2 ontologies Ocopy = {B ≡ U }, Ocopy = {U ≡ Z}, On = ∅. Let Nn be the union i of Nn−1 with the set of the following import relations: hOcopy , {Z, A, B, r}, On−1 i, 1 2 for i = 1, 2, hOn , {Z, A, U, r}, Ocopy i, and hOn , {U, A, B, r}, Ocopy i. Let us verify that {I|sig (ϕ) | I |=Nn On } = {I|sig (ϕ) | I |= ϕ}. By the induction assumption we have On−1 |=Nn Z ≡ ∃(r, A)1exp(n−1) .B. Then by the definition of Nn , it holds 1 2 Ocopy |=Nn Z ≡ ∃(r, A)1exp(n−1) .U and Ocopy |=Nn U ≡ ∃(r, A)1exp(n−1) .B and thus, On |=Nn {Z ≡ ∃(r, A)1exp(n−1) .U, U ≡ ∃(r, A)1exp(n−1) .B}, which yields On |=Nn ϕ. To complete the proof, we show that any model I |= ϕ can be expanded to a model Jn |=Nn On by setting U Jn = (∃(r, A)1exp(n−1) .B)I . The following claim is proved identically to Lemma 3: Lemma 4. An axiom of the form Z v ∃(r, A)1exp(n) .B, Z ≡ ∀r1exp(n) .A, or (r)2exp(n) v s, where Z, A, B ∈ NC , r, s are roles, and n > 0, is expressible by an acyclic EL-, ALC-, and R-ontology network, respectively, having size polynomial in n. We continue with results on the expressiveness of acyclic R-ontology networks. Lemma 5. An axiom ϕ of the form Z v ∀r2exp(n) .A, where Z, A ∈ NC and n > 0, is expressible by an acyclic R-ontology network of size polynomial in n. Proof. Consider ontology O = {Z v ∀s.A, (r)2exp(n) v s}. Clearly, it holds O |= ϕ and any model I |= ϕ can be expanded to a model J |= O by setting sJ = ((r)2exp(n) )I . By Lemmas 1, 4, O is expressible by an acyclic R-ontology net- work of size polynomial in n, from which the claim follows. Similarly, we demonstrate that an axiom of the form Z v ∀r<2exp(n) .A, where Z, A ∈ NC and n > 0, is expressible by an acyclic R-ontology network of size polyno- mial in n and show the next statement, which is an analogue of Lemma 4 for the case of double exponent. Lemma 6. An axiom ϕ of the form Z v ∃(r, A)2exp(n) .B, where Z, A ∈ NC and n > 0, is expressible by an acyclic R-ontology network of size polynomial in n. Proof. Consider ontology Ō = {Z v ∃s.>, Z v ∀s<2exp(n) .X, Z v ∀s2exp(n) .Y, s v r}. By Lemmas 1, 5, and the claim above, we show that Ō is expressible by an acyclic R-ontology network of size polynomial in n. Then by Lemma 2, so is ontology O = Ō[X 7→ A u ∃s.>, Y 7→ A u B]. Clearly, we have O |= ϕ. Now let I be an arbitrary model of ϕ and for m = 2exp(n), let x0 , . . . , xm be arbitrary domain elements such that x0 ∈ Z I , hx0 , x1 i ∈ rI , and hxi , xi+1 i ∈ rI , xi ∈ AI , for 1 6 i < m, and xm ∈ AI uB I . Let J be an expansion of I in which sJ = {hxi , xi+1 i}06i 0, is expressible by an acyclic R-ontology network of size polynomial in n. Proof. Consider ontology Ō = {Z v ∀r2exp(n) .A, Z̄ v ∃r2exp(n) .Ā}. By Lemmas 1, 5, 6, Ō is expressible by an acyclic R-ontology network of size polynomial in n and by Lemma 2, so is ontology O = Ō[Z̄ 7→ ¬Z, Ā 7→ ¬A]. It remains to note that O and {ϕ} are equivalent, so the claim is proved. We conclude this section with lemmas formulating the expressibility of substitutions by ontology networks. Lemma 8. Let L be a DL and O an ontology, which is expressible by a L-ontology network N . Let C1 , . . . , Cm be L-concepts and {A1 , . . . , Am } a set of concept names such that Ai ∈ sig (O), for i = 1, . . . , m and m > 1. Then for k = 1, 2 and n > 0, ontology Õ = O[A1 7→ ∀rkexp(n) .C1 , . . . , Am 7→ ∀rkexp(n) .Cm ] is expressible by a L0 -ontology network, which is acyclic if so is N and has size polynomial in the size of N , n, and Ci , for i = 1, . . . , m, where: L0 = L if L contains ALC and k = 1, or L0 = L if L contains R and k = 2. Proof. The proof uses Lemmas 4, 7 and is identical to the proof of Lemma 2. The next statement can be shown similarly by using Lemma 3: Lemma 9. In the conditions of Lemma 8, ontology Õ = O[A1 7→ ∃r1exp(n) .C1 , . . . , Am 7→ ∃r1exp(n) .Cm ], for n > 0, is expressible by a L0 -ontology network, which is acyclic if so is N and has size polynomial in the size of N , n, and Ci , for i = 1, . . . , m, where L0 = L if L contains EL. Lemma 10. Let L be a DL and O an ontology, which is (N , ON )-expressible, for a L- ontology network N and an ontology ON . Let {A1 , . . . , An }, n > 1, be concept names such that Ai ∈ sig (O), for i = 1, . . . , n, and let {C1 , . . . , Cn } be L-concepts, where every Ci is of the form ∃(r, D)p .Ai , for some role r, concept name D, and p > 1. Then S ontology Õ = m>0 Om , where O0 = O and Om+1 = Om [A1 7→ C1 , . . . , An 7→ Cn ], for all m > 0, is expressible by a cyclic L-ontology network. Proof Sketch. Let σ = {B1 , . . . , Bk } = i=1,...,n (sig (Ci ) ∩ NC ) and σ 0 = {B10 , . . . , S Bk0 } be a set of fresh concept names disjoint with σ and sig (O). Let {C10 , . . . , Cn0 } be ‘copy’ concepts obtained from C1 , . . . , Cn by replacing every Bi with Bi0 , for i = 1, . . . , k. Consider ontologies ÕN 0 = { Bi ≡ Bi0 }i=1,...,k , O0 = { Ai ≡ Ci0 }i=1,...,n , and an ontology network N 0 given by the union of N with the set of import relations hÕN 0 , sig (O), ON i, hÕN 0 , Σ 0 , O0 i, hO0 , Σ, ÕN 0 i, where Σ 0 = (Σ \ σ) ∪ σ 0 and Σ = sig (O) ∪ i=1,...,n sig (Ci ). We claim that ontology Õ is (N 0 , ÕN 0 )-expressible. S 0 0 Denote Õ0 = m>0 Om = Om [B1 7→ B10 , . . . , Bk 7→ Bk0 ], for all m > S , where Om 0. First, we show by induction that ÕN 0 |=N 0 Om , for all m > 0. The induction base for n = 0 is trivial, since we have O0 = O and O is (N , ON )-expressible, hÕN 0 , sig (O), ON i ∈ N 0 , and thus, ÕN 0 |=N 0 O. Suppose ÕN 0 |=N 0 Om , for some m > 0. Since hO0 , Σ, ÕN 0 i ∈ N 0 , we have O0 |=N 0 Om and thus, by the equivalences in O0 , it holds O0 |=N 0 Om+1 0 . Since hÕN 0 , Σ 0 , O0 i, we have ÕN 0 |=N 0 Om+1 0 and hence, by the equivalences in ÕN 0 , it holds that ÕN 0 |=N 0 Om+1 . Finally, in the full proof we show that any model I of Õ can be expanded to a model J |=N 0 ÕN 0 , which shows that Õ is (N 0 , ÕN 0 )-expressible. 4 Hardness Results We use reductions from the word problem for Turing machines (TMs) and alternat- ing Turing machines (ATMs) to obtain most of the hardness results. We define a Turing Machine (TM) as a tuple M = hQ, A, δi, with qh ∈ Q being the accepting state, and assume w.l.o.g. that configuration of M is a word in the alphabet Q ∪ A. An initial con- figuration is a word of the form b . . . bq0 b . . . b, where q0 ∈ Q and b ∈ A is the blank symbol. It is a well-known property of the transition functions of Turing machines that the symbol c0i at position i of a successor configuration c0 is uniquely determined by a 4-tuple of symbols ci−2 , ci−1 , ci , ci+1 at positions i − 2, i − 1, i, and i + 1 of a config- uration c. We assume that this correspondence is given by the (partial) function δ 0 and δ0 use the notation ci−2 ci−1 ci ci+1 7→ c0i . Theorem 1. Entailment in acyclic EL-ontology networks is ExpTime-hard. Proof Sketch. We reduce the word problem for TMs making exponentially many steps to entailment in EL-ontology networks. Let M be a TM and n = 1exp(m) an exponential, for m > 0. Consider an ontology O defined for M and n by the following axioms: A v ∃rn·(2n+3) .(q0 u ∃(r, b)2n+2 ), where A 6∈ Q ∪ A (1) 2n δ0 ∃r (X u ∃r.(Y u ∃r.(U u ∃r.Z))) v W, for XY U Z 7→ W (2) ∃r.qh v H, ∃r.H v H, where H 6∈ Q ∪ A (3) The first axiom gives a r-chain containing n + 1 segments of length 2n + 3, which are used to store fragments of consequent configurations of M . We assume the following enumeration of segments in the r-chain: |{z}. . . .. |{z} . . . q0 b . . . b, i.e., s0 represents a | {z } sn s1 s0 fragment of the initial configuration c0 of M . For 0 6 i < n, every i-th and (i + 1)-st segments in the r-chain are reserved for a pair of configurations ci , ci+1 such that ci+1 is a successor of ci . Axioms (2), with X, Y, U, Z, W ∈ Q ∪ A, represent transitions of M and define the ‘content’ of (i + 1)-st segment based on the ‘content’ of i-th segment. Finally, axioms (3) are used to initialise the halting marker H and propagate it to the ‘left’ of the r-chain. We show that M accepts the empty word in n steps iff O |= A v H. For the ‘only if’ direction we assume there is a sequence of configurations c0 , . . . , cn such that for all 0 6 i < n, ci+1 is a successor configuration of ci and qh is the state symbol in cn . Let I be a model of O and a domain element such that a ∈ AI . Then by axiom (1), there is an r-chain outgoing from x, which contains segments s0 , . . . , sn of length 2n + 3, where s0 represents a fragment of c0 . It can be shown by induction that due to axioms (2), every segment si represents a fragment of ci , for 1 6 i 6 n, and contains the state symbol from ci . Then by axiom (3), it follows that a ∈ H I . For the ‘if’ direction, one can provide a model I of O such that AI = {a} is a singleton, qh I = H I = ∅, and I gives an r-chain outgoing from a, which contains n + 1 segments representing fragments of consequent configurations of M , neither of which contains qh . To complete the proof of the theorem we show that ontology O is expressible by an acyclic EL-ontology network of size polynomial in m. Consider axiom (1) and a concept inclusion ϕ of the form A v ∃rn·(2n+3) .B, where p B is a concept name. Observe that it is equivalent to A v ∃r | {z.∃rp} . ∃r n | .∃r n n {z .∃r } .B, 2 times 3 times where p = 1exp(2m). Consider axiom ψ of the form A v B. By iteratively applying Lemma 9 we obtain that ψ[B 7→ ∃rp .∃rp .B] is expressible by an acyclic EL-ontology network of size polynomial in m. By repeating this argument we obtain the same for ϕ. Further, by Lemma 2, the axiom θ = ϕ[B 7→ q0 u B] is expressible by an acyclic EL-ontology network of size polynomial in m. Again, by iteratively applying Lemma 9 together with Lemma 2 we conclude that θ[B 7→ ∃(r, b)2n+2 ] is expressible by an acyclic EL-ontology network of size polynomial in m and thus, so is axiom (1). The expressibility of axioms (2) is shown identically. The remaining axioms of ontology O are EL-axioms whose size does not depend on m. By applying Lemma 1 we obtain that there exists an acyclic EL-ontology network N of size polynomial in m and an ontology ON such that O is (N , ON )-expressible and thus, it holds ON |=N A v H iff M accepts the empty word in 1exp(m) steps. Theorem 2. Entailment in cyclic EL-ontology networks is RE-hard. Proof Sketch. For a TM M , we define an infinite ontology O, which contains variants of axioms (1-2) from Theorem 1 and additional axioms for a correct implementation of transitions of M : A v ∃rk .(∃v l .L u ε u ∃r.(q0 u ∃(r, b)2l+2 )), where A, L, ε 6∈ Q ∪ A (4) k k ∃r.∃v .L v ∃v .L, k > 0 (5) k 2k+4 ∃v .L u ∃r .ε v ε, k > 0 (6) 0 δ ∃v k .L u ∃r2k+1 .(X u ∃r.(Y u ∃r.(U u ∃r.Z))) v W, for XY U Z 7→ W (7) δ0 ∃v k .L u ∃r2k .(b u ∃r.(ε u ∃r.(Y u ∃r.(U u ∃r.Z)))) v W, for bY U Z 7→ W (8) 0 δ ∃v k .L u ∃r2k .(b u ∃r.(b u ∃r.(ε u ∃r.(U u ∃r.Z)))) v W, for bbU Z 7→ W (9) 0 δ ∃v k .L u ∃r2k .(X u ∃r.(b u ∃r.(b u ∃r.(ε u ∃r.Z)))) v W, for XbbZ 7→ W (10) qh v H, ∃r.H v H, where H 6∈ Q ∪ A (11) Axioms (4) give an infinite family of r-chains, each having a ‘prefix’ of length k + 1, for k > 0 (reserved for fragments of consequent configurations of M ), and a ‘postfix’ containing a chain of length 2l + 3, for l > 0, which represents a fragment of the initial configuration c0 . Propagated to the ‘left’ by axioms (5), concept ∃v k .L indicates the length of the ‘postfix’ for c0 on every r-chain given by axioms (4). The concept ε is used to separate fragments of consequent configurations of M and is propagated by axioms (6). The family of axioms, (7)-(10), with X, Y, U, Z, W ∈ Q ∪ A and k > 0, implements transitions of M . Concept ∃v k .L guarantees that transitions have effect only along r-chains which represent a fragment of c0 of length 2k + 3. Since ε 6∈ Q ∪ A, the transitions involving ε are implemented separately by axioms (8)-(10). The more involved implementation of transitions (in comparison to Theorem 1) allows to prevent defect situations, when there are two consequent segments si ,si+1 of an r- chain, which represent fragments of configurations ci ,ci+1 of M , respectively, but ci+1 is not a successor of ci . In Theorem 1, the prefix of length n · (2n + 3) given by axiom (1) guarantees a correct implementation of up to n transitions of the TM. The situation is different in the infinite case, since the prefix reserved for fragments of consequent configurations of M can be of any length, due to axioms (4). We prove that M halts iff O |= A v H. Suppose that c0 is an accepting config- uration and M halts in n steps; w.l.o.g. we assume that n > 1. Let I be a model of O and a ∈ AI a domain element. Due to axioms (4), I is a model of the concept inclusion: A v ∃rn·(2n+4) .(∃v n .L u ε u ∃r.(q0 u ∃(r, b)2n+2 )) and thus, I gives a r-chain containing n + 1 segments of length 2n + 3 separated by ε. By using argu- ments from the proof of Theorem 1, it can be shown that due to axioms (5) - (10), these segments represent fragments of consequent configurations of M , starting with c0 , and there is an element b in the r-chain such that b ∈ qh I . Then by axiom (11), it holds a ∈ H I . For the ‘if’ direction, one can show that if M does not halt, then there exists a model I of O such that qh I = H I = ∅, AI = {a} is a singleton and there are infinitely many disjoint r-chains {Rm,n }m,n>1 outgoing from a, such that every Rm,n represents a fragment of c0 of length n and has a prefix of length m + 1 repre- senting fragments of consequent configurations of M , each having length 6 2n + 3. To complete the proof of the theorem we show that ontology O is expressible by a cyclic EL-ontology network. Let us demonstrate that so is the family of axioms (4). Let ϕ = A v B be a concept inclusion and B, B1 , B2 concept names. By Lemma 10, ontology O1 = {ϕ[B 7→ ∃rk .B] | k > 0} is expressible by a cyclic EL-ontology network. Then by Lemma 2, ontology O2 = O1 [B 7→ B1 u ε u ∃r.(q0 u B2 )] is ex- pressible by a cyclic EL-ontology network. By applying Lemma 10 again, we conclude that so is ontology O3 = l>0 O2 [B1 7→ ∃v l .B1 , B2 7→ ∃(r, b)2l .B2 ], i.e., the on- S tology given by axioms A v ∃rk .(∃v l .B1 u ε u ∃r.(q0 u ∃(r, b)2l .B2 )), for k, l > 0. Further, by Lemma 2, we obtain that O2 [B1 7→ L, B2 7→ ∃(r, b)2 ] is expressible by a cyclic EL-ontology network and hence, so is the family of axioms (4). A similar ar- gument shows the expressibility of ontologies given by axioms (5)-(10). The remaining subset of axioms (11) of O is finite. By Lemma 1, there exists a cyclic EL-ontology network N and an ontology ON such that O is (N , ON )-expressible and thus, it holds ON |=N A v H iff M halts. Theorem 3. Entailment in ALC-ontology networks is 2ExpTime-hard. Proof Sketch. The proof is by reduction of the word problem for 1exp(n)-space bounded ATMs to entailment in ALC-ontology networks. We demonstrate that under a minor modification the construction from Theorem 7 in [7] shows that there exists a ALC- ontology O and a concept name A such that O 6|= A v ⊥ iff a given 1exp(n)-space bounded ATM M accepts the empty word. The ontology contains axioms with concepts of the form ∃(r, C)1exp(n) .D and ∀r1exp(n) .D. By using Lemmas 4, 8, we show that ev- ery axiom of O containing concepts of size exponential in n is expressible by an acyclic ALC-ontology network N of size polynomial in n. Then by applying Lemma 1 we ob- tain that there exists an acyclic ALC-ontology network N of size polynomial in n and an ontology ON such that O is (N , ON )-expressible and thus, it holds ON |=N A v ⊥ iff M accepts the empty word. Since AExpSpace = 2ExpTime, we obtain the re- quired statement. Theorem 4. Entailment in R-ontology networks is 3ExpTime-hard. Proof Sketch. Given a 2exp(n)-space bounded ATM M and a number n > 0, we con- sider ontology O from the proof of Thm. 3 for M and let O0 be the ontology obtained from O by replacing every concept of the form ∃(r, C)1exp(n) .D and ∀r1exp(n) .D with ∃(r, C)2exp(n) .D and ∀r2exp(n) .D, respectively. A repetition of the proof of Thm. 3 using Lemmas 1, 6, 8 shows that there is an acyclic R-ontology network N of size polynomial in n and an ontology ON such that O0 is (N , ON )-expressible and thus, ON |=N A v ⊥ iff M accepts the empty word. Since A2ExpSpace = 3ExpTime, we obtain the required statement. Theorem 5. Entailment in ALCHOIF-ontology networks is coN2ExpTime-hard. Proof Sketch. The theorem is proved by reduction of the N2ExpTime-hard problem of domino tiling of size 2exp(n) × 2exp(n) to (non-)entailment in ALCHOIF-ontology networks. Under a minor modification the construction from Theorem 5 in [7] shows that there exists a ALCHOIF-ontology O and a concept name A such that O 6|= A v ⊥ iff a given domino system admits a tiling of size 2exp(n) × 2exp(n), for n > 0. Ontology O contains axioms with concepts of the form ∃r1exp(n) .C and ∀r1exp(n) .C. By using the same arguments as in the proof of Theorem 3 we show that there is a ALCHOIF-ontology network N of size polynomial in n and an ontology ON such that ON |=N A v ⊥ iff the domino system does not admit a tiling. Theorem 6. Entailment in ROIF-ontology networks is coN3ExpTime-hard. Proof Sketch. The proof is by reduction of the N3ExpTime-hard problem of domino tiling of size 3exp(n) × 3exp(n) to (non-)entailment in ROIF-ontology networks. The proof employs a modification of the ontology O from the proof of Thm. 5 which is obtained like in the proof sketch to Thm. 4. 5 Membership Results As a tool for proving upper complexity bounds, we demonstrate that entailment in a network N can be reduced to entailment from (a possibly infinite) union of ‘copies’ S ontologies appearing in N . For an ontology network N , let us denote sig (N ) = of hO1 ,Σ,O2 i∈N (sig (O1 ) ∪ Σ ∪ sig (O2 )). An import path in N is a sequence p = {O0 , Σ1 , O1 , . . . , On−1 , Σn , On }, n ≥ 0, such that hOi−1 , Σi , Oi i ∈ N for each i, with 1 ≤ i ≤ n. We denote by len(p) = n and last(p) = On the length of p and the last ontology on the path p. By paths(N , O) we denote the set of paths that originate in O. For every symbol X ∈ sig (N ) and every import path p in N , take a distinct symbol Xp of the same type (concept name, role name, or individual) not occurring in sig (N ). For each import path p in N , define a renaming θp of symbols in sig (N ) inductively as follows. If len(p) = 0, we set θp (X) = X for every X ∈ sig (N ). Otherwise, p = p0 ∪ {On−1 , Σn , On } for some path p0 and we define θp (X) = θp0 (X) if X ∈ Σn and θp (X) = Xp otherwise. A renamed import closure of an ontology O in S N is defined by Õ = p∈paths(N ,O) θp (last(p)). Lemma 11. If I |= Õ then I |=N O and for every I |=N O there exists J |= Õ such that J =sig (N ) I. Theorem 7. Let N be an ontology network, O an ontology in N , and α an axiom such that sig (α) ⊆ sig (N ). Then O |=N α iff Õ |= α. Theorem 7 provides a method for reducing the entailment problem in ontology net- works to entailment from ontologies. Note that, in general, the renamed closure Õ of an ontology O in a (cyclic) network N can be infinite (even if N and all ontologies in N are finite). There are, however, special cases when Õ is finite. For example, if all import signatures in N include all symbols in sig (N ), then it is easy to see that Õ is equiva- lent to the union of ontologies appearing in N . Õ is also finite if paths(N , O) is finite, e.g., if N is acyclic. In this case, the size of Õ is at most exponential in O. If there is at most one import path between every pair of ontologies (i.e., if N is tree-shaped) then the size of Õ is the same as the size of N . This immediately gives the upper complexity bounds on deciding entailment in acyclic networks. Theorem 8. Let L be a DL with the complexity of entailment in [co][N]TIME(f (n)) ([co] and [N] denote possible co- and N-prefix, respectively). Let N be an acyclic on- tology network and O an ontology in N such that Õ is a L-ontology. Then for L-axioms α, the entailment O |=N α is decidable in [co][N]TIME(f (2n )). If N is tree-shaped then deciding O |=N α has the same complexity as entailment in L. The next theorem is proved by the compactness theorem for First-Order Logic by showing that the renamed import closure of an ontology is recursively enumerable. Theorem 9. Let L be a DL, which can be translated to FOL, N an ontology network, and O an ontology in N such that Õ is a L-ontology. Then for L-axioms α, the entail- ment O |=N α is semi-decidable. 6 Conclusions We have introduced a new mechanism for ontology integration based on semantic import relations between ontologies. Reasoning over ontologies with semantic imports can be reduced to reasoning over the union of ontologies obtained as ‘copies’ of ontolo- gies from the import closure under an injective renaming of signature symbols. We have shown that this gives an upper bound on the complexity of reasoning with acyclic se- mantic imports, which is one exponential harder than entailment in the underlying DLs, from EL to SROIQ. Our hardness results demonstrate that the increased complexity of reasoning is unavoidable. When cyclic imports are allowed, the complexity jumps to undecidability, even if every ontology in a combination is given in the DL EL. These complexity results are shown for situations when the imported symbols include roles. It is natural to ask whether the complexity drops when only concept names are imported. The second parameter which may influence the complexity of reasoning is the semantics which is ‘imported’. In the proposed mechanism, importing the semantics of symbols is implemented via agreement of models of ontologies. One can consider refinements of this mechanism, e.g., by carefully selecting the classes of models of ontologies which must be agreed. The third way to decrease the complexity is to restrict the language in which ontologies are formulated. We conjecture that reasoning with cyclic imports is decidable for ontologies formulated in the family of DL-Lite. Acknowledgements The second author acknowledges support of German Research Foundation within the Transregional Collaborative Research Center SFB/TRR 62 Companion-Technology for Cognitive Technical Systems, while working at the Institute of Artificial Intelli- gence, University of Ulm, and support of RSF Grant No. 17-11-01176, while working at the Institute of Informatics Systems, Novosibirsk State University. References 1. Bao, J., Voutsadakis, G., Slutzki, G., Honavar, V.: Package-based description logics. In: Mod- ular Ontologies, pp. 349–371 (2009) 2. Borgida, A., Serafini, L.: Distributed description logics: Assimilating information from peer sources. J. Data Semantics pp. 153–184 (2003) 3. Euzenat, J., Zimmermann, A., de Freitas, F.L.G.: Alignment-based modules for encap- sulating ontologies. In: Proceedings of the 2nd International Workshop on Modular On- tologies, WoMO 2007, Whistler, Canada, October 28, 2007 (2007), http://ceur-ws.org/Vol- 315/paper4.pdf 4. Grau, B.C., Motik, B.: Reasoning over ontologies with hidden content: The import-by-query approach. J. Artif. Intell. Res. (JAIR) pp. 197–255 (2012) 5. Grau, B.C., Parsia, B., Sirin, E.: Ontology integration using epsilon-connections. In: Modular Ontologies, pp. 293–320 (2009) 6. Homola, M., Serafini, L.: Towards formal comparison of ontology linking, mapping and im- porting. In: Description Logics (2010) 7. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Proc. 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’08). pp. 274–284. AAAI Press (2008) 8. Pan, J.Z., Serafini, L., Zhao, Y.: Semantic import: An approach for partial on- tology reuse. In: Haase, P., Honavar, V., Kutz, O., Sure, Y., Tamilin, A. (eds.) WoMO. CEUR Workshop Proceedings, vol. 232. CEUR-WS.org (2006), http://dblp.uni- trier.de/db/conf/semweb/womo2006.html