Query Conservative Extensions in Horn Description Logics with Inverse Roles

1 Introduction

In the past years, access of incomplete data mediated by description logic (DL) ontologies has gained increasing importance [Poggi et al., 2008; Bienvenu and Ortiz, 2015]. The main idea is to specify domain knowledge and semantics of the data in the ontology, resulting in more complete answers to queries. Significant research activity has led to efficient algorithms and tools for a wide range of DLs such as DL-Lite [Calvanese et al., 2007], more expressive Horn-DLs [Eiter et al., 2012; Trivela et al., 2015; Bienvenu et al., 2016], and "full Boolean" DLs such as ALC [Kollia and Glimm, 2013; Zhou et al., 2015].

In contrast to query answering, which is by now wellunderstood, there is a need to develop reasoning services for ontology engineering that are tailored towards query-centric applications and support tasks such as ontology versioning and module extraction from ontologies. For example, if one wants to safely replace an ontology with a new version or with a smaller subset of itself (a module), then the new ontology should preserve the answers to all queries over all ABoxes (which store the data) [Kontchakov et al., 2010]. The same guarantee ensures that one can safely replace an ontology with another version in an application [Konev et al., 2012]. In both cases, ontologies need to be tested not for their logical equivalence, but for giving the same answers to relevant queries over relevant datasets.

This requirement can be formalized using conservative extensions. In the following, we use the DL term TBox instead of ontology. A TBox T2 ⊇ T1 is a (Γ,Σ)-query conservative extension of a TBox T1, where Γ and Σ are signatures of concept/role names relevant for data and queries, respectively, if all Σ-queries give the same answers w.r.t. T1 and T2, for every Γ-ABox. Note that the subset relationship T2 ⊇ T1 is natural when replacing a TBox with a module, but not in versioning, so we might not want to insist on it. In this more general case, T1 and T2 are called (Γ, Σ)-query inseparable. Conservativity and inseparability of TBoxes, as defined above, are useful when knowledge is considered static and data changes frequently. Variants of these notions for knowledge bases (KBs), which consist of a TBox and an ABox, can be used for applications with static data [Wang et al., 2014; Arenas et al., 2016].

We also consider the basic notion of query entailment: T1 (Γ,Σ)-query entails T2 if all Σ-queries give at least the answers w.r.t. T1 that they give w.r.t. T2, on any Γ-ABox. Query inseparability and conservativity are special cases of entailment: inseparability is bidirectional entailment and conservativity is entailment with the assumption that T1 ⊆ T2. It thus suffices to prove upper bounds for query entailment and lower bounds for conservative extensions. As a query language, we concentrate on conjunctive queries (CQs); since we work with Horn-DLs and quantify over the queries, this is equivalent to using unions of CQs (UCQs) or positive existential queries (PEQs). CQ entailment has been studied for various DLs [Kontchakov et al., 2009; Lutz and Wolter, 2010; Konev et al., 2012; Botoeva et al., 2016c], also in the KB version [Botoeva et al., 2016b; Botoeva et al., 2016c] and for OBDA specifications [Bienvenu and Rosati, 2015], see also the survey [Botoeva et al., 2016a]. Nevertheless, there is still a notable gap in our understanding of this notion: query entailment between TBoxes is poorly understood in Horn DLs with inverse roles, often considered a crucial feature, for which there do not seem to be any available results. This is for a reason: it has been observed in [Botoeva et al., 2016a; Botoeva et al., 2016b] that standard techniques for Horn DLs without inverse roles fail when inverse roles are added.

In fact, for Horn-DLs without inverse roles query entailment can be characterized by the extence of homomorphisms between universal models [Lutz and Wolter, 2010; Botoeva et al., 2016a]. The resulting characterizations provide an important foundation for decision procedures, often based on tree automata [Botoeva et al., 2016a]. In the presence of inverse roles, however, such characterizations are only correct if we require the existence of nbounded homomorphisms, for any n [Botoeva et al., 2016a; Botoeva et al., 2016b]. It is not obvious how the existence of such infinite families of bounded homomorphisms can be verified using tree automata (or related techniques) and, consequently, decidability results for query conservative extensions in Horn-DLs with inverse roles are difficult to obtain. The only result we are aware of concerns inseparability of KBs, and it is proved using intricate game-theoretic techniques.

In this paper, we develop decision procedures for query entailment and related problems in Horn DLs with inverse roles. The main idea is to provide a more refined characterization, mixing unbounded and bounded homomorphisms and using unbounded homomorphisms only in places where this is strictly necessary. We can then deal with the "unbounded part" using tree automata while the "bounded part" is addressed by precomputing relevant information using a mosaic technique. In this way, we establish decidability and a 2EXPTIME upper bound for query entailment (and thus inseparability and conservativity) in Horn-ALCHIF. Together with lower bounds from [Botoeva et al., 2016c], we get 2EXPTIME-completeness for all fragments of Horn-ALCHIF that contain ELI or Horn-ALC.

We additionally study the case of deductive entailment between TBoxes, i.e., the question whether T1 entails at least the same concept and role inclusions as well as functionality assertions over Σ as T2. This problem too has not previously been studied for Horn DLs with inverse roles. We consider ELHIF⊥-TBoxes and show that deductive entailment is equivalent to a restricted version of query entailment. We obtain a model theoretic characterization, a decision procedure, and a 2EXPTIME upper complexity bound. We also give a CONEXPTIME lower bound.

Omitted proofs can be found in the long version here: www.informatik.uni-bremen.de/tdki/research/papers.html

2 Preliminaries

2.1 Horn-ALCHIF

We introduce Horn-ALCHIF, a member of the Horn-SHIQ family of DLs whose reasoning problems have been widely studied [Hustadt et al., 2007; Kr¨otzsch et al., 2007; Eiter et al., 2008; Kazakov, 2009; Lutz and Wolter, 2012; Ib´a˜nezGarc´ıa et al., 2014]. Let NC,NR,NI be sets of concept, role, and individual names. A role is either a role name r or an inverse role r-. As usual, we identify (r-)- and r, allowing to switch between roles names and their inverses easily. A concept inclusion (CI) is of the form L ⊑ R, where L and R are concepts defined by the syntax rules

with A ranging over concept names and r over roles. A role inclusion (RI) is of the form r ⊑ s with r, s roles and a functionality assertion (FA) is of the form func(r) with r a role. ELI⊥-concepts are expressions that are built according to the syntax rule for L above, but do not use "⊔".

A Horn-ALCHIF TBox T is a set of CIs, RIs, and FAs. An ELHIF⊥ TBox is a set of ELI⊥-CIs, RIs, and FAs. To avoid dealing with rather messy technicalities that do neither seem to be very illuminating from a theoretical viewpoint nor too useful from a practical one, 1 we generally assume that functional roles cannot have any subroles, that is, r ⊑ s ∈ T implies func(s) /∈ T . We conjecture that our main results also hold without that restriction. An ABox A is a non-empty set of concept and role assertions of the form A(a) and r(a, b), where A ∈ NC, r ∈ NR and a, b ∈ NI. We write ind(A) for the set of individuals in A.

The semantics is defined as usual in terms of interpretations I = (∆I , ·I ) complying with the standard name assumption, i.e., aI = a for all a ∈ NI [Baader et al., 2017]. An interpretation I is a model of a TBox T if it satisfies all inclusions and assertions in it, and likewise for ABoxes. A is consistent with T if T and A have a common model.

A signature Σ is a set of concept and role names. A Σ-ABox is an ABox that uses only concept and role names from Σ, and likewise for Σ-ELI⊥-concepts and other syntactic objects.

Generally and without further notice, we work with HornALCHIF TBoxes that are in a certain nesting-free normal form, that is, they contain only CIs of the form

where A,B,A1,A2 are concept names and r, s are roles. It is well-known that every Horn-ALCHIF TBox T can be converted into a TBox T ′ in normal form (introducing additional concept names) such that T is a logical consequence of T ′ and every model of T can be extended to one of T ′ by interpreting the additional concept names, see e.g. [Bienvenu et al., 2016]. As a consequence, all results obtained in this paper for TBoxes in normal form lift to the general case.

2.2 Query Conservative Extensions and Entailment

A conjunctive query (CQ) is of the form q(x) = ∃y ϕ(x, y), where x and y are tuples of variables and ϕ(x, y) is a conjunction of atoms of the form A(v) or r(v, w) with A ∈ NC, r ∈ NR, and v, w ∈ x ∪ y. We call x answer variables and y quantified variables of q. A CQ q is tree-shaped if the undirected graph (x ∪ y, {{v,w} | r(v,w) is an atom in q}) is a tree; tree-shaped CQs are thus connected and may contain multi-edges. A tree-shaped CQ q is strongly tree-shaped or an stCQ if the root is the one and only answer variable and q has no multi-edges, i.e., no two atoms r1(z1, z2), r2(z′1 , z′2 ) with r1 ̸= r2 and {z1, z2} = {z′1 , z′2 }.

A match of q in an interpretation I is a function π : x ∪ y → ∆I such that π(v) ∈ AI for every atom A(v) of q and (π(v), π(w)) ∈ rI for every atom r(v,w) of q. We write I |= q(a1, . . . , an) if there is a match of q in I with π(xi) = ai for all i < n. A tuple a of elements from NI is a certain answer to q over an ABox A given a TBox T , written T ,A |= q(a), if I |= q(a) for all models of T and A.

1 E.g., out of 439 available ontologies in BioPortal [Matentzoglu and Parsia, 2017], only 21 (≤ 4.8%) contain the described pattern. A significant fraction of the occurrences of the pattern appear to be due to modeling mistakes.

Definition 1 Let Γ,Σ be signatures and T1, T2 HornALCHIF TBoxes. We say that T1 (Γ, Σ)-CQ entails T2, written T1 |=CQ Γ,Σ T2, if for all Γ-ABoxes A consistent with T1 and T2, all Σ-CQs q(x) and all tuples a ⊆ ind(A), T2, A |= q(a) implies T1,A |= q(a). If in addition T1 ⊆ T2, we say that T2 is a (Γ,Σ)-CQ conservative extension of T1. If T1 |=CQ Γ,Σ T2 and vice versa, then T1 and T2 are (Γ, Σ)-CQ inseparable.

We also consider (Γ, Σ)-stCQ entailment, denoted |=stCQ Γ,Σ and defined in the obvious way by replacing CQs with stCQs.

If T1 ̸|=CQ Γ,Σ T2 because T2, A |= q(a) but T1, A ̸|= q(a) for some Γ-ABox A consistent with both Ti, Σ-CQ q(x) and a, we call the triple (A, q, a) a witness to non-entailment.

Example 2 Let T1 = {PhDStud ⊑ ∃advBy.Prof, advBy ⊑ adv-} and T2 = T1 ∪ {func(advBy)}, Σ = {Prof} and Γ = {PhDStud, adv}. Then T1 ̸|=CQ Γ,Σ T2 because of the witness ({PhDStud(john), adv(mary, john)}, Prof(x), mary).

If we drop from Definition 1 the condition that A must be consistent with both T1 and T2, then we obtain an alternative notion of CQ entailment that we call CQ entailment with inconsistent ABoxes. While this new notion trivially implies CQ entailment in the original sense, the converse fails.

Example 3 Let T1 = ∅, T2 = {A1 ⊓ A2 ⊑ ⊥} and Γ = {A1,A2}, Σ = {B}. Then T1 |=CQ Γ,Σ T2 but T1 does not (Γ, Σ)-CQ entail T2 with inconsistent ABoxes.

The following lemma relates the two notions of CQ entailment. CQ evaluation is the problem to decide, given a TBox T , an ABox A, a CQ q, and a tuple a ∈ ind(A), whether T ,A |= q(a).

Lemma 4 CQ entailment with inconsistent ABoxes can be decided in polynomial time given access to oracles deciding CQ entailment and CQ evaluation.

Consequently and since CQ evaluation is in EXPTIME in HornALCHIF [Eiter et al., 2008], all complexity results obtained in this paper also apply to CQ entailment with inconsistent ABoxes.

It is easy to see that T1 ̸|=CQ Γ,Σ T2 if there is a Γ-role r and a Σ-role s with T2 |= r ⊑ s but T1 ̸|= r ⊑ s. We write T1 |=RI Γ,Σ T2 if there are no such r and s. Clearly, T1 |=RI Γ,Σ T2 can be decided via |Γ| · |Σ| many Horn-ALCHIF subsumption tests, thus in EXPTIME [Tobies, 2001]. It is thus safe to assume T1 |=RI Γ,Σ T2 when deciding CQ entailment, which we will generally do from now on to avoid dealing with special cases.

2.3 Deductive Conservative Extensions

Another natural notion of entailment is deductive entailment, which generalizes the notion of deductive conservative extensions [Ghilardi et al., 2006; Lutz et al., 2007; Konev et al., 2009; Lutz and Wolter, 2010], and which separates two TBoxes in terms of concept and role inclusions and functionality assertions, instead of ABoxes and queries.

Definition 5 Let Σ be a signature and let T1 and T2 be ELHIF⊥ TBoxes. We say that T1 Σ-deductively entails T2, written T1 |=ELHIF⊥ Σ T2, if for all Σ-ELI⊥-concept inclusions α and all Σ-RIs and Σ-FAs α: T2 |= α implies T1 |= α.

If additionally T1 ⊆ T2, then we say that T2 is a Σ-deductive conservative extension of T1. If T1 |=ELHIF⊥ Σ T2 and vice versa, then T1 and T2 are Σ-deductively inseparable.

Although closely related, it is not difficult to see that deductive and query entailment are orthogonal.

Example 6 (1) Let T1, T2 be as in Example 3 and Σ = {A1,A2,B}. Then T1 |=stCQ Σ,Σ T2, but T1 ̸|=ELHIF⊥ Σ T2.

Nevertheless, the two notions are sufficiently closely related so that we have the following.

Lemma 7 In ELHIF⊥, deductive entailment can be decided in polynomial time given access to oracles for stCQ entailment and stCQ evaluation.

2.4 Homomorphisms and the Universal Model

For interpretations I1, I2 and a signature Σ, a Σhomomorphism from I1 to I2 is a total function h : ∆I1 → ∆I2 such that (1) h(a) = a for all a ∈ NI, (2) h(d) ∈ AI2 for all d ∈ AI1 , A ∈ NC ∩ Σ, and (3) (h(d), h(d′ )) ∈ rI2 for all (d, d′ ) ∈ rI1 , r ∈ NR ∩ Σ. If there is a Σ-homomorphism from I1 to I2, we write I1 →Σ I2.

Let T be a Horn-ALCHIF TBox in normal form and A an ABox consistent with T . A type for T is a set t ⊆ sub(T )∩NC such that T |= d t ⊑ A impliesA ∈ t for all concept namesA. For a ∈ ind(A), let tpT (a) = {A | T ,A |= A(a)} be the type of a relative to T . When a ∈ ind(A), t, t′ are types for T , and r is a role, we write

• a ⇝T ,A r t if T ,A |= ∃r. d t(a) and t is maximal with this condition, and
• t ⇝Tr t′ if T |= d t ⊑ ∃r. d t′ and t′ is maximal with this condition.

A path for A and T is a finite sequence π = ar0t1 · · · tn-1rn-1tn, n ≥ 0, with a ∈ ind(A), r0, . . . , rn-1 roles, and t1, . . . , tn types for T such that

• (i) a ⇝T ,A r0 t1 and, if func(r0) ∈ T , then there is no b ∈ ind(A) such that T , A |= r0(a, b);
• (ii) for every 1 ≤ i < n, we have ti ⇝Tri ti+1 and, if func(r) ∈ T , then ri-1 ̸= ri .

When n > 0, we use tail(π) to denote tn. Let Paths be the set of all paths for A and T . The universal model IT ,A of T and A is defined as follows:

It is standard to prove that IT ,A is indeed a model of T and A and that it is universal in the sense that for every model I

of T and A, we have I → IT ,A. Consequently, T , A |= q(a) iff IT ,A |= q(a), for all CQs q(x) and tuples a of individuals.

We also need universal models of a TBox T and a type t, instead of an ABox. More precisely, we define IT ,t = IT ,At where At = {A(a) | A ∈ t} for a fixed a ∈ NI.

3 Model-theoretic Characterization

We aim to provide a model-theoretic characterization of query entailment that will be the basis for our decision procedure later on. The first step towards this characterization consists in showing that non-entailment is always witnessed by treeshaped ABoxes and tree-shaped CQs with at most one answer variable. Here, tree-shaped ABoxes A are defined analogously to tree-shaped CQs: A is tree-shaped if the undirected graph GA = (ind(A), {{a, b} | r(a, b) ∈ A}) is a tree.

Lemma 8 Let T1 and T2 be Horn-ALCHIF TBoxes with T1 |=RI Γ,Σ T2. If T1 ̸|=CQ Γ,Σ T2, then there is a witness (A, q, a) where A and q are tree-shaped and |a| ≤ 1, i.e., q has at most one answer variable. If T1 ̸|=stCQ Γ,Σ T2, then there is such a witness where additionally q is an stCQ.

Our goal is to characterize query entailment in terms of homomorphisms between (universal) models. Homomorphisms are natural because answers to CQs are preserved under homomorphisms (both on interpretations and on ABoxes). In fact, they are preserved even under bounded homomorphisms if the bound is not smaller than the number of variables in the CQ.

Let I1, I2 be interpretations, d ∈ ∆I1 , and n ≥ 0. We say that there is an n-bounded Σ-homomorphism from I1 to I2, written I1 →nΣ I2, if for any subinterpretation I ′1 of I1 with |∆I ′1| ≤ n, we have I ′1 →Σ I2. Moreover, we write I1 →fin Σ I2 if I1 →nΣ I2 for any n. The following characterization follows from the definition of CQ entailment, Lemma 8, and the connection between CQs and suitably bounded homomorphisms.

Lemma 9 Let T1 and T2 be Horn-ALCHIF TBoxes with T1 |=RI Γ,Σ T2. Then T1 |=CQ Γ,Σ T2 iff for all tree-shaped ΓABoxes A consistent with T1 and T2, IT2,A →fin Σ IT1,A.

Ideally, we would like to use Lemma 9 as a basis for a decision procedure based on tree automata. To this end, it is useful that the ABox A and models IT1,A and IT2,A in the lemma are treeshaped. What is problematic is that Lemma 9 speaks about unbounded homomorphisms, for any bound (corresponding to the unbounded size of CQs), since it does not seem possible to verify such a condition using automata. We would thus like to replace bounded homomorphisms with unbounded ones, which does not compromise the characterization in the case of Horn-DLs without inverse roles [Lutz and Wolter, 2010; Botoeva et al., 2016c]. However, this is not true already for ELI TBoxes [Botoeva et al., 2016a]:

Example 10 Let T1 = {A ⊑ ∃s.B, B ⊑ ∃r-.B}, T2 = {A ⊑ ∃s.B, B ⊑ ∃r.B}, Γ = {A}, and Σ = {r}. Then both IT1,A and IT2,A contain an infinite r-path; the r-path in IT1,A has a final element while the one in IT2,A does not. Hence IT2,A ̸→Σ IT1,A, but T1 |=CQ Γ,Σ T2 (see Thm. 11 below).

We now show that it is possible to refine Lemma 9 so that it makes a much more careful statement in which bounded homomorphisms are partly replaced by unbounded ones. It is then possible to check the unbounded homomorphism part of the characterization using tree automata as desired, and to deal with unbounded homomorphisms using a mosaic technique that "precompiles" relevant information about unbounded homomorphisms to be used in the automaton construction.

We start with introducing relevant notation. For a signature Σ, we use I|con Σ to denote the restriction of the interpretation I to those elements that can be reached from an ABox individual by traveling along Σ-roles (forwards or backwards). For a TBox T , an ABox A, and a ∈ ind(A), we use IT ,A|a to denote the subtree interpretation in the universal model IT ,A rooted at a. A Σ-subtree in IT ,A is a maximal tree-shaped, Σconnected sub-interpretation I of IT ,A that does not comprise any ABox individuals. The root of I is the (unique) element of ∆I that can be reached from an ABox individual on a shortest path among all element of ∆I . The refined characterization uses simulations instead of homomorphisms for the stCQ case because they are insensitive to multi-edges. Given a signature Σ and two interpretations I, J , a Σ-simulation of I in J is a relation σ ⊆ ∆I ×∆J such that: (1) (a, a) ∈ σ for all a ∈ NI, (2) if d ∈ AI with A ∈ Σ and (d, e) ∈ σ, then d2 ∈ AJ , and (3) if (d, d′ ) ∈ rI with r a Σ-role and (d, e) ∈ σ, then there is some e′ with (e, e′ ) ∈ rJ and (d′ , e′ ) ∈ σ. We write I ⪯Σ J if there is a Σ-simulation of I in J .

Theorem 11 Let T1 and T2 be Horn-ALCHIF TBoxes with T1 |=RI Γ,Σ T2. Then T1 |=CQ Γ,Σ T2 iff for all tree-shaped ΓABoxes A consistent with T1 and T2, and for all tree-shaped, finitely branching models I1 of A and T1, the following hold:

1. IT2,A|con Σ →Σ I1;
2. for all Σ-subtrees I in IT2,A, one of the following holds:
3. (a) I →Σ I1;
4. (b) I →fin Σ IT1,tpI1 (a) for some a ∈ ind(A).

Furthermore, T1 |=stCQ Γ,Σ T2 iff for all A and I1 as above, IT2,A|con Σ ⪯Σ I1.

4 Decidability and Complexity

We prove that, in Horn-ALCHIF, CQ entailment can be decided in 2EXPTIME. By existing lower bounds, the former is thus 2EXPTIME-complete in all fragments of Horn-ALCHIF that contain ELI or Horn-ALC. Moreover, stCQ entailment in Horn-ALCHIF and deductive entailment in ELHIF⊥ can also be decided in 2EXPTIME. We establish a CONEXPTIME lower bound and leave the precise complexity open.

To obtain the upper bounds, we use a combination of tree automata and mosaics to implement the characterization in Theorem 11. We start with a mosaic-based decision procedure for Condition (2b). Note that a Σ-subtree I in IT2,A can be uniquely identified by the type t2 of its root. It therefore suffices to show the following.

Theorem 12 Given two Horn-ALCHIF TBoxes T1 and T2 and types ti for Ti, i ∈ {1, 2}, it can be decided in time 22p(|T2|log|T1|) whether IT2,t2 |con Σ →fin Σ IT1,t1 , p a polynomial.

Although we cannot get rid of bounded homomorphisms in Theorem 11, a central idea for applying a mosaic approach to prove Theorem 12 is to first replace bounded homomorphisms with unbounded ones. To make this possible, we also replace IT1,t1 with a suitable class of interpretations used as targets for the unbounded homomorphisms.

To illustrate, consider Example 10 and let t1 = t2 = {B}. The difference between IT2,t2 →fin Σ IT1,t1 and IT2,t2 →Σ IT1,t1 is that unbounded homomorphisms fail once they "reach the root" of IT1,t1 while bounded homomorphisms can, depending on the bound, map the root of IT2,t2 deeper and deeper into IT1,t1 , thus never reaching its root. The latter is possible because IT1,t1 is regular in the sense that any two elements which have the same type root isomorphic subtrees. This is of course not only true in this example, but by construction in any universal model. To transition back from bounded to unbounded homomorphisms, we replace IT1,t1 with a class of (finite and infinite) interpretations that can be seen as a "backwards regularization" of IT1,t1 . In our concrete example, we would include an interpretation where a predecessor is added to the root of IT1,t1 because IT1,t1 contains an element of the same type as the root that has such a predecessor, an interpretation where that predecessor has a predecessor, and so on, even ad infinitum. We will now make this precise.

An interpretation I is quasi tree-shaped if:

1. ∆I ⊆ ({-1} ∪N)∗ ;
2. (d, e) ∈ rI implies that e = d · c or d = e · c for some c ∈ {-1} ∪ N.

For d, e ∈ ∆I , we say that e is a successor of d if e = d · c for some c ∈ N or d = e · -1. By this convention, quasi treeshaped interpretations can be viewed as directed graphs. The directedness does not correspond to the distinction between roles and inverse roles; in particular, there can be several role edges in both directions between the same d and e. Quasi tree-shaped interpretations can be viewed as a finite or infinite trees that need not have a root as they can extend indefinitely not only downwards but also upwards.

Let T be a Horn-ALCHIF TBox and let tp(T ) be the set of all types for T consistent with T . For every t0 ∈ tp(T ), we use tp(T , t0) to denote the set of all t ∈ tp(T ) that occur in the universal model IT ,t0 of t0 and T . Furthermore, given a quasi tree-shaped interpretation I and an element d ∈ ∆I , the 1-neighborhood of d in I is a tuple nI1 (d) = (t-, ρ, t, S) such that (a) t = tpI(d); (b) if there is a predecessor d0 ∈ ∆I of d, then t- = tpI(d0) and ρ = {r | (d0, d) ∈ rI }, otherwise ρ = t- = ⊥; (c) S is the set of all pairs (ρ′ , t′ ) such that there is a successor d′ of d with (d, d′ ) ∈ ρ′ (ρ′ maximal) and t′ = tpI(d′ ). We write (t-1 , ρ1, t1, S1) ⊑ (t-2 , ρ2, t2, S2) if t1 = t2, S1 ⊆ S2 and, if ρ1 ̸= ⊥, then ρ1 = ρ2 and t-1 = t-2 .

In the following, we define a class canω(T , t0) of quasi tree-shaped models of T . To construct a model from this class, choose a type t ∈ tp(T , t0) and define I = ({d0}, ·I ) such that tpI(d0) = t. Then extend I by applying the following rule exhaustively in a fair way:

• (R) Let d ∈ ∆I . Choose some e ∈ ∆IT ,t0 such that nI1 (d) ⊑ nIT ,t0 1 (e), and add to d the predecessor and/or successors required to achieve nI1 (d) = nIT ,t0 1 (e).

The potentially infinite class canω(T , t0) is the set of all interpretations I obtained as a limit of this construction.

Lemma 13 Let T be a Horn-ALCHIF TBox, t0 ∈ tp(T ), and I a tree-shaped interpretation. Then I →fin Σ IT ,t0 iff there is a J ∈ canω(T , t0) with I →Σ J .

We can now use Lemma 13 to devise the mosaic-based procedure for deciding the existence of a bounded homomorphism. Let T1, T2 be as in Theorem 11. We denote with rol(Ti) the set of all roles r, r- such that the (possibly inverse) role r occurs in Ti. Moreover, for a set of roles ρ, denote with ρ|Σ the restriction of ρ to Σ-roles.

Fix now some t1 ∈ tp(T1). Intuitively, a mosaic for t1 represents a possible 1-neighborhood of some element in IT1,t1 together with a decoration with sets of types for T2 that can be homomorphically embedded into the neighborhood. Formally, a mosaic for t1 is a tuple M = (t-, ρ, t, S, ℓ) such that (t-, ρ, t, S) = nIT1,t1 1 (d) for some d ∈ ∆IT1,t1 and ℓ : {t-, t} ∪ S → 2tp(T2) satisfies the following condition:

• (M) For all ̂t ∈ ℓ(t) we have ̂t∩Σ ⊆ t and, for all ̂t′ ∈ tp(T2), r ∈ rol(T2) with ̂t ⇝T2 r ̂ t′ , one the following holds for σ = {s | T |= r ⊑ s}:
• (a) σ|Σ = ∅;
• (b) t- ̸= ⊥, σ|Σ ⊆ ρ-, and ̂ t′ ∈ ℓ(t-);
• (c) there is (ρ′ , t′ ) ∈ S with ̂ t′ ∈ ℓ(ρ′ , t′ ) and σ|Σ ⊆ ρ′ .

To ease notation, we use t-M to denote t-, ρM to denote ρ, and likewise for the other components of a mosaic M. Let M be the set of all mosaics for t1 andM′ ⊆M. An M ∈ M′ is good inM′ if the following conditions are satisfied:

1. for each (ρ, t) ∈ SM, there is an N ∈ M′ such that (tM, ρ, t) = (t-N , ρN, tN), ℓM(ρ, t) = ℓN(tN), and ℓM (tM ) = ℓN (t-N ).
2. if t-M ̸= ⊥, there is N ∈M′ with (ρM, tM) ∈ SN, t-M = tN, ℓM(t-M ) = ℓN(tN), and ℓM(tM) = ℓN(ρM, tM).

Let M0,M1, . . . be the sequence obtained by starting with M0 = M and defining Mi+1 to be Mi when all mosaics that are not good inMi have been removed. Assume that Mp is where the sequence stabilizes.

Lemma 14 Let ti ∈ tp(Ti) for i ∈ {1, 2}. Then there is a J ∈ canω(T1, t1) such that IT2,t2 |con Σ →Σ J iffMp contains a mosaic M with t2 ∈ ℓM(tM).

Since there are at most 2|T1|2|T2| mosaics for t1, we obtain the desired Theorem 12.

We now develop the decision procedure for CQ and stCQ entailment in Horn-ALCHIF, based on Theorems 11 and 12. Our main tool are alternating two-way tree automata with counting (2ATAc), an extension of alternating tree automata over unranked trees [Gr¨adel and Walukiewicz, 1999] with the ability to count. A tree is a non-empty (potentially infinite) set of words T ⊆ (N \ 0)∗ closed under prefixes. We assume that trees are finitely branching, i.e., for every w ∈ T , the set {i | w·i ∈ T} is finite. For any w ∈ (N\0)∗ , we set w·0 := w. If w = n0n1 · · · nk, k ≥ 0, we set w ·-1 := n0 · · · nk-1. For an alphabet Θ, a Θ-labeled tree is a pair (T, L) with T a tree and L : T → Θ a node labeling function.

A 2ATAc is a tuple A = (Q, Θ, q0, δ, Ω) where Q is a finite set of states, Σ is the input alphabet, q0 ∈ Q is the initial state, δ is a transition function, and Ω : Q → N is a priority function. The transition function δ maps every state q and input letter a ∈ Θ to a positive Boolean formula δ(q, a) over the truth constants true and false and transition atoms of the form q, 〈-〉q, [-]q, ✸nq and ✷nq. Informally, a transition q expresses that a copy of A is sent to the current node in state q; 〈-〉q means that a copy is sent in state q to the predecessor node, which is required to exist; [-]q means the same except that the predecessor node is not required to exist; ✸nq (resp., ✷nq) means that a copy of q is sent to k (resp., to all but k) successors. The semantics of 2ATAc is given in terms of runs as usual, please see the appendix. We use L(A) to denote the set of trees accepted by A. It is standard to verify closure of 2ATAc under intersection. The following is obtained via reduction to standard alternating parity tree automata [Vardi, 1998].

Theorem 15 The emptiness problem for 2ATAc can be solved in time exponential in the number of states.

Let T1, T2 be Horn-ALCHIF TBoxes and Γ, Σ signatures. We aim to show that one can construct a 2ATAc A such that L(A) = ∅ iff T1 ̸|=CQ Γ,Σ T2. In fact, A is the intersection of four 2ATAc A1,A2,A3,A4. They run over Θ-labeled trees with Θ = 2Θ0 × 2Θ1 × 2Θ2 , where Θ0 = Γ ∪ {r- | r ∈ Γ} and Θi = sig(Ti) ∪ {r- | r ∈ sig(Ti)} for i = 1, 2. For a Θlabeled tree (T, L), we use Li, i ∈ {0, 1, 2} to refer to the i-th component of L, that is, L(n) = (L0(n),L1(n),L2(n)), for all n ∈ T . The component L0 represents a (possibly infinite) ABox A = {A(n) | A ∈ L0(n)}∪{r(n ·-1, n) | n ̸= ε, r ∈ L0(n)}, where r-(a, b) is identified with r(b, a). The 2ATAc A1 accepts a Θ-labeled tree (T, L) iff A is finite, connected and includes the root of T (and is thus tree-shaped), and it is straightforward to construct.

Components L1,L2 give rise to interpretations I1 = (T, ·I1 ) and I2 = (ind(A), ·I2 ), where for i ∈ {1, 2}:

A2 verifies that I1 is a model of A and T1, which is standard, too. A3 verifies that A is consistent with T2, and I2 is IT2,A restricted to ind(A). This involves computing the type of an ABox element without having access to the anonymous (that is: non-ABox) part of IT2,A, using a characterization of ABox entailments [Bienvenu et al., 2013] in terms of derivation trees. Finally, A4 verifies that either (1) or (2) from Theorem 11 is not satisfied. For (1), A4 sends a copy of itself to every tree I starting at an ABox element in IT2,A, and attempts to show that I cannot be homomorphically embedded into a corresponding tree in I1. This attempt is successful if either incompatible types are found in the root or, recursively, there is some successor of the current type in IT2,A that cannot be mapped to any neighbor in I1. Since the anonymous part of IT2,A is not explicit in the input, the current type is stored in the states, and the generating relation t ⇝T2 r t′ is "hardcoded" into the transition function. For Condition (2a), A4

non-deterministically guesses a Σ-subtree I and proceeds as in (1); Condition (2b) is verified based on Theorem 12 by pre-computing →fin Σ . Thus the number of states of A4 is exponential in T2 (because of the types) but only polynomial in |T1|. Automata A1, A2, A3 have polynomially many states.

In the special case of stCQ entailment, we simply replace A4 with a 2ATAc A′4 that refutes the simulation condition of Theorem 11 analogously to how A4 refutes Condition (1).

To obtain the desired upper complexity bounds for query and deductive entailment, we observe that, in both cases, A can be constructed in time polynomial in |T1| and exponential in |T2|, and the emptiness check adds an exponential blowup (Theorem 15). For deductive entailment, we use the reduction to stCQ entailment (Lemma 7).

Theorem 16 InHorn-ALCHIF, the following problems can be decided in time 22p(|T2|log|T1|) , p a polynomial: (Γ, Σ)-CQ entailment, (Γ, Σ)-CQ inseparability, and (Γ, Σ)-CQ conservative extensions. The same holds for Σ-deductive entailment, Σ-deductive inseparability, and Σ-deductive conservative extensions in ELHIF⊥.

Matching lower bounds for all problems except deductive entailment are provided by [Botoeva et al., 2016c]. They hold even in the case where Γ = Σ.

Corollary 17 In any fragment of Horn-ALCHIF that contains ELI or Horn-ALC, the following problems are 2EXPTIME-complete: (Γ,Σ)-CQ entailment, (Γ,Σ)-CQ inseparability, and (Γ, Σ)-CQ conservative extensions.

In the description logic EL, which is ELI without inverse roles, deductive conservative extensions and deductive Σ-entailment are EXPTIME-complete [Lutz and Wolter, 2010]. This raises the question whether the upper bound for deductive entailment reported in Theorem 16 is tight. While we leave this question open, we observe that the transition from EL to ELI does increase the complexity of deductive conservative extensions and related problems to at least CONEXPTIME. We consider this a surprising result since in reasoning problems that are not defined in terms of conjunctive queries, adding inverse roles does typically not result in an increase of complexity. The following is established by a non-trivial reduction of a tiling problem.

Theorem 18 In ELI and in ELHIF⊥, deductive conservative extensions, deductive Σ-entailment, and deductive Σinseparability are CONEXPTIME-hard.

5 Conclusion

As future work, it would be interesting to close the gap in complexity between CONEXPTIME and 2EXPTIME for deductive entailment in ELI and ELHIF⊥. Furthermore, it would be interesting to extend the results to ontology languages from the family of Datalog+/- (aka existential rules), in particular to frontier-guarded TGDs.

Acknowledgments

This work was partially supported by DFG project LU 1417/2 and ERC Consolidator Grant 647289 CODA.