Import-by-Query: Ontology Reasoning under Access Limitations

1 Introduction

The Web Ontology Language (OWL) and its revision OWL 2 are widely used ontology languages whose formal underpinnings are provided by description logics (DLs) [Baader et al., 2007]-a family of knowledge representation formalisms with well-understood formal properties. Ontologies are used, for example, in several countries to describe electronic patient records (EPR). In such a system, patients' data typically involves ontological descriptions of human anatomy, medical conditions, drugs and treatments, and so on. The latter domains have already been described in well-established reference ontologies such SNOMED-CT and GALEN. In order to save resources, increase interoperability between applications, and rely on experts' knowledge, an EPR application should preferably reuse these reference ontologies.

For example, assume that some reference ontology Kh describes concepts such as the "ventricular septum defect." An EPR application might reuse the concepts and roles from Kh to define its own ontology Kv of concepts such as "patients having a ventricular septum defect." It is generally accepted that ontology reuse should be modular-that is, the axioms of Kv should not affect the meaning of the symbols reused from Kh [Lutz et al., 2007; Cuenca Grau et al., 2008].

To enable reuse, OWL allows Kv to import Kh. OWL reasoners deal with imports by internally merging the axioms of the two ontologies; thus, to process Kv ∪Kh, an EPR application would require physical access to the axioms of Kh.

The vendor of Kh, however, might be reluctant to distribute the axioms of Kh, as doing this might allow the competitors to plagiarize Kh. Moreover, Kh might contain information that is sensitive from a privacy point of view and should not be shared. Finally, the vendor of Kh might impose different costs for reusing parts of Kh. To reflect this situation, we say that Kh is hidden and, by analogy, Kv is visible.

This problem could be addressed if Kh were made accessible via an oracle (i.e., a limited query interface), thus allowing Kv to import Kh "by query." In this paper, we study import-by-query algorithms, which can answer questions about Kv ∪ Kh by accessing only Kv and the oracle. We focus on schema reasoning problems, such as concept subsumption and satisfiability, which are useful during ontology development; this is in contrast to the information integration [Lenzerini, 2002] and peer-to-peer [Calvanese et al., 2004] scenarios, which focus on the reuse of data.

We proceed as follows. In Section 3 we formalize the import-by-query problem and fix the appropriate query language. Then, in Section 4 we show that no import-by-query algorithm exists in general even if Kv and Kh are expressed in the light-weight description logic EL [Baader et al., 2005]. In Section 5, we present such an algorithm for the case when Kv reuses only atomic concepts from Kh, and this is done in a modular way. Under certain assumptions, our algorithm is worst-case optimal; however, it is unlikely to be suitable for practice. Therefore, for the case when Kh is expressed in a Horn DL [Hustadt et al., 2005], we present a practical algorithm that extends the state-of-the-art tableaux algorithms [Kutz et al., 2006]. Finally, in Section 6 we extend our results to the case when Kv also reuses roles fromKh, but this is done in a syntactically restricted way. Our results may also increase the performance of reasoning: if Kv is non-Horn but Kh is, then Kv ∪Kh can be reasoned with by applying a general-purpose tableau algorithm only to Kv and using a more efficient algorithm for Kh.

2 Preliminaries

