When Are Description Logic Knowledge Bases Indistinguishable?

1 Introduction

A description logic (DL) knowledge base (KB) consists of a terminological box (TBox) and an assertion box (ABox). The TBox represents conceptual knowledge by providing a vocabulary for a domain of interest together with axioms that describe semantic relationships between the vocabulary items. To illustrate, the following toy TBox, Ta, defines a vocabulary for the automotive industry:

Minivan ⊑ Automobile, Hybrid ⊑ Automobile,

Automobile ⊑ ∃poweredBy.Engine,

Hybrid ⊑ ∃poweredBy.EEngine ⊓ ∃poweredBy.ICEngine,

EEngine ⊑ Engine, ICEngine ⊑ Engine.

For example, the first two axioms say that minivans and hybrids are automobiles; the third axiom claims that every automobile is powered by an engine. Thus, the TBox introduces, among others, concept names (sets) Minivan, Automobile and Engine, states that the concept Minivan is subsumed by the concept Automobile and uses the role name (binary relation) poweredBy to say that automobiles are powered by engines. The last two axioms state that electric and internal combustion engines are engines. TBoxes are often called ontologies and presented in applications in terms of the Web Ontology Language OWL 2, which is underpinned by DLs.

The ABox of a KB is a set of facts storing data about the concept and role names introduced in the TBox. An example ABox, Aa, in the automotive domain is given by Hybrid(toyota highlander), Minivan(toyota highlander), Minivan(nissan note).

∗This paper was invited for submission to the Best Papers From Sister Conferences Track, based on a paper that appeared in the Proc. of the 14th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2014).

Typical applications of KBs in modern information systems use the semantics of concepts and roles in the TBox to enable the user to query the data in the ABox. This is particularly useful if the data is incomplete or comes from heterogenous data sources which is the case, for example, in linked data applications [Polleres et al., 2013] and large scale data integration projects [Poggi et al., 2008; Giese et al., 2013], or if the data comprises web content gathered by search engines using semantic markup [Hitzler et al., 2009].

As the data may be incomplete, the open world assumption is made when querying a KB K: a tuple a of individuals from K is a (certain) answer to a query q over K iff q(a) is true in every model I of K. As general first-order queries are undecidable under the open-world semantics, the basic and most important querying instrument is conjunctive queries (CQs), which are ubiquitous in relational database systems and form the core of the Semantic Web query language SPARQL. A CQ q(x) is a first-order formula ∃y ϕ(x, y), where ϕ(x, y) is a conjunction of atoms of the form A(z1) or P(z1, z2) for a concept name A, a role name P, and variables z1, z2 from x, y. 1 For instance, to find minivans powered by electric engines, one can use the following CQ:

Then toyota highlander is its only certain answer in (Ta, Aa).

The problem of answering CQs over KBs has been the focus of significant research in the DL community with deep complexity results for a large variety of DLs (see below), the introduction of new DLs for which query answering is tractable for data complexity [Hustadt et al., 2005; Calvanese et al., 2007], the invention of various query answering techniques [Calvanese et al., 2007; Lutz et al., 2009] and the development of powerful implemented systems; see, e.g., [Kontchakov and Zakharyaschev, 2014] and references therein.

Apart from developing query answering techniques, a major research problem is KB engineering and maintenance. In fact, with typically large data and often complex and tangled ontologies, tool support for transforming and comparing KBs is becoming indispensable for applications. To begin with, KBs are never static entities. Like most software artefacts, they are updated to incorporate new information, and distinct versions are introduced for different applications. Thus, developing support for KB versioning has become a major research problem [Jim´enez-Ruiz et al., 2011; Konev et al., 2012]. As dealing with a large and semantically tangled KB can be costly, one may want to extract from it a smaller module that is indistinguishable from the whole KB as far as the given application is concerned [Stuckenschmidt et al., 2009]. Another technique for extracting relevant information is forgetting, where the task is to replace a given KB by a new KB using only those concept and role names that are needed by the application but still providing the same information about those names as the original KB [Konev et al., 2009; Koopmann and Schmidt, 2014b]. Finally, the vocabulary of a given KB may not be convenient for a new application. In this case, similarly to data exchange in databases [Arenas et al., 2014]-where data structured under a source schema is converted to data under a target schema-one may want to transform a KB in a source signature to a KB given in a more useful target signature and representing the original KB in an accurate way. This task is known as knowledge exchange [Arenas et al., 2012; 2013].

1 Since we consider Horn DLs, the results of this paper actually apply to disjunctions (or unions) of CQs (UCQs). For simplicity, however, we concentrate on CQs only.

In this paper, we investigate a relationship between KBs that is fundamental for all such tasks if querying the data via CQs is the main application. Let Σ be a signature consisting of a set of concept and role names. We say that KBs K1 and K2 are Σ-query inseparable and write K1 ≡Σ K2 if any CQ formulated in Σ has the same answers over K1 and K2. Note that even for Σ containing all concept and role names in the KBs, Σ-query inseparability does not necessarily imply logical equivalence: e.g., (∅, {A(a)}) is {A,B}-query inseparable from ({B ⊑ A}, {A(a)}) but the two KBs are clearly not logically equivalent. Thus, if KBs are used for purposes other than querying data via CQs, then different notions of inseparability are required. We now discuss the applications of Σ-query inseparability for the tasks above in more detail.

Versioning. Version control systems for KBs provide a range of operations including, for example, computing the relevant differences between KBs, merging KBs and recovering KBs. All these operations rely on checking whether two versions, K1 and K2, of a KB are indistinguishable from the application point of view. If that application is querying the data using CQs over a given signature Σ, then K1 and K2 should be regarded as indistinguishable just in case they give the same answers to CQs in Σ. Thus, the basic task for a query-centric approach to KB versioning is to check whether K1 ≡Σ K2.

Modularisation. Modularisation and module extraction are major research topics in ontology engineering and maintenance. In module extraction, the problem is to find a (small) subset of the axioms of a given large KB that is indistinguishable from it with respect to the intended application. If that application is querying a KB K using CQs over a signature Σ, then the problem is to find a small Σ-query module of K, that is, a KB K′ ⊆ K with K′ ≡Σ K. Note that one can extract a minimal Σ-query module from a KB using a polynomial-time algorithm with the Σ-query inseparability check as an oracle. To illustrate the notion of Σ-query module, consider the automotive ontology Ka = (Ta,Aa) described above and the signature Σm = {Automobile, Engine, poweredBy}. Then Km = (Tm, Aa) is a Σm-query module of Ka, where Tm is Minivan ⊑ Automobile, Automobile ⊑ ∃poweredBy.Engine.

Knowledge Exchange. In knowledge exchange, we want to transform a KB K1 in a signature Σ1 to a KB K2 in a new signature Σ2 connected to Σ1 via a declarative mapping specification given by a TBox T12. Such mapping specifications between KBs are also known as ontology alignments or ontology matchings and have been studied extensively [Shvaiko and Euzenat, 2013]. If, as above, we are interested in querying data via CQs, then the target KB K2 should be a sound and complete representation of K1 w.r.t. querying data, and so satisfy the condition K1 ∪ T12 ≡Σ2 K2, in which case it is called a universal CQ-solution. To illustrate, consider again the ontology Ka = (Ta,Aa), and let Tae relate the signature Σa of Ka to Σe = {Car, HybridCar, ElectricMotor, Motor, hasMotor}:

Then Ke = (Te, Ae) is a universal CQ-solution, where

Te = { ElectricMotor ⊑ Motor, Car ⊑ ∃hasMotor.Motor, HybridCar ⊑ Car ⊓ ∃hasMotor.ElectricMotor },

Ae = { HybridCar(toyota highlander), Car(nissan note) }.

Forgetting. A KB K′ results from forgetting a signature Σ in a KB K if K′ ≡sig(K)\Σ K and sig(K′ ) ⊆ sig(K) \ Σ, where sig(K) is the signature of K. Thus, the result of forgetting Σ does not use Σ and gives the same answers to CQs without symbols in Σ as K. The result of forgetting is also called a uniform interpolant for K w.r.t. sig(K) \ Σ. Forgetting is of interest for a number of applications. Typically, when reusing an existing KB in a new application, only a small number of its symbols is relevant, and so instead of reusing the whole KB, one can take the potentially smaller KB resulting from forgetting the extraneous symbols. Forgetting can also be used for predicate hiding: if a KB is to be published, but some part of it has to be concealed from the public, then this part can be removed by forgetting its symbols [Cuenca Grau and Motik, 2012]. Finally, forgetting can be used for KB summary: the result of forgetting often provides a smaller and more focused ontology that summarises what the original ontology says about the retained symbols, potentially facilitating KB comprehension. To illustrate, for Σf = {Automobile, Engine, poweredBy}, the KB (Tf , Af ),

Tf = { Automobile ⊑ ∃poweredBy.Engine },

Af = { Automobile(toyota highlander),

Automobile(nissan note) },

is a result of forgetting sig(Ka) \ Σf in Ka.

We investigate the data and combined complexity of deciding Σ-query inseparability of KBs given in various fragments of the DL Horn-ALCHI [Kr¨otzsch et al., 2013], which include DL-LiteHcore [Calvanese et al., 2007; Artale et al., 2009], EL and ELH [Baader et al., 2005] underlying the OWL 2 profiles OWL 2 QL and OWL 2 EL. For all of these DLs, Σ-query inseparability turns out to be P-complete for data complexity, which matches the data complexity of CQ evaluation in all of our DLs lying outside the DL-Lite family. The obtained tight combined complexity results are summarised in the diagram below:

2 Horn-ALCHI and its Fragments

All the DLs considered in this paper are Horn fragments of ALCHI. To define them, we fix lists of individual names ai, concept names Ai, and role names Pi, for i < ω. A role is a role name Pi or an inverse role P - i ; we assume (P - i )- = Pi. ALCI-concepts, C, are defined by the grammar

where R is a role. We use ⊥, C1 ⊔ C2 and ∀R.C as abbreviations for ¬⊤, ¬(¬C1 ⊓ ¬C2) and ¬∃R.¬C, respectively. ALC-concepts are ALCI-concepts without inverse roles; EL-concepts are ALC-concepts without ¬. DL-Litehornconcepts are ALCI-concepts without ¬, in which C = ⊤ in every occurrence of ∃R.C. Finally, DL-Litecore-concepts are DL-Litehorn-concepts without ⊓; in other words, they are basic concepts of the form ⊤, Ai or ∃R (a shortcut for ∃R.⊤).

For a DL L, an L-concept inclusion (CI) takes the form C ⊑ D, where C and D are L-concepts. An L-TBox, T , contains a finite set of L-CIs. An ALCHI, DL-LiteHhorn and DL-LiteHcore TBox can also contain a finite set of role inclusions (RIs) R1 ⊑ R2, where the Ri are roles. In ALCH and ELH, TBoxes have RIs but without inverse roles. DL-Lite TBoxes also contain disjointness constraints B1 ⊓ B2 ⊑ ⊥ and R1 ⊓ R2 ⊑ ⊥, for basic concepts Bi and roles Ri. 2

To introduce the Horn fragments of these DLs, we require the following (standard) recursive definition [Hustadt et al.,

2 Although role disjointness constraints are not in the syntax of ALCHI, they play no essential part in our constructions, and the techniques we develop for ALCHI are also applicable to DL-Lite.

2005; Kazakov, 2009]: a concept C occurs positively in C; if C occurs positively (respectively, negatively) in C ′ then C occurs positively (negatively) in C ′ ⊓D, ∃R.C′ , D ⊑ C ′ , and it occurs negatively (positively) in ¬C ′ and C ′ ⊑ D. A TBox T is Horn if no concept of the form ¬C occurs negatively in T and no ∃R.¬C occurs positively in T . In the DL Horn-L, where L is one of our DLs, only Horn-L-TBoxes are allowed. Clearly, EL- and DL-Lite-TBoxes are Horn by definition.

An ABox, A, is a finite set of assertions of the form Ak(ai) or Pk(ai, aj). An L-TBox T and an ABox A form an L-KB K = (T ,A); ind(K) is the set of individual names in K.

The semantics for the DLs is defined in the usual way based on interpretations I = (∆I , ·I ) that comply with the unique name assumption: aIi ̸= aIj for i ̸= j [Baader et al., 2003]. We write I |= α in case an inclusion or assertion α is true in I. If I |= α, for all α ∈ T ∪A, then I is a model of a KB K = (T ,A); in symbols: I |= K. K is consistent if it has a model. K |= α means that I |= α for all I |= K.

A conjunctive query (CQ) q(x) is a formula ∃yϕ(x, y), where ϕ is a conjunction of atoms of the form Ak(z1) or Pk(z1, z2) with zi in x, y. A tuple a in ind(K) (of the same length as x) is a certain answer to q(x) over K = (T ,A) if I |= q(a) for all I |= K; in this case we write K |= q(a). If x = ∅, the answer to q is 'yes' if K |= q and 'no' otherwise.

For combined complexity, the problem 'K |= q(a)?' is NP-complete for the DL-Lite logics [Calvanese et al., 2007], EL and ELH [Rosati, 2007], and EXPTIME-complete for the remaining Horn DLs above [Eiter et al., 2008]. For data complexity (with fixed T and q), this problem is in AC0 for the DL-Lite logics [Calvanese et al., 2007] and P-complete for the remaining DLs [Rosati, 2007; Eiter et al., 2008].

A signature, Σ, is a set of concept and role names. By a Σ-concept, Σ-role, Σ-CQ, etc. we understand any concept, role, CQ, etc. constructed using the names from Σ. Given an interpretation I and a signature Σ, we define the Σ-types tIΣ(u) and rIΣ(u, v) of u, v ∈ ∆I by taking:

3 Σ-Query Entailment and Inseparability

Now we define the central notions of the paper, Σ-query entailment and inseparability, and establish their semantic characterisation based on the notion of materialisation. We then show how to construct materialisations by developing a theory of finitely generated materialisations.

Definition 1. Let K1 and K2 be KBs and Σ a signature. We say that K1 Σ-query entails K2 if K2 |= q(a) implies K1 |= q(a), for all Σ-CQs q(x) and all tuples a in ind(K2). Knowledge bases K1 and K2 are Σ-query inseparable if they Σ-query entail each other; in this case we write K1 ≡Σ K2.

Checking Σ-query inseparability can be trivially reduced to two Σ-query entailment checks. Conversely, for most languages we have a semantically transparent reduction of Σquery entailment to Σ-query inseparability:

Theorem 1. Let L be any of our DLs containing EL or having role inclusions. Then Σ-query entailment of L-KBs is LOGSPACE-reducible to Σ-query inseparability of L-KBs.

To prove the upper complexity bounds for both problems, we give a semantic characterisation of Σ-query entailment in terms of materialisations and finite Σ-homomorphisms. An interpretation M is a materialisation of a KB K if K |= q(a) iff M |= q(a), for all CQs q(x) and all tuples a in ind(K). We say that K is materialisable if it has a materialisation.

Suppose Mi is a materialisation of Ki, for i = 1, 2. A function h: ∆M2 → ∆M1 is a Σ-homomorphism if tM2 Σ (u) ⊆ tM1 Σ (h(u)) and rM2 Σ (u, v) ⊆ rM1 Σ (h(u), h(v)), for all u, v ∈ ∆M2 , and h(aM2 ) = aM1 for all a ∈ ind(K2) that belong to a Σ-concept or a Σ-role. As answers to Σ-CQs are preserved under Σ-homomorphisms, K1 Σ-query entails K2 if there is a Σ-homomorphism fromM2 to M1. However, the converse does not necessarily hold:

MaterialisationsMi of Ki, for i = 1, 2, are shown in Fig. 1a. Let Σ = {Q,R, S, T}. Then there is no Σ-homomorphism fromM2 toM1 (as rM2 Σ (a, u) = ∅, we can map u to, say, σ but then only the shaded part of M2 can be mapped Σhomomorphically to M1). However, for any Σ-query q(x), M2 |= q(a) impliesM1 |= q(a) as any finite subinterpretation of M2 can be Σ-homomorphically mapped to M1.

We say that M2 is finitely Σ-homomorphically embeddable into M1 if, for every finite subinterpretation M′2 of M2, there exists a Σ-homomorphism fromM′2 toM1. Intuitively, finite M′2 can be regarded as a CQ whose variables are elements of ∆M2 and the answer variables are the ind(K2).

Theorem 2. Suppose Ki is a consistent KB with a materialisationMi, i = 1, 2. Then K1 Σ-query entails K2 iff M2 is finitely Σ-homomorphically embeddable into M1.

One problem with applying Theorem 2 is that materialisations are in general infinite. We address this problem by introducing finite representations of materialisations, and show that Horn-ALCHI and all of its fragments enjoy having such representations. Let K = (T ,A) be a KB and let G = (∆G , ·G ,❀) be a finite structure such that

• ∆G = ind(K) ∪ Ω, for some Ω with ind(K) ∩ Ω = ∅,
• (∆G , ·G ) is an interpretation with P G i ⊆ ind(K) × ind(K), for all role names Pi,
• (∆G ,❀) is a directed graph (possibly containing loops) with nodes ∆G and arcs ❀⊆ ∆G × Ω, where each u ❀ v is labelled with a set (u, v)G ̸= ∅ of roles satisfying the condition: if ui ❀ v and u2 ❀ v then (u1, v)G = (u2, v)G.

A path σ in G is a sequence u0 . . . un with u0 ∈ ind(K) and ui ❀ ui+1 for i < n. Denote the last element of σ by tail(σ). The unravelling M of G is an interpretation (∆M, ·M), where ∆M is the set of paths in G and ·M is given by:

for concept and role names A and P . We call G a generating structure for K if its unravelling is a materialisation of K. We say that a DL L has finitely generated materialisations if every L-KB has a generating structure. In Example 1, M2 is generated by the structure G2 in Fig. 1b.

Theorem 3. Horn-ALCHI and all its fragments defined above have finitely generated materialisations. Moreover,

• for any L ∈ {ALCHI,ALCI,ALCH,ALC} and any Horn-L KB (T ,A), a generating structure can be constructed in time |A| · 2p(|T |) , p a polynomial;
• for anyL in the ELandDL-Lite families introduced above and any L-KB (T , A), a generating structure can be constructed in time |A| · p(|T |), p a polynomial.

4 Σ-Query Entailment by Games

Suppose a DL L has finitely generated materialisations. We now show that the problem of checking finite Σ-homomorphic embeddability between materialisations of L-KBs can be reduced to the problem of finding a winning strategy in a game played on the generating structures for these KBs.

For a generating structure G for K and a signature Σ, the Σ-types tGΣ(u) and rGΣ(u, v) of u, v ∈ ∆G are defined by:

where (P -)G is the converse of P G . We write u ❀Σ v if u ❀ v and rGΣ(u, v) ̸= ∅.

Suppose Ki is a consistent L-KB, for i = 1, 2, and Σ a signature. Let Gi = (∆Gi , ·Gi ,❀i) be a generating structure for Ki and let Mi be its unravelling; GΣ i andMΣi denote the restrictions of Gi andMi to Σ. We begin with a very simple game on the finite generating structure GΣ 2 and the possibly infinite materialisation MΣ1 .

Infinite Game. This game is played by two players. Intuitively, player 1 tries to construct a homomorphism, while player 2 wants to impede him by choosing a path in M2 to which player 1 cannot find a homomorphic image given his previous choices. The states of the game are of the form si = (ui ↦→ σi), for i ≥ 0, where ui ∈ ∆G2 and σi ∈ ∆M1 satisfy the following condition:

The game starts in a state s0 = (u0 ↦→ σ0) with σ0 = u0 in case u0 ∈ ind(K2) belongs to a Σ-concept or a Σ-role. In each round i > 0, player 2 challenges player 1 with some ui ∈ ∆G2 such that ui-1 ❀Σ2 ui. Player 1 has to respond with a σi ∈ ∆M1 satisfying (s1) and

This gives the next state si = (ui ↦→ σi). Note that of all the ui only u0 may be an ABox individual; however, there is no such a restriction on the σi. A play of length n ≥ 0 starting from s0 is any sequence s0, . . . , sn of states obtained as described above. For an ordinal λ ≤ ω, we say that player 1 has a λ-winning strategy in the game GΣ(G2,M1) starting from a state s0 if, for any play of length i < λ, which starts from s0 and conforms with this strategy, and any challenge of player 2 in round i+1, player 1 has a response. The next theorem gives a game-theoretic flavour to the criterion of Theorem 2.

Theorem 4. M2 is finitely Σ-homomorphically embeddable intoM1 iff the following conditions hold:

(abox) tM2 Σ (a) ⊆ tM1 Σ (a), rM2 Σ (a, b) ⊆ rM1 Σ (a, b), for any a, b ∈ ind(K2) that belong to a Σ-concept or a Σ-role;

(win) for any u0 ∈ ∆G2 and n < ω, there exists σ0 ∈ ∆M1 such that player 1 has an n-winning strategy in the game GΣ(G2,M1) starting from (u0 ↦→ σ0).

Example 2. Consider GΣ 2 for K2,MΣ1 for K1 andΣ fromExample 1. For each n < ω, player 1 has an n-winning strategy from (u ↦→ σn 0 ): for n = 4, it is shown in Fig. 1b by dotted lines (in round 2, player 2 has two possible challenges).

The criterion of Theorem 4 does not seem to be a big improvement on Theorem 2 as we still have to deal with an infinite materialisation. Our aim now is to replace (win) by a more complex game on the finite generating structures G2 and G1. We consider four types, τ, of strategies in GΣ(G2,M1) and for each of them we define a game GτΣ(G2, G1) such that, for any u0 ∈ ∆G2 , the following conditions are equivalent:

(<ωτ ) for every n < ω, player 1 has an n-winning τstrategy in GΣ(G2,M1) starting from some (u0 ↦→ σn 0 ); (ωτ ) player 1 has an ω-winning strategy inGτΣ(G2, G1) starting from some state depending on u0 and τ .

We begin with simplest 'forward' winning strategies.

Forward Strategies. We say that a λ-strategy (λ ≤ ω) for player 1 in the game GΣ(G2,M1) is forward if, for any play of length i - 1 < λ, which conforms with this strategy, and any challenge ui-1 ❀Σ2 ui by player 2, the response σi of player 1 is such that either σi-1, σi ∈ ind(K1) or

σi = σi-1w, for some w ∈ ∆G1 . If the Gi, i = 1, 2, are such that the Σ-labels on ❀i-edges contain no inverse roles, then every strategy in GΣ(G2,M1) is forward. This is the case for DLs without inverse roles: Horn-ALCH, EL, etc.

The existence of a forward λ-winning strategy for player 1 in GΣ(G2,M1) is equivalent to the existence of such a strategy in the game GfΣ(G2, G1), which is defined similarly to GΣ(G2,M1) except that it is played on G2 and G1, and the response wi ∈ ∆G1 of player 1 to a challenge ui-1 ❀Σ2 ui must be such that either wi-1, wi ∈ ind(K1) or wi-1 ❀1 wi. This game is a standard reachability game on finite graphs, where the existence of ω-winning strategies for player 1 can be checked in polynomial time in the size of G1 and G2 [Mazala, 2001]. By Theorem 3, we obtain the P and EXPTIME upper complexity bounds for ELH and Horn-ALCH, respectively. In contrast to forward strategies, the winning strategies of Example 2 can be described as 'backward.'

Backward Strategies. A λ-strategy for player 1 in GΣ(G2,M1) is backward if, for any play of length i - 1 < λ, which conforms with this strategy, and any challenge ui-1 ❀Σ2 ui by player 2, the response σi of player 1 is the immediate predecessor of σi-1 in M1 in the sense that σi-1 = σiw, for some w ∈ ∆G1 ; player 1 loses if σi-1 ∈ ind(K1). Note that, sinceM1 is tree-shaped, the response of player 1 to any other challenge ui-1 ❀Σ2 u′i must be the same σi. That is why the states of the game GbΣ(G2, G1) are of the form (Ξi ↦→ wi), where Ξi is the set of all ❀Σ2 -successors of elements of Ξi-1 (forward strategies need only one successor). The more complex structure of the states leads to an increase in the complexity: checking whether player 1 has an ω-winning strategy in GbΣ(G2, G1) is CONP-hard.

Observe that in the case of DL-Litecore and DL-Litehorn (which have inverse roles but no RIs), generating structures G = (∆G , ·G ,❀) are so that, for any u ∈ ∆G and R, there is at most one v with u ❀ v and R ∈ rG (u, v) [Kontchakov et al., 2010a]. As a result, any n-winning strategy consists of a (possibly empty) backward part followed by a (possibly empty) forward part. Moreover, in the backward games for these DLs, the sets Ξi are singletons. Thus, the number of states in the combined backward/forward games is polynomial, and the existence of winning strategies is in P.

In general, however, the forward strategy in the combination is not enough, and we require start-bounded strategies.

Start-Bounded Strategies. A strategy for player 1 in the game GΣ(G2,M1) starting from (u0 ↦→ σ0) is start-bounded if it never leads to (ui ↦→ σi) with σ0 = σiw, for some w ∈ ∆G1 and i > 0. In other words, player 1 cannot use elements ofM1 that are located closer to the ABox than σ0; the ABox individuals inM1 can only be used if σ0 ∈ ind(K1). Consider GΣ 2 andMΣ1 in Fig. 2a. Player 1 has awinning startbounded strategy from (u2 ↦→ σ1) as shown in Fig. 2a by dashed lines (indices indicate rounds). Observe that player 1 moves forwards and backwards along ❀1 inM1: σ4 = σ3w is visited in round 2 between visits to σ3 in rounds 1 and 3.

Start-bounded finite game GsΣ(G2, G1) ensures that player 1 moves only forwards along ❀1 in G1 and so, he has to guess all elements of G2 that are mapped to the same element in M1. The states of GsΣ(G2, G1) are of the form u1

si = (Γi, Ξi ↦→wi), where Ξi is the guess and Γi is required to ensure that only forward moves are possible.

Consider GΣ 2 and MΣ1 in Fig. 2a. Suppose that G1 is isomorphic to M1 and denote by wi the element of G1 that corresponds to σi in M1. Then player 1 has an ω-winning strategy in GsΣ(G2, G1) from (∅, {u2, u9} ↦→ w1). Player 2 challenges with u2 ❀Σ2 u6, and player 1 responds with ({u2, u9}, {u6, u8} ↦→ w3). Then player 2 picks u6 ❀Σ2 u7 and player 1 responds with ({u6, u8}, {u7} ↦→ w4), where the game ends. Note the crucial guesses {u2, u9} ↦→ w1 and {u6, u8} ↦→ w3 made by player 1. If player 1 responded with ({u2, u9}, {u6} ↦→ w3) (and failed to guess that u8 must also be mapped to w3), then after the challenge u6 ❀Σ2 u7 and the only possible response ({u6}, {u7} ↦→ w4)), player 2 would pick u7 ❀Σ2 u8, to which player 1 could not respond.

General Strategies. A general winning strategy in the game GΣ(G2,M1) is composed of one backward and a number of start-bounded strategies. Consider, for example, GΣ 2 andMΣ1 in Fig. 2b. Starting from (u1 ↦→ σ2), player 1 can respond to the challenges u1 ❀Σ2 u2 ❀Σ2 u3 according to the backward strategy; to u2 ❀Σ2 u6 ❀Σ2 u7 ❀Σ2 u8 ❀Σ2 u9 according to the start-bounded strategy as above, see Fig. 2a; while u9 ❀Σ2 u10 is again responded according to the backward strategy. We can combine the two backward strategies into a single one, but keep the start-bounded one separate.

In general, the finite game GgΣ(G2, G1) begins as the backward game but with states of the form (Ξi ↦→ wi, Ψi), where Ξi and wi are as above and Ψi indicates initial challenges in start-bounded games. In each round i > 0, player 2 can choose from two options. First, if wi-1 /∈ ind(K1), he can challenge player 1 with the set Ψi-1 (that is, similar to the backward game but with a possibly smaller Ψi-1 instead of the set of all successors). Second, player 2 can launch the start-bounded game from (∅, Ξi-1 ↦→ wi-1), where his first challenge cannot be picked from Ψi-1.

The full game graph is exponential in the size of the generating structures, and so checking whether player 1 has an ωwinning strategy can also be done in exponential time. This matches the EXPTIME-hardness of checking whether player 1 has an ω-winning strategy in the start-bounded game.

Theorem 5. For combined complexity, both KB Σ-query inseparability and KB Σ-query entailment are

• (f) P-complete in EL and ELH and EXPTIME-complete in Horn-ALC and Horn-ALCH;
• (b+f) P-complete in DL-Litecore and DL-Litehorn;
• (b+s) EXPTIME-complete in DL-LiteHhorn and DL-LiteHcore ; 2EXPTIME-complete in Horn-ALCHI, Horn-ALCI.

For data complexity, all these problems are P-complete.

5 RelatedWork

Σ-query inseparability of KBs has not been investigated systematically before. However, the polynomial upper bound for EL was established as a preliminary step to study TBox query inseparability [Lutz and Wolter, 2010]. This notion was also used to study forgetting in DL-LiteNbool [Wang et al., 2010].

Σ-query inseparability of KBs is closely related to knowledge exchange between KBs and inseparability between TBoxes. Suppose K1 and K2 are KBs given in disjoint signatures Σ1 and Σ2, and T12 consists of inclusions of the form S1 ⊑ S2, where the Si are concept (or role) names in Σi. Then deciding whether K1 ∪ T12 ≡Σ2 K2 is called the membership problem for universal CQ-solutions. For DLs L with role inclusions, this problem is in fact a Σ2-query inseparability problem in L, and so the complexity upper bounds for Σ-query inseparability can be applied directly to obtain upper bounds for the membership problem. Conversely, Σ-query entailment for any of our DLs L is LOGSPACE-reducible to the membership problem for universal CQ-solutions in L, and so we can also apply complexity lower bounds for query inseparability of KBs.

As for TBox inseparability, recall that T1 and T2 are Σquery inseparable if, for all Σ-ABoxes A, the KBs (T1,A) and (T2,A) are Σ-query inseparable. This notion has been extensively studied [Kontchakov et al., 2010b; Lutz and Wolter, 2010; Konev et al., 2011; 2012]. TBox and KB inseparabilities have different applications. The former supports ontology engineering when data is unknown or changes frequently: one can equivalently replace one TBox with another only if they return the same answers to queries over every ΣABox. In contrast, KB inseparability is useful in applications where data is stable-such as knowledge exchange or variants of module extraction and forgetting with fixed data-in order to use the KB in a new application or as a compilation step to make CQ answering more efficient. For many DLs, TBox Σ-query inseparability is harder than KB query inseparability: in DL-Litehorn, the space of relevant ABox counterexamples is exponential and, in fact, TBox inseparability is NP-hard, while KB inseparability is in P. Similarly, Σ-query inseparability of EL KBs is tractable, while Σ-query inseparability of TBoxes is EXPTIME-complete. The complexity of TBox inseparability for Horn-DLs extending Horn-ALC is still unknown. For work on other notions of TBox inseparability and the corresponding notions of modules and forgetting, the reader is referred to [Cuenca Grau et al., 2008; Konev et al., 2009; Del Vescovo et al., 2011; Nikitina and Rudolph, 2014; Nikitina and Glimm, 2012; Lutz et al., 2012; Koopmann and Schmidt, 2014a; Nortje et al., 2013].