The formal underpinnings of OWL 2 are provided by the DL SROIQ [Kutz et al., 2006]. The syntax of SROIQ is defined w.r.t. a signature Σ, which is the union of disjoint countable sets of atomic concepts, atomic roles, and individuals. A role is either an atomic role or an inverse role R- for R an atomic role. For R and Ri roles, a role inclusion axiom has the form R1 . . .Rn ⊑ R, and a role disjointness axiom has the form Dis(R1,R2). The set of concepts is the smallest set containing ⊤, A, {a}, ¬C, C1 ⊓ C2, ∃R.C, ∃R.Self, and ⩾nR.C, for A an atomic concept, a an individual, C, C1, and C2 concepts, R a role, and n a nonnegative integer. Concepts of the form {a} are called nominals. Furthermore, ⊥ is an abbreviation for ¬⊤, C1 ⊔C2 for ¬(¬C1 ⊓¬C2), ∀R.C for ¬(∃R.¬C), and ⩽nR.C for ¬(⩾n+1R.C). A concept inclusion axiom has the form C1 ⊑ C2 for C1 and C2 concepts, and a concept equivalence C1 ≡ C2 is an abbreviation for C1 ⊑ C2 and C2 ⊑ C1. A TBox T is a finite set of concept inclusion, role inclusion, and role disjointness axioms. An assertion has the form C(a), R(a, b), or a ̸≈ b, for C a concept, R a role, and a and b individuals. An ABox A is a finite set of assertions. A SROIQ knowledge base is a pair K = 〈T , A〉 where T is a TBox and A is an ABox. By a suitable syntactic test, certain roles in K can be identified as being simple. To ensure decidability of reasoning, the role axioms in T must satisfy a syntactic restriction which we omit for brevity, and simple roles must not occur in ⩾nR.C, ∃R.Self, and role disjointness axioms. The definition of SROIQ by [Kutz et al., 2006] provides other constructs, all of which are expressible by the ones presented above.

A interpretation I = (△I , ·I ) consists of a nonempty domain set △I and a function ·I that assigns an object aI ∈ △I to each individual a, a set AI ⊆△I to each atomic concept A, and a relation RI ⊆△I ×△I to each atomic role R. Table 1 defines the extension of ·I to roles and concepts, and the satisfaction of axioms in I. An interpretation I is a model of K, written I |= K, if I satisfies all axioms in K; if such I exists, then K is satisfiable. A concept C is satisfiable w.r.t. K if a model I of K exists such that CI ̸= ∅. A nonempty set of interpretations S is compatible if for each I1, I2 ∈ S we have △I1 = △I2 and aI1 = aI2 for each individual a; the intersection of such S is defined in the obvious way.

SRIQ is obtained from SROIQ by disallowing nominals. EL [Baader et al., 2005] supports only concepts of the form ⊤, ⊥, A, C1 ⊓ C2, and ∃R.C for A an atomic concept and R an atomic role, and it supports no axioms about roles. Significant effort has been devoted to the development of DL languages with good computational properties, such as EL, DL-Lite [Calvanese et al., 2007], and Horn-SHIQ [Hustadt et al., 2005]. Each knowledge base K expressed in one of these languages is Horn in the sense that the intersection of every compatible set of models of K is also a model of K.

For α a concept, a role, an axiom, or a knowledge base, sig(α) is the signature of α-that is, the set of atomic concepts, atomic roles, and individuals occurring in α. A position p is a finite sequence of integers. The empty position is denoted with ϵ. If a position p1 is a proper prefix of a position p2, then and p1 is above p2, and p2 is below p1. The subterm α|p of a concept or axiom α at a position p is defined as follows: α|ϵ = α; (C1 ▷◁ C2)|ip = Ci|p for ▷◁ ∈ {⊓, ⊑} and i ∈ {1, 2}; and α|1p = C|p for α of the form ¬C, ∃R.C, ⩾nR.C, or C(a). The concept closure cls(K) of K = 〈T ,A〉 is the smallest set that contains all subterms of ¬C ⊔ D for each C ⊑ D ∈ T and of C for each C(a) ∈ A.

3 Importing Ontologies by Query

To illustrate the notion of import-by-query, Table 2 shows a reference knowledge base Kh whose axioms are to be kept hidden, but that is reused in a visible knowledge base Kv. The hidden knowledge base Kh provides concepts describing organs such as Heart, and medical conditions such as CHD (congenital heart defect), VSD (ventricular septum defect), and AS (aortic stenosis). Furthermore, the role cond relates organs to medical conditions and is used to define concepts such as CHD Heart (a heart with a congenital heart disorder) and VSD Heart (a heart with a ventricular septal defect). The shared symbols of Kh are written in bold font. In addition to these, Kh might contain nonshared symbols; however, for the sake of brevity, we do not show any axioms involving such symbols. The visible knowledge base Kv provides the concept Pat representing patients, and it defines various types of patients by relating the organs from Kh with the patients using the hasOrgan role. In addition, Kv extends the list of defects in Kh by EA (Ebstein's anomaly). The symbols private to Kv are written in italic font.

When reusing ontologies, it is commonly accepted that Kv should not affect the meaning of the symbols reused from Kh-that is, Kv ∪Kh |= α should imply Kh |= α for each axiom α containing only the reused symbols [Lutz et al., 2007; Cuenca Grau et al., 2008]. This is guaranteed if the TBox Tv of Kv is local w.r.t. the set Γ of concepts and roles imported fromKh-that is, if I |= Tv for each interpretation I in which, for each concept or role X ̸∈ Γ, we have XI = ∅. For example, δ1 is local w.r.t. {CHD Heart} because δ1 is satisfied in any interpretation that interprets the nonshared symbols as ∅. [Cuenca Grau et al., 2008] have shown how to check this condition using a DL reasoner.

To formalize the notion of import-by-query, we introduce the notion of a Γ-oracle, which is responsible for advertising the shared signature Γ of Kh and answering satisfiability of (not necessarily atomic) concepts w.r.t. Kh. Concept satisfiability is available in all DL reasoners known to us, so it provides us with a natural query language for Γ-oracles; we leave the investigation of richer query languages to future work.

Definition 1. Let Kbe aKB and Γ ⊆ sig(K) a signature. The Γ-oracle for K is the function ΩK defined for each concept C (in the same DL as K) with sig(C) ⊆ Γ such that ΩK(C) = t if C is satisfiable w.r.t. K, and ΩK(C) = f otherwise.

An import-by-query algorithm checks whether Kv ∪ Kh is satisfiable; other relevant reasoning problems, such as concept subsumption, can be solved using the well-known transformations. The notion of an algorithm in the following definition can be made precise using a formal computation model such as Turing machines in the obvious way.

Definition 2. An import-by-query algorithm takes a Γ-oracle ΩKh and a KB Kv with sig(Kv) ∩ sig(Kh) ⊆ Γ as input, and it terminates after a finite number of computation steps returning t iff Kv ∪Kh is satisfiable.

4 The Limits of Import-by-Query Reasoning

We next show that no import-by-query algorithm exists even for a light-weight DL such as EL.

Theorem 1. No import-by-query algorithm exists if Kv and Kh are in EL, Γ is allowed to contain at least one atomic role, and the TBox of Kv is local in Γ.

Proof. Consider an application of an import-by-query algorithm to Kv given in (1) and Γ = {R}. Clearly, the TBox of Kv is local in Γ. Since the algorithm terminates on all inputs, the number of questions posed to any Γ-oracle is bounded by some integer m and, consequently, the quantifier depth of each concept C passed to the Γ-oracle is bounded by an integer n, where both m and n depend only on Γ and Kv . Let K1h and K2h be as in (2) and (3), respectively.

For each EL concept C of quantifier depth at most n with sig(C) ⊆ Γ, we have K1h |= C ⊑ ⊥ iff K2h |= C ⊑ ⊥, so ΩK1h (C) = ΩK2h (C). Thus, when applied to Kv and ΩK1h , the algorithm returns the same value as when it is applied to Kv and ΩK2h . Since Kv ∪K1h is satisfiable but Kv ∪K2h is not, the algorithm does not satisfy Definition 2.

5 Importing Atomic Concepts

The proof of Theorem 1 relies on the fact that Kv reuses a role from Kh. We now present an import-by-query algorithm for the case when no role is reused. In our example, this allows one to express axioms δ1, δ2, and δ5, which, together with Kh, allow us to conclude VSD Pat ⊑ CHD Pat .

5.1 InterfacingModels Point-Wise

The following definition identifies valid inputs for our algorithm. In particular, we allow Kv to be any OWL 2 ontology that reuses the symbols of Kh in a local way; however, we disallow the usage of nominals in Kh for technical reasons.

Definition 3. Let Kv = 〈Tv, Av〉 and Kh = 〈Th, Ah〉 be KBs such that Γ = sig(Kv) ∩ sig(Kh) contains only atomic concepts. Then, Kh is safe for import-by-query into Kv if Kv is in SROIQ, Kh is in SRIQ, and Tv is local w.r.t. Γ.

Our core observation is that a model of Kv ∪Kh can be obtained by taking a model I of Kv and extending it at each point x ∈ △I with a fresh model Jx of Kh that contains a point y ∈ △Jx such that x and y coincide on the interpretation of the concepts in Γ. This is a consequence of the fact that (i) Kv uses the concepts from Γ in a local way, and (ii) Kh does not contain nominals, so the union of all models Jx is also a model of Kh. To formalize this idea, we use the following notion: for S = {D1, . . . ,Dn} a nonempty finite set of concepts, a selection w.r.t. S is a concept of the form L1 ⊓ . . . ⊓Ln where each Li is either Di or ¬Di; furthermore, ⊤ is the only selection w.r.t. S = ∅.

Lemma 1. Let Kh be safe for import-by-query into Kv, and let Γ = sig(Kv) ∩ sig(Kh). Then, Kv ∪Kh is satisfiable iff a model I of Kv exists such that ΩKh (C) = t for each selection C w.r.t. Γ such that CI ̸= ∅.

Proof. (⇒) If I is a model of Kv ∪Kh, then clearly I |= Kv, and ΩKh (C) = t for each selection C w.r.t. Γ with CI ̸= ∅.

(⇐) Let I = (△I , ·I ) be a model of Kv and consider each x ∈ △I and the selection C w.r.t. Γ such that x ∈ CI . Since ΩKh (C) = t, an interpretation Jx = (△Jx , ·Jx ) exists such that Jx |= Kh and y ∈ CJx for some y ∈ △Jx . W.l.o.g. we assume that y = x; △Jx ∩△I = {x}; △Jx1 ∩△Jx2 = ∅ for each x1, x2 ∈ △I with x1 ̸= x2; and XJx = ∅ for each X ∈ sig(Kv) \ Γ. Let M = (△M , ·M ) be such that

XM = ⋃ x∈△I XJx for each atomic concept or role X, and

aM = aJx for each individual a and some (arbitrarily chosen) interpretation Jx.

SRIQ does not allow for nominals, so it is invariant under disjoint unions-that is, the union of any number of disjoint models of Kh is also a model of Kh [Baader et al., 2002]; thus, M |= Kh. Furthermore, since Tv is local in Γ, we have M |= Tv ∪Kh. Finally, let N = (△N , ·N ) be an interpretation defined by △N = △M and

Algorithm 1 Import-by-Query Algorithm

Algorithm: ibq(Kv,ΩKh , S)

Inputs: a knowledge base Kv, a Γ-oracle ΩKh , and a set of concepts S over the signature Γ

• 1 Compute the set N of all axioms of the form C ⊑ ⊥ such that C is a selection w.r.t. S with ΩKh (C) = f.
• 2 Return t iff the SROIQ knowledge base Kv ∪N is satisfiable.

N and M have the same domains and they coincide on the interpretation of the symbols in sig(Kh), so N |= Kh. To show that N |= Kv, we first prove the following claim (⋆): for each C ∈ cls(Kv), we have CN = CI ∪ (CM \△I ). The proof of (⋆) is by induction on the structure of concepts, so consider each C ∈ cls(Kv).

If C is an atomic concept with C ∈ Γ, then by the definition of M we have CI = CM ∩ △I , so CI ∪ (CM \ △I ) = (CM ∩△I ) ∪ (CM \△I ) = CM ; by the definition of N, we have CM = CN , which implies (⋆).

If C is a nominal or an atomic concept with C ̸∈ Γ, then CM = ∅ and CN = CI , which trivially imply (⋆).

If C = ¬D, then CN = (△I ∪ (△M \△I )) \DN = (△I \ DN ) ∪ ((△M \ △I ) \ DN ). By applying the induction hypothesis, the first disjunct reduces to △I \DI , and, since, △M \DN = △M \ (DI ∪ (DM \△I )) = (△M \DI ) \ (DM \△I ) = △M \DM , the second one reduces to (△M \DM ) \△I . But then, (⋆) holds.

If C = D1 ⊓ D2, then CN = DN 1 ∩DN 2 , which is equal to (DI1 ∪ (DM 1 \△I )) ∩ (DI2 ∪ (DM 2 \△I )) by the induction hypothesis; but (DM 1 \△I ) ∩DI2 = (DM 2 \△I ) ∩DI1 = ∅, so CN = (DI1 ∩ DI2 ) ∪ ((DM 1 \△I ) ∩ (DM 2 \△I )); finally, (DM 1 \△I ) ∩ (DM 2 \△I ) = (DM 1 ∩DM 2 ) \△I .

If C = ⩾nR.D or C = ∃R.Self, since R ̸∈ sig(Kh), we have RM = ∅ and CM = ∅; furthermore, RN = RI and DI ⊆DN by the induction hypothesis, so CN = CI . This completes the proof of (⋆).

Consider now each axiom α in Kv. For α a concept inclusion axiom, we assume w.l.o.g. that it is of the form ⊤ ⊑ C. By (⋆), CN = CI ∪ (CM \△I ). Since I |= α, we have CI =△I ; furthermore, since Tv is local w.r.t. Γ, we have M |= α, so CM = △M ; thus, CN = △N , so N |= α. For α a role assertion, a role inclusion, or a role disjointness axiom, we have N |= α because N coincides with I on the interpretation of all roles from sig(Kv). For α = C(a), we have aN ∈ CN by (⋆) and a ̸∈ Γ. Finally, for α = a ̸≈ b, we have aN ̸= bN because {a, b} ∩ Γ = ∅. Thus, N |= Kv.

Lemma 1 motivates Algorithm 1.

Theorem 2. Let Kh be safe for import-by-query into Kv, Γ = sig(Kv) ∩ sig(Kh), and ΩKh the Γ-oracle for Kh. Then, ibq(Kv, ΩKh , Γ) is an import-by-query algorithm, and it can be implemented such that it runs in N2EXPTIME with an exponential number of calls to ΩKh .

Proof. That ibq(Kv,ΩKh , Γ) is an import-by-query algorithm is a direct consequence of Lemma 1. Furthermore, the number of selections w.r.t. Γ is exponential in the size of Γ, so N can be computed by an exponential number of calls to ΩKh . Let ria(·) be the transformation by [Kazakov, 2008] for eliminating role inclusion axioms from SROIQ KBs. Then, ria(Kv) is equisatisfiable with and exponentially larger than Kv [Kazakov, 2008]. Furthermore, N contains the same concepts as ria(Kv) and no role inclusions axioms, so ria(Kv ∪N) = ria(Kv) ∪N = K′ . Thus, K′ is equisatisfiable with and exponentially larger than Kv. We can check satisfiability of K′ by transforming K′ polynomially into an equisatisfiable formula ϕ of the two-variable fragment with counting, and deciding the satisfiability of ϕ in NEXPTIME [Pratt-Hartmann, 2005]. Clearly, the overall algorithm runs in N2EXPTIME with exponentially many calls to ΩKh .

5.2 Importing Horn Ontologies

Algorithm 1 is unlikely to be suitable for practice because Step 1 is exponential in the size of Γ. In this section, we present a practical algorithm for the case when Kh is Horn. 1 This algorithm calls the Γ-oracle "on demand," which makes it "more goal-oriented." The correctness of the algorithm is based on the following observation about Horn KBs.

Proposition 1. Let K be a Horn knowledge base, C a conjunction of atomic concepts, and A1, . . . , An atomic concepts such that C ⊓ ¬Ai is satisfiable w.r.t. K for each 1 ≤ i ≤ n. Then, C ⊓ ¬A1 ⊓ . . . ⊓ ¬An is satisfiable w.r.t. K as well.

Proof. Let Ki = K∪ {C(a), ¬Ai(a)} for 1 ≤ i ≤ n and a an individual not occurring in K. Let Ii be a model of each Ki; w.l.o.g. we assume that the set S = {Ii | 1 ≤ i ≤ n} is compatible (e.g., we can select Ii to be Herbrand models of Ki). Let J be the intersection of S. Since K is Horn, we have J |= K. Furthermore, aJ ∈ CJ and aJ ̸∈ AJi for each 1 ≤ i ≤ n; therefore, aJ ∈ (C ⊓ ¬A1 ⊓ . . . ⊓ ¬An)J .

We extend the tableau algorithms used in many state-ofthe-art DL reasoners. Our extension, however, is largely independent from the intricacies of these algorithms, so we introduce an abstraction of a tableau algorithm as a tuple T = 〈C, R〉 with the following structure.

• C assigns to each ABox A a value from {t, f} such that C(A) = t only if A is unsatisfiable. A contains a clash if C(A) = t; otherwise, A is clash-free.
• R is a set of derivation rules, where each ρ ∈ R assigns to each pair (T ,A) a set of n-tuples of ABoxes (tuples in this set can vary in arity). A rule ρ is applicable to T and A if ρ(T , A) ̸= ∅.

A derivation for K = 〈T ,A〉 by T = 〈C, R〉 is a pair 〈Θ, σ〉 where Θ is a finitely branching tree and σ labels each node v of Θ with an ABox σ(v) such that (i) σ(v) = A for v the root of Θ; (ii) if C(σ(v)) = t or no derivation rule in R is applicable to (T , σ(v)), then v is a leaf of Θ; (iii) if C(σ(v)) = f and a derivation rule in R is applicable to (T , σ(v)), then v has children v1, . . . , vn such that 〈σ(v1), . . . , σ(vn)〉 ∈ ρ(T , σ(v)) for some (arbitrarily chosen) derivation rule ρ ∈ R.

T is terminating if, for each K, each derivation for K by T can be constructed using finitely many steps. T is sound if, for each model I of each 〈T ,A〉, each derivation rule ρ ∈ R, and each 〈A1, . . . ,An〉 ∈ ρ(T ,A), an interpretation I ′ exists such that XI = XI ′ for each X ̸∈ sig(Ai) \ sig(A), and I ′ |= 〈T ,Ai〉 for some 1 ≤ i ≤ n. T is complete if a partial function M mapping ABoxes to interpretations exists such that, in each derivation (Θ, σ) for K by T, and for each leaf v of (Θ, σ) such that A′ = σ(v) is clash-free, the value of M(A′ ) is defined and M(A′ ) |= K. Furthermore, we assume that M(A′ ) = (△I , ·I ) always satisfies the following property (♦): for each conjunction of atomic concepts C = A1 ⊓ . . . ⊓ An such that CI ̸= ∅ and (C ⊓ B)I = ∅ for each atomic concept B not occurring in C, an individual s exists such that Ai(s) ∈ A′ for each 1 ≤ i ≤ n, and B(s) ̸∈ A′ for each atomic concept B not occurring in C. Intuitively, (♦) ensures that conjunctive concepts are interpreted in M(A′ ) in accordance with their instantiations in A′ . Most tableau algorithms used in practice are sound, complete, and terminating; furthermore, all such algorithms known to us satisfy (♦).

1 From the infrastructure point of view, the Γ-oracle for Kh should indicate to clients if Kh is (known to be) Horn.

We now show how to extend T to an import-by-query algorithm for the case when Kh is Horn.

Definition 4. Let T = 〈C, R〉 be a sound, complete, and terminating tableau algorithm, Γ a set of atomic concepts, and ΩKh a Γ-oracle. The tableau algorithm TΓ,ΩKh is obtained by extending T with the ask-rule as follows: ask(T , A) is defined for each (T ,A) as the smallest set such that, for each individual s in A, the concept C obtained as the conjunction of all Ai ∈ Γ with Ai(s) ∈ A, and each B ∈ Γ ∪ {⊥} with ΩKh (C ⊓ ¬B) = f, we have

Intuitively, the ask-rule deterministically adds B(s) to each ABox that contains assertions A1(s) . . . ,An(s) such that Kh |= A1 ⊓ . . . ⊓An |= B.

Theorem 3. Let Kh = 〈Th,Ah〉 be a Horn knowledge base that is safe for import-by-query into Kv = 〈Tv,Av〉, let Γ = sig(Kv) ∩ sig(Kh), let ΩKh be the Γ-oracle for Kh, and let T be a sound, complete, and terminating tableau algorithm. Then, TΓ,ΩKh satisfies the following two claims:

1. if Kv ∪Kh is satisfiable, then each derivation for Kv by TΓ,ΩKh contains a branch on which all nodes are labeled with clash-free ABoxes; and
2. if a derivation for Kv by TΓ,ΩKh contains a leaf labeled with a clash-free ABox, then Kv ∪ Kh is satisfiable.

Proof. (Claim 1) Assume that I is a model of Kv ∪Kh, and consider each derivation for Kv by TΓ,ΩKh . We assume w.l.o.g. that the derivation rules of TΓ,ΩKh do not introduce assertions involving symbols from sig(Kh) \ Γ. Consider now the tuple 〈A1, . . . ,An〉 obtained from Av by an application of a derivation rule of TΓ,ΩKh . If the derivation rule is from T, since T is sound, I can be extended to a model I ′ of some 〈Tv,Ai〉; since this extension does not involve the symbols in sig(Kh), we have I ′ |= Kh as well. For the ask-rule, n = 1 and sI ∈ CI , so ΩKh (C ⊓ ¬B) = f implies sI ∈ BI and I |= 〈Tv,A1〉 ∪Kh. By repeating this claim inductively, we conclude that the derivation contains a branch on which each node is labeled with an ABox A′ such that 〈Tv,A′ 〉 ∪Kh is satisfiable; thus, each A′ is clash-free.

(Claim 2) Let A′ be a clash-free ABox labeling a leaf of a derivation for Kv by TΓ,ΩKh , and let M(A′ ) = (△I , ·I ). Furthermore, let C be a selection w.r.t. Γ such that CI ̸= ∅, and let D be the conjunction of all atomic concepts that occur positively in C. By (♦) and the fact that C is maximal, an individual s in A exists such that Ai(s) ∈ A′ for each Ai in D, and Bj(s) ̸∈ A′ for each atomic concept Bj, 1 ≤ j ≤ n that occurs negatively in C. Since the ask-rule is not applicable to A′ , then D ⊓ ¬Bj is satisfiable w.r.t. Kh for each 1 ≤ j ≤ n. Since Kh is Horn, by Proposition 1 we have that D⊓¬B1 ⊓ . . . ⊓¬Bn = C is satisfiable w.r.t. Kh as well. But then, Kv ∪Kh is satisfiable by Lemma 1.

Each derivation for Kv by TΓ,ΩKh is clearly finite. Furthermore, the value of ask(T ,A) can be determined by asking ΩKh (C) for each selection C w.r.t. Γ occurring in A. Therefore, a derivation for Kv by TΓ,ΩKh can be constructed by a finite number of steps, which provides us with an import-byquery algorithm. Such an algorithm may, in the worst case, make an exponential number of calls to the oracle; however, such calls are made as needed, which makes this algorithm more amenable to implementation than Algorithm 1.

6 Importing Atomic Roles

We now extend the results from Section 5 and allow the reuse of roles under the following syntactic restriction.

Definition 5. For Γ a set of atomic concepts and roles, we say that a concept is Γ-modal if it is of the form ∃R.Self, ∃R.C, or ⩾nR.C, for R ∈ Γ.

Let Kv and Kh be KBs such that Γ = sig(Kv) ∩ sig(Kh) contains both concepts and roles. Then, Kh is safe for importby-query into Kv if, in addition to the conditions from Definition 3, roles from Γ do not occur in role inclusion and disjointness axioms in Kv; for each ∃R.Self or ⩾nR.C in Kv, if R ∈ Γ then R is simple in Kh; and sig(C) ⊆ Γ for each Γ-modal concept C ∈ cls(Kv).

For satisfiability of Kv ∪Kh to be decidable, only simple roles from Kh can occur in certain concepts in Kv [Horrocks et al., 2000]. Thus, the Γ-oracle for Kv should also advertise to clients which roles in Γ are simple. This is a syntactic check that is provided by most DL reasoners.

In our example, Definition 5 allows us to express δ3: the role cond from Kh occurs in a Γ-modal concept ∃cond.AS, but AS is fromKh as well. This is in contrast to δ4, in which ∃cond.EA contains EA that is not from Kh. Note that δ1, δ3, and Kh allow us to conclude AS Pat ⊑ CHD Pat .

By using the appropriate set S, Algorithm 1 is an importby-query algorithm for the case of shared roles as well. In the following theorem, we say that position p in a concept or axiom α is Γ-outermost if α|p is a Γ-modal concept, and α|q is not a Γ-modal concept for each position q above p.

Theorem 4. Let Kv, Γ, and ΩKh be as in Theorem 2 with the difference that Γ can also contain atomic roles, and let

S = {A ∈ Γ | A is an atomic concept} ∪ {α|p | α ∈ Kv and p is Γ-outermost in α}.

Then, ibq(Kv,ΩKh , S) is an import-by-query algorithm, and it can be implemented such that it runs in N2EXPTIME with an exponential number of calls to ΩKh .

Proof. Let QD be a fresh atomic concept uniquely associated with each D ∈ S. Furthermore, let K′v be the knowledge base obtained from Kv by replacing in each axiom α ∈ Kv the concept α|p with Qα|p for each Γ-outermost position p in α. Also, let K′h be obtained from Kh by adding the axiom QC ≡ C for each C in S. Finally, let Γ′ = sig(K′v ) ∩ sig(K′h ), and let ΩK′h be the Γ′ -oracle such that ΩK′h (C1) = ΩKh (C2) for each C1 and C2 where C2 is obtained from C1 by replacing all QD with D. Since Kv satisfies the condition from Definition 5 and Γ′ contains only atomic concepts, K′h , K′v , and ΩK′h satisfy the preconditions of Theorem 2. Furthermore, it is obvious that ibq(K′v ,ΩK′h , Γ′ ) = ibq(Kv,ΩKh , S), so the latter is an import-by-query algorithm. The proof for the algorithm's running time is the same as in Theorem 2.

When each Γ-modal concept C occurring in Kv is Horn [Hustadt et al., 2005], the tableau algorithm from Definition 4 can be extended to the case when Γ contains roles by using the set S from Theorem 4 instead of Γ in the ask-rule.

Finally, the results from this section can be extended to the case when Kv contains concepts of the form ⩾nR.D with R ∈ Γ and sig(D) ̸⊆ Γ, provided that the unfolding of D in Kv and results in a concept containing only symbols from Γ. In our example, the nonshared symbol EA in δ4 can be unfolded with its definition in δ5, resulting in EA Pat ≡ Pat ⊓ ∃hasOrgan .(Heart ⊓ ∃cond.CHD); after this preprocessing step, we can use the import-by-query algorithm to conclude EA Pat ⊑ CHD Pat .

7 RelatedWork

In a peer-to-peer setting, [Calvanese et al., 2004] consider the problem of answering a query q over two KBs Kv and Kh with disjoint signatures and a set M of mappings of the form qh ⇝ qv by reformulating q as queries that can be evaluated over Kv and Kh in isolation. The query reformulation algorithm accesses only Kv and M; thus, q can be answered by means of an oracle for Kh. In such a setting, however, a satisfiable Kh cannot affect the subsumption of concepts in Kv. Consider the following example:

Now Kh ∪Kv ∪M̸|= Cv ⊑ Av, since the mappings in M are unidirectional. Thus, whereas [Calvanese et al., 2004] consider simple schemas (i.e., both Kh and Kv must be in DL-Lite) and conjunctive query answering, we focus on rich TBoxes and schema reasoning.

[Baader et al., 2002] study the transfer of decidability results when combining decidable logics. In particular, they show how to integrate algorithms that decide satisfiability of Kv and Kh independently into an algorithm that decides satisfiability of Kv ∪ Kh, provided that the two KBs do not share roles and do not contain nominals. This situation is similar to the one in Section 5, with the difference that we allow Kv to contain nominals but require it to be local in Γ.

8 Conclusion

In this paper, we have studied the problem of importing an ontology without knowing its axioms. We have shown that this problem does not have a general solution. Furthermore, we have identified solvable cases, for which we have presented two algorithms. In future work, one might consider relaxing the syntactic restrictions on the usage of roles, particularly if one were to extend the query language of the oracle.