Query-Based Entailment and Inseparability for ALC Ontologies

1 Introduction

In recent years, data access using description logic (DL) TBoxes has become one of the most important applications of DLs [Poggi et al., 2008; Bienvenu and Ortiz, 2015], where the underlying idea is to use a TBox to specify semantics and background knowledge for the data (stored in an ABox), and thereby derive more complete query answers. A major research effort has led to the development of efficient algorithms and tools for a number of DLs ranging from DL-Lite [Calvanese et al., 2007; Rodriguez-Muro et al., 2013] via more expressive Horn DLs such as Horn-ALC [Eiter et al., 2012; Trivela et al., 2015] to DLs with all Boolean constructors such as ALC [Kollia and Glimm, 2013; Zhou et al., 2015].

While query answering with DLs is now well-developed, this is much less the case for reasoning services that support ontology engineering and target query answering as an application. In ontology versioning, for example, one would like to know whether two versions of an ontology give the same answers to all queries formulated over a given vocabulary of interest, which means that the newer version can safely replace the older one [Konev et al., 2012]. Similarly, if one wants to know whether an ontology can be safely replaced by a smaller subset (module), it is the answers to all queries that should be preserved [Kontchakov et al., 2010]. In this context, the fundamental relationship between ontologies is thus not whether they are logically equivalent (have the same models), but whether they give the same answers to any relevant query.

The resulting entailment problem can be formalized in two ways, with different applications. First, given a class Q of queries, knowledge bases (KBs) K1 and K2, and a signature ⌃ of relevant concept and role names, we say that K1 ⌃-Qentails K2 if the answers to any ⌃-query in Q over K2 are contained in the answers to the same query over K1. Further, K1 and K2 are ⌃-Q-inseparable if they ⌃-Q-entail each other. Note that a KB includes an ABox, and thus this notion of entailment is appropriate if the data is known and does not change frequently. Applications include data-oriented KB versioning and KB module extraction, KB forgetting [Wang et al., 2014], and knowledge exchange [Arenas et al., 2013].

If the data is not known or changes frequently, it is not KBs that should be compared, but TBoxes. Given a pair ⇥ = (⌃1↪⌃2) that specifies a relevant signature ⌃1 for ABoxes and ⌃2 for queries, we say that a TBox T1 ⇥-Qentails a TBox T2 if, for every ⌃1-ABox A, the KB (T1↪A) ⌃2-Q-entails (T2↪A). T1 and T2 are ⇥-Q-inseparable if they ⇥-Q-entail each other. Applications include data-oriented TBox versioning, TBox modularization and TBox forgetting [Kontchakov et al., 2010].

In this paper, we concentrate on the most important choices for Q, conjunctive queries (CQs) and unions thereof (UCQs); we also consider the practically relevant classes of rooted CQs (rCQs) and UCQs (rUCQs), in which every variable is connected to an answer variable. So far, CQ-entailment has been studied for Horn DL KBs [Botoeva et al., 2014], EL TBoxes [Lutz and Wolter, 2010; Konev et al., 2012], DL-Lite TBoxes [Kontchakov et al., 2009], and also for OBDA specifications, that is, DL-Lite TBoxes with mappings [Bienvenu and Rosati, 2015]. No results are available for non-Horn DLs (neither in the KB nor in the TBox case) and for expressive Horn DLs in the TBox case. In particular, query entailment in non-Horn DLs has had the reputation of being a technically challenging problem.

This paper makes a first breakthrough into understanding query entailment and inseparability in these cases, with the main results summarized in Figures 1 and 2 (those marked with (?) are from [Botoeva et al., 2014]). Three of them came as a real surprise to us. First, it turned out that CQ- and rCQentailment between ALC KBs is undecidable, even when the first KB is formulated in Horn-ALC (in fact, EL) and without any signature restriction. This should be contrasted with the decidability of subsumption-based entailment between ALC

rUCQ 2EXPTIME

Figure 1: KB query entailment.

TBoxes [Ghilardi et al., 2006] and of CQ-entailment between Horn-ALC KBs [Botoeva et al., 2014]. The second surprising result is that entailment between ALC KBs becomes decidable when CQs are replaced with rUCQs. For ALC TBoxes, CQ- and rCQ-entailment are undecidable as well. We obtain decidability for Horn-ALC TBoxes (where CQ- und UCQentailments coincide) using the fact that non-entailment is always witnessed by tree-shaped ABoxes. As another surprise, CQ-entailment of Horn-ALC TBoxes is 2EXPTIMEcomplete while rCQ-entailment is only EXPTIME-complete. This should be contrasted with the EL case, where both problems are EXPTIME-complete [Lutz and Wolter, 2010]. All upper bounds and most lower bounds hold also for inseparability in place of entailment. A model-theoretic foundation for these results is a characterization of query entailment between KBs and TBoxes in terms of (partial) homomorphisms, which, in particular, enables the use of tree automata techniques to establish the upper bounds in Figs. 1 and 2. Omitted proofs are available in the full version [Botoeva et al., 2016].

2 Preliminaries

Fix lists of individual names ai, concept names Ai, and role names Ri, for i < !. ALC-concepts, C, are defined by the grammar

We use ?, C1 t C2 and 8R▷C as abbreviations for ≻>, ≻(≻C1 u ≻C2) and ≻9R▷≻C, respectively. A concept inclusion (CI) takes the form C v D, where C and D are concepts. An ALC TBox is a finite set of CIs. In a Horn-ALC TBox, no concept of the form ≻C occurs negatively and no 9R▷≻C occurs positively [Hustadt et al., 2005; Kazakov, 2009]. An EL TBox does not contain ≻ at all. An ABox, A, is a finite set of assertions of the form Ak(ai) or Rk(ai↪ aj); ind(A) is the set of individual names in A. Taken together, T and A form a knowledge base (KB) K = (T ↪ A); we set ind(K) = ind(A).

A conjunctive query (CQ) q(x) is a formula 9y'(x↪ y), where ' is a conjunction of atoms of the form Ak(z1) or Rk(z1↪ z2) with zi in x↪ y; the variables in x are the answer variables of q(x). We call q rooted (rCQ) if every y 2 y is connected to some x 2 x by a path in the graph whose

The semantics is defined as usual based on interpretations I = (∆I ↪ ·I ) that comply with the standard name assumption in the sense that aIi = ai [Baader et al., 2003]. We write I ♣= ↵ if an inclusion or assertion ↵ is true in I. If I ♣= ↵, for all ↵ 2 T [ A, then we call I a model of K and write I ♣= K. K is consistent if it has a model; we then also say that A is consistent with T . K ♣= ↵ means that I ♣= ↵ for all I ♣= K.

nodes are the variables in q and edges are the pairs ¶u↪ v♦ with R(u↪ v) 2 q, for some R. A union of CQs (UCQ) is a disjunction q(x) = Wi qi(x) of CQs qi(x) with the same answer variables x; it is rooted (rUCQ) if all qi are rooted.

A set M of models of a KB K is called complete for K if, for every UCQ q(x), we have K ♣= q(a) iff I ♣= q(a) for all I 2 M. We call an interpretation I a ditree interpretation if the directed graph GI with nodes d 2 ∆I and edges (d↪ e) 2 RI , for some R, is a tree and RI \ SI = ;, for any distinct roles R and S. I has outdegree n if GI has outdegree n. A model I of a KB K = (T ↪A) is forest-shaped if I is the disjoint union of ditree interpretations Ia with root a, for a 2 ind(A), extended with all R(a↪ b) 2 A. The outdegree of I is the maximum outdegree of the Ia. It is well known that the class M fo K of all forest-shaped models of an ALC KB K of outdegree bounded by ♣T ♣ is complete for K [Lutz, 2008]. If K is a Horn-ALC KB, then a single member IK of M fo K is complete for K. IK is constructed using the standard chase procedure and called the canonical model of K.

A tuple a in ind(K) is a certain answer to a UCQ 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. The problem of checking whether a tuple is a certain answer to a given (U)CQ over a given ALC KB is known to be EXPTIME-complete for combined complexity [Lutz, 2008]. The EXPTIME lower bound actually holds for Horn-ALC [Kr¨otzsch et al., 2013].

A signature, ⌃, is a set of concept and role names. By a ⌃-concept, ⌃-CQ, etc. we understand any concept, CQ, etc. constructed using the names from ⌃. We say that ⌃ is full if it contains all concept and role names. A model I of a KB K is ⌃-connected if, for any u 2 ∆I ∩ ind(K), there is a path RI 1 (a↪ u1)↪ ▷ ▷ ▷ ↪ RIn (un↪ u) with a 2 ind(K) and the Ri in ⌃.

Definition 1. Let K1 and K2 be consistent KBs, ⌃ a signature, and Q one of CQ, rCQ, UCQ or rUCQ. We say that K1 ⌃-Q-entails K2 if K2 ♣= q(a) implies a ✓ ind(K1) and K1 ♣= q(a), for all ⌃-Q q(x) and all tuples a in ind(K2). K1 and K2 are ⌃-Q inseparable if they ⌃-Q entail each other.

As larger classes of queries separate more KBs, ⌃-UCQ inseparability implies all other inseparabilities. The following example shows that, in general, no other implications between the different notions of inseparability hold for ALC.

Now, let ⌃1 = ¶E↪B♦, T1 = ;, and T 0 1 = ¶E v 9R▷B♦. Let A1 = ¶E(a)♦, K1 = (T1↪A1), and K01 = (T 0 1 ↪ A1).

Example 2. Suppose T0 = ;, T 0 0 = ¶E v A t B♦ and ⌃0 = ¶A↪B↪E♦. Let A0 = ¶E(a)♦, K0 = (T0↪A0), and K00 = (T 0 0 ↪ A0). Then K0 and K00 are ⌃0-CQ inseparable but not ⌃0-rUCQ inseparable. In fact, K00 ♣= q(a) and K0 6♣= q(a) for q(x) = A(x) _ B(x).

Then K1 and K01 are ⌃1-rUCQ inseparable but not ⌃1-CQ inseparable. In fact, K01 ♣= 9xB(x) but K1 6♣= 9xB(x).

Definition 3. Let T1 and T2 be TBoxes, Q one of CQ, rCQ, UCQ or rUCQ, and let ⇥ = (⌃1↪ ⌃2) be a pair of signatures. We say that T1 ⇥-Q entails T2 if, for every ⌃1-ABox A that is consistent with both T1 and T2, the KB (T1↪ A) ⌃2-Q entails the KB (T2↪A). T1 and T2 are ⇥-Q inseparable if they ⇥- Q entail each other. If ⌃1 is the set of all concept and role names, we say 'full ABox signature ⌃2-Q entails' or 'full ABox signature ⌃2-Q inseparable'.

We only consider ABoxes that are consistent with both TBoxes because the problem whether a ⌃1-ABox consistent with T2 is also consistent with T1 is well understood: it is mutually polynomially reducible with the containment problem for ontology-mediated queries with CQs of the form 9xA(x), which is NEXPTIME-complete for ALC and EXPTIME-complete for Horn-ALC [Bienvenu et al., 2012; 2014].

Example 4. Consider the TBoxes T0 and T 0 0 from Example 2 and let ⇥ = (⌃↪ ⌃) for ⌃ = ¶R↪ A↪ B↪ E♦. Then T0 does not ⇥-rCQ entail T 0 0 as (T 0 0 ↪ A) ♣= q(a) and (T0↪ A) 6♣= q(a) for

We observe that ⇥-CQ-entailment in the restricted case with ⇥ = (⌃↪ ⌃) has been investigated for EL TBoxes by Lutz and Wolter [2010] and Konev et al. [2012].

As in the KB case, ⌃-UCQ inseparability of ALC TBoxes implies all other types of inseparability, and Example 2 can be used to show that no other implications hold in general. The situation changes for Horn-ALC KBs and TBoxes. The following can be proved by observing that a Horn-ALC KB entails a UCQ iff it entails one of its disjuncts:

Theorem 5. Let K1 be an ALC KB and K2 a Horn-ALC KB. Then K1 ⌃-UCQ entails K2 iff K1 ⌃-CQ entails K2. The same holds for rUCQ and rCQ, and for TBox entailment.

3 Model-Theoretic Criteria for ALC KBs

Suppose Ii is an interpretation for a KB Ki, i = 1↪ 2. A function h: ∆I2 ! ∆I1 is called a ⌃-homomorphism if u 2 AI2 implies h(u) 2 AI1 and (u↪ v) 2 RI2 implies (h(u)↪ h(v)) 2 RI1 for all u↪ v 2 ∆I2 , ⌃-concept names A, and ⌃-role names R, and h(a) = a for all a 2 ind(K2). It is known from database theory that homomorphisms characterize CQ-containment [Chandra and Merlin, 1977]. For KB ⌃-query entailment, finite partial homomorphisms are required. We say that I2 is n⌃-homomorphically embeddable into I1 if, for any subinterpretation I 02 of I2 with ♣∆I 02 ♣  n, there is a ⌃-homomorphism from I 02 to I1. If, additionally, we require I 02 to be ⌃-connected then I2 is said to be con-n⌃- homomorphically embeddable into I1.

We now give model-theoretic criteria for ⌃-entailment between KBs. The product Q I of a set I of interpretations is defined as usual in model theory [Chang and Keisler, 1990, page 405]. Note that, for any CQ q(x) and any tuple a of individual names, Q I ♣= q(a) iff I ♣= q(a) for each I 2 I.

Theorem 6. Let K1 and K2 be ALC KBs, ⌃ a signature, and let Mi be complete for Ki, i = 1↪ 2.

1. K1 ⌃-UCQ entails K2 iff, for any n > 0 and I1 2 M1, there exists I2 2 M2 that is n⌃-homomorphically embeddable into I1.
2. K1 ⌃-CQ entails K2 iff Q M2 is n⌃-homomorphically embeddable into Q M1 for any n > 0.
3. K1 ⌃-rUCQ entails K2 iff, for any n > 0 and I1 2 M1, there exists I2 2M2 that is con-n⌃-homomorphically embeddable into I1.
4. K1 ⌃-rCQ entails K2 iff Q M2 is con-n⌃-homomorphically embeddable into Q M1 for any n > 0.

Proof. We only show (1). Suppose K2 ♣= q but K1 6♣= q. Let n be the number of variables in q. Take I1 2 M1 such that I1 6♣= q. Then no I2 2 M2 is n⌃-homomorphically embeddable into I1. Conversely, suppose I1 2M1 is such that, for some n, no I2 2 M2 is n⌃-homomorphically embeddable into I1. We can regard any subinterpretation of any I2 2 M2 with domain of size  n as a CQ (with answer variable corresponding to ABox individuals). The disjunction of all such CQs is entailed by K2 but not by K1.

Note that n⌃-homomorphic embeddability cannot be replaced by ⌃-homomorphic embeddability. For example, in (1), let K1 = K2 = (¶> v 9R▷>♦↪ ¶A(a)♦), M1 = ¶I1♦, where I1 is the infinite R-chain starting with a, and let M2 contain arbitrary finite R-chains starting with a followed by an arbitrary long R-cycle. M1 and M2 are both complete for K, but there is no ⌃-homomorphism from any I2 2 M2 to I1. In Section 5, we show that in some cases we can find characterizations with full ⌃-homomorphisms and use them to present decision procedures for entailment.

If both Mi are finite and contain only finite interpretations, then Theorem 6 provides a decision procedure for KB entailment. This applies, for example, to KBs with acyclic classical TBoxes [Baader et al., 2003], and to KBs for which the chase terminates [Grau et al., 2013].

4 Undecidability for ALC KBs and TBoxes

We show that CQ and rCQ-entailment and inseparability for ALC KBs are undecidable-even if the signature is full and K1 is a Horn-ALC (in fact, EL) KB. We establish the same results for TBoxes except that in the rCQ case, we leave it open whether the full ABox signature is sufficient for undecidability.

Theorem 7. (i) The problem whether a Horn-ALC KB ⌃-Q entails an ALC KB is undecidable for Q 2 ¶CQ↪ rCQ♦.

• (iii) Both (i) and (ii) hold for the full signature ⌃.

(ii) ⌃-Q inseparability between Horn-ALC and ALC KBs is undecidable for Q 2 ¶CQ↪ rCQ♦.

Proof. The proof is by reduction of the undecidable N ⇥Mtiling problem: given a finite set T of tile types T with four colours up(T), down(T), left(T) and right(T), a tile type I 2 T, and two colours W (for wall) and C (for ceiling), decide whether there exist N↪M 2 N such that the N ⇥M grid can be tiled using T in such a way that (1↪ 1) is covered by a tile of type I; every (N↪ i), for i  M, is covered by a tile of type T with right(T) = W; and every (i↪M), for i  N, is covered by a tile of type T with up(T) = C.

Given an instance of this problem, we first describe a KB K2 = (T2↪ ¶A(a)♦) that uses (among others) 3 concept names Tk, k = 0↪ 1↪ 2, for each tile type T 2 T. If a point x in a model I of K2 is in Tk and right(T) = left(T 0 ), then x has an R-successor in T 0k . Thus, branches of I define (possibly infinite) horizontal rows of tilings with T. If a branch contains a point y 2 Tk with right(T) = W, then this y can be the last point in the row, which is indicated by an R-successor z 2 Row of y. In turn, z has R-successors in all T(k+1)mod 3 that can be possible beginnings of the next row of tiles. To coordinate the up and down colours between the rows-which will be done by the CQs separating K1 and K2- we make every x 2 Tk, starting from the second row, an instance of all T 0 (k-1) mod 3 with down(T ) = up(T 0 ). The row started by z 2 Row can be the last one in the tiling, in which case we require that each of its tiles T has up(T) = C. After the point in Row indicating the end of the final row, we add an R-successor in End for the end of tiling. The beginning of the first row is indicated by a P-successor in Start of the ABox element a, after which we add an R-successor in I0 for the given initial tile type I; see the lowest branch in Fig. 3. To generate a tree with all possible branches described above, we only require EL axioms of the form E v D and E v 9S▷D.

The existence of a tiling of some N ⇥M grid for the given instance can be checked by Boolean CQs qn that require an R-path from Start to End going through Tk- or Row-points:

with Bi 2 ¶Row♦ [ ¶Tk ♣ T 2 T↪ k = 0↪ 1↪ 2♦; see Fig. 3. The key trick is-using an axiom of the form D v EtE0-to ensure that the Row-point before the final row of the tiling has two alternative continuations: one as described above, and the other one having just a single R-successor in End; see Fig. 3 where _ indicates an or-node. This or-node gives two models of K2 denoted Il and Ir in the picture. If K2 ♣= qn, then qn holds in both of them, and so there are homomorphisms hl : qn ! Il and hr : qn ! Ir. As hl(xn-1) and hr(xn-1) are instances of Bn-1, we have Bn-1 = T NM-1 1 in the picture, and so up(T NM-1 ) = down(T NM ). By repeating this argument until x0, we see that the colours between horizontal rows match and the rows are of the same length. (For this trick to work, we have to make the first Row-point in every branch an instance of Start.) In fact, we have:

Lemma 8. An instance of the N ⇥M-tiling problem has a positive answer iff there exists qn such that K2 ♣= qn.

It is to be noted that to construct T2 with the properties described above one needs quite a few auxiliary concept names.

Next, we define K1 = (T1↪ ¶A(a)♦) to be the EL KB with the following canonical model:

where ⌃0 = ¶Row♦ [ ¶Tk ♣ T 2 T↪ k = 0↪ 1↪ 2♦. Note that the vertical R-successors of the Start-points are not instances of any concept name, and so K1 does not satisfy any query qn. On the other hand, K2 ♣= q implies K1 ♣= q, for every ⌃-CQ q without a subquery of the form qn and ⌃ = sig(K1).

This proves (i) for ⌃-CQ entailment. For ⌃-rCQ entailment, we slightly modify the construction, in particular, by adding R(a↪ a) and Row(a) to the ABox ¶A(a)♦, and a conjunct R(y↪ x0) with a free y to qn. (The loop R(a↪ a) plays roughly the same role as the path between two Start-points in Fig. 3.) To prove (ii), we take K02 = K2 [ K1 and show that K1 ⌃-CQ entails K2 iff K1 and K02 are ⌃-CQ inseparable. Finally, we prove (iii) by replacing non-⌃ symbols in K2 with complex ALC-concepts that cannot be used in CQs and extending the TBoxes appropriately; cf. [Lutz and Wolter, 2012, Lemma 21].

The TBoxes from the proof above can also be used to obtain

Theorem9. (i) The problemwhether a Horn-ALC TBox ⇥-Q entails an ALC TBox is undecidable for Q 2 ¶CQ↪ rCQ♦.

(iii) For CQs, (i) and (ii) hold for full ABox signatures and for ⇥ = (⌃1↪ ⌃2) with ⌃1 = ⌃2.

(ii) ⇥-Q inseparability between Horn-ALC and ALC TBoxes is undecidable for Q 2 ¶CQ↪ rCQ♦.

Observe that our undecidability proof does not work for UCQs as the UCQ composed of the two disjunctive branches shown in Fig. 3 (for non-trivial instances) distinguishes between the KBs independently of the existence of a tiling. We now show that, at least for rUCQs, entailment is decidable.

5 rUCQ-Entailment for ALC-KBs

Theorem 7 might seem to suggest that any reasonable notion of query inseparability is undecidable for ALC KBs. Interestingly, this is not the case: we show now that rUCQ-entailment is decidable. We first strengthen the characterization of Theorem 6 (2), and then develop a decision procedure based on tree automata. The first step replaces con-n⌃-homomorphic embeddability with con-⌃-homomorphic embeddability, where I2 is con-⌃-homomorphically embeddable into I1 if the maximal ⌃-connected subinterpretation of I2 is ⌃- homomorphically embeddable into I1.

Theorem 10. Let K1 and K2 be ALC KBs, ⌃ a signature, and let M1 be complete for K1. Then K1 ⌃-rUCQ entails K2 iff for any I1 2M1, there exists I2 ♣= K2 such that I2 is con-⌃-homomorphically embeddable into I1.

Proof. In viewof Theorem6 (2), it suffices to prove ()). Suppose I1 2 M1. By Theorem 6 (2), for every n ≥ 0, we have J 2Mfo K2 and a ⌃-homomorphism hn : J♣n ! I1, where J♣n is the subinterpretation of J whose elements are connected to ABox individuals by ⌃-paths of length  n. Clearly, for any n ≥ 0, there are only finitely many non-isomorphic pairs (J♣n↪ hn). It can be shown that, thus, one can construct the required I2 2 Mfo K2 and con-⌃-homomorphism h as the limits of suitable chains J♣0 ✓ J♣1 ✓ · · · and h0 ✓ h1 ✓ · · · , respectively.

For the second step, let K1, K2 be ALC-KBs and ⌃ a signature. We use two-way alternating automata on infinite trees (2ATAs) with a trivial acceptance condition (every run is accepting) and employ Theorem 10 for the class M fo K1 , encoding forest-shaped interpretations as labeled trees to make them accessible to 2ATAs. A tree is a non-empty (possibly infinite) set T ✓ ⇤ closed under prefixes with root ". We say that T is m-ary if, for every x 2 T , the set ¶i ♣ x · i 2 T♦ is of cardinality m. Let Γ be an alphabet with symbols from the set

where CN(Ti) (resp. RN(Ti)) denotes the set of concept (resp. role) names in Ti. A Γ-labeled tree is a pair (T↪L) with T a tree and L: T ! Γ a node labeling function. We represent forest-shaped models of T1 as m-ary Γ-labeled trees, with m = max(♣T1♣↪ ♣ind(K1)♣). The root node labeled with root is not used in the representation. Each ABox individual is represented by a successor of the root labeled with a symbol from ind(K1) ⇥ 2CN(T1) ; non-ABox elements are represented by nodes deeper in the tree labeled with a symbol fromRN(T1) ⇥2CN(T1) . The label empty is used for padding to make sure that every tree node has exactly m successors.

Now we construct three 2ATAs Ai, for i = 0↪ 1↪ 2. A0 ensures that the tree is labeled in a meaningful way, e.g. that the root label only occurs at the root node; A1 accepts Γ-labeled trees that represent a model of K1, and A2 accepts Γ-labeled trees (T↪ L) which represent an interpretation I(T↪L) such that some model of K2 is con-⌃-homomorphically embeddable into I(T↪L). The most interesting automaton is A2, which guesses a model of K2 along with a homomorphism to I(T↪L);

in fact, both can be read off from a successful run of the automaton. The number of states of the Ai is exponential in ♣K1 [K2♣. It then remains to combine these automata into a single 2ATA A such that L(A) = L(A0) \ L(A1) \ L(A2), which is possible with only polynomial blowup, and to test (in time exponential in the number of states) whether L(A) = ;.

Theorem 11. It is in 2EXPTIME to decide whether an ALC KB K1 ⌃-rUCQ entails an ALC KB K2.

The best known lower bound is EXPTIME, which is easy to establish by reduction from satisfiability.

6 (r)CQ-Entailment for (Horn-)ALC-TBoxes

We show that CQ- and rCQ-entailment between ALC TBoxes becomes decidable when the second TBox is given in HornALC. In this case, entailments for CQs and UCQs and, respectively, rCQs and rUCQs coincide. We start with rCQs.

Our first observation is that if a ⌃1-ABox is a witness for non-⇥-rCQ entailment, then one can find a witness ⌃1-ABox that is tree-shaped and of bounded outdegree. Here, an ABox A is tree-shaped if the graph with nodes ind(A) and edges ¶a↪ b♦ for each R(a↪ b) 2 A is a tree, and R(a↪ b) 2 A implies S(a↪ b) ◁2 A for all S 6= R and S(b↪ a) ◁2 A for all S.

Theorem 12. Let T1 be an ALC TBox, T2 a Horn-ALC TBox, and ⇥ = (⌃1↪⌃2). Then T1 ⇥-rCQ-entails T2 iff, for all tree-shaped ⌃1-ABoxes A of outdegree bounded by ♣T2♣ and consistent with T1 and T2, IT2↪A is con-⌃2-homomorphically embeddable into any model I1 of (T1↪A).

Proof. It is known that Horn-ALC is unravelling tolerant, that is, (T ↪A) ♣= C(a) for a Horn-ALC TBox T and ELconcept C iff (T ↪ A0 ) ♣= C(a) for a finite sub-ABox A0 of the tree-unravelling of A at a [Lutz and Wolter, 2012]. Thus, any witness ABox for non-entailment w.r.t. EL-instance queries can be transformed into a tree-shaped witness ABox. The result follows by observing that if T1 does not ⇥-rCQ-entail T2, then this is witnessed by an EL-instance query and by applying Theorem 10 to the KBs. The bound on the outdegree is obtained by a careful analysis of derivations.

For the automaton construction, let T1 be an ALC TBox, T2 a Horn-ALC TBox, and ⇥ = (⌃1↪ ⌃2) a pair of signatures. Though Theorem 12 provides a natural characterization that is similar in spirit to Theorem 10, we first need a further analysis of con-⌃2-homomorphic embeddability in terms of simulations whose advantage is that they are more compositional (they can be partial and are closed under union).

Let I1↪ I2 be interpretations and ⌃ a signature. A relation S ✓ ∆I1 ⇥∆I2 is a ⌃-simulation from I1 to I2 if (i) d 2 AI1 and (d↪ d0 ) 2 S imply d0 2 AI2 for all ⌃-concept names A, and (ii) if (d↪ e) 2 RI1 and (d↪ d0 ) 2 S then there is a (d0 ↪ e0 ) 2 RI2 with (e↪ e0 ) 2 S for all ⌃-role names R. Let di 2 ∆Ii , i 2 ¶1↪ 2♦. (I1↪ d1) is ⌃-simulated by (I2↪ d2), in symbols (I1↪ d1) ⌃ (I2↪ d2), if there exists a ⌃-simulation S with (d1↪ d2) 2 S.

Lemma 13. Let A be a ⌃1-ABox and I1 a model of (T1↪ A). Then IT2↪A is not con-⌃2-homomorphically embeddable into I1 iff there is a 2 ind(A) such that one of the following holds:

1. there is a ⌃2-concept name A with a 2 AIT2↪A ∩ AI1 ;
2. there is an R-successor d of a in IT2↪A, for some ⌃2-role name R, such that d ◁2 ind(A) and, for all R-successors e of a in I1, we have (IT2↪A↪ d) 6⌃2 (I1↪ e).

We use a mix of two-way alternating B¨uchi automata on finite trees (2ABTAs) and non-deterministic top-down automata on finite trees (NTAs). A finite tree T is m-ary if, for every x 2 T , the set ¶i ♣ x·i 2 T♦ is of cardinality zero or exactly m. We use labeled trees to represent a tree-shaped ABox A and a model I1 such that, for some a 2 ind(A), conditions (1) and (2) from Lemma 13 are satisfied, and thus IT2↪A is not con-⌃2-homomorphically embeddable into I1. To ensure that later, additional bookkeeping information is needed. Node labels are taken from the alphabet

where Γ0 is the set of all subsets of ⌃1 [ ¶R- ♣ R 2 ⌃1♦ that contain at most one role (a role name R or its inverse R-), cl(Ti) is the set of subconcepts of (concepts in) Ti closed under single negation, and sub(T2) is the set of subconcepts of (concepts in) T2. For a Γ-labeled tree (T↪ L) and a node x from T , we use Li(x) to denote the (i+1)st component of L(x), where i 2 ¶0↪ ▷ ▷ ▷ ↪ 4♦. Intuitively, the L0-component represents the ABox A, the L1-component the model I1, the L2-component represents IT2↪A, and the L3- and L4-components help to guarantee conditions (1) and (2) from Lemma 13.

To ensure that each component i 2 ¶0↪ ▷ ▷ ▷ ↪ 4♦ indeed represents what it is supposed to, we impose on it an i-properness condition. For example, a Γ-labeled (T↪ L) tree is 0-proper if (i) L0(") contains no role and (ii) for every non-root node x of T , L0(x) contains a role. A 0-proper Γ-labeled tree (T↪ L) represents the following tree-shaped ⌃1-ABox:

Due to space limitations, we skip the remaining definitions of properness and concentrate on explaining the most interesting components L3 and L4 of Γ-labels. The L3-component marks a single node x in the tree, which is the individual a from Lemma 13 that satisfies conditions (1) and (2). If (1) is satisfied, we do not need the L4-component. Otherwise, we store in that component at x a set of concepts S = ¶9R▷A↪ 8R▷B1↪ ▷ ▷ ▷ ↪ 8R▷Bn♦ such that R 2 ⌃2 and all concepts from S are true at x in IT2↪A. This successor set represents the R-successor d in condition (2) of Lemma 13. We then have to make sure that, for any neighboring node y of x that represents an R-successor of x in A(T↪L), we have (IT2↪A↪ d) 6⌃2 (I1↪ y). This can again happen via a concept name or via a successor; we are done in the fomer case and use the L4-component of y in the latter. It is important to note that we can never return to the same node in this tracing process since we only follow roles in the forward direction and the represented ABox is tree-shaped. This is crucial for achieving the EXPTIME overall complexity.

We show that T2 is not ⇥-rCQ-entailed by T1 iff there is an m-ary Γ-labeled tree that is i-proper for any i 2 ¶0↪ ▷ ▷ ▷ ↪ 4♦. It then remains to design a 2ABTA A that accepts exactly those trees. We construct A as the intersection of five automata Ai, i < 5, where each Ai ensures i-properness. Some of the automata are 2ABTAs with polynomially many states while others are NTAs with exponentially many states. We mix automata models since some properness conditions (2properness) are much easier to describe with a 2ABTA while for others (4-properness), it does not seem to be possible to construct a 2ABTA with polynomially many states. In summary, we obtain the following result.

Theorem 14. It is EXPTIME-complete to decide whether an ALC TBox T1 (⌃1↪ ⌃2)-rCQ entails a Horn-ALC TBox T2.

Note that the EXPTIME lower bound holds already for entailment of EL TBoxes and ⌃1 = ⌃2 [Lutz and Wolter, 2010]. We now study the non-rooted case, starting with an analogue of Theorem 12. As expected, moving to unrestricted queries corresponds to moving to unrestricted homomorphisms.

Theorem 15. Let T1 and T2 be Horn-ALC TBoxes and ⇥ = (⌃1↪ ⌃2). Then T1 ⇥-CQ entails T2 iff, for all tree-shaped ⌃1ABoxes A of outdegree  ♣T2♣ and consistent with T1 and T2, IT2↪A is ⌃2-homomorphically embeddable into IT1↪A.

The automata construction described above can largely be reused for this case. The main difference is that the two conditions in Lemma 13 need to be extended with a third one: there is an element d in the subtree of IT2↪A rooted at a that has an R-successor d0, R ◁2 ⌃2, such that, for all elements e of I1, we have (I2↪ d0) 6⌃2 (I1↪ e). To deal with this condition, it becomes necessary to store multiple successor sets in the L4components instead of only a single one, which increases the overall complexity to 2EXPTIME. A matching lower bound can be proved by a (non-trivial) reduction of the word problem for exponentially bounded alternating Turing machines.

Theorem 16. ⇥-CQ entailment for Horn-ALC TBoxes is 2EXPTIME-complete. The lower bound holds for ⇥ = (⌃↪ ⌃).

7 FutureWork

We have made first steps towards understanding query entailment and inseparability for KBs and TBoxes in expressive DLs. Many problems remain to be addressed. From a theoretical viewpoint, it would be of interest to solve the open problems in Figures 1 and 2, and also consider other expressive DLs such as DL-Lite Hbool [Artale et al., 2009] or ALCI. For example, if Theorem 10 could be generalized to UCQs (and ⌃-homomorphisms), we would obtain a 2EXPTIME upper bound for UCQ-entailment between ALC KBs using the same technique as for rUCQs. Also, our undecidability proof goes through for DL-Lite Hbool , but the other cases remain open. From a practical viewpoint, our model-theoretic criteria for query entailment are a good starting point for developing algorithms for approximations of query entailment based on simulations. Our undecidability and complexity results also indicate that rUCQ-entailment is more amenable to practical algorithms than, say, CQ-entailment and can be used as an approximation of the latter.

Acknowledgments. This work has been supported by the EU IP project Optique, grant n. FP7-318338, DFG grant LU 1417/2-1, and EPSRC UK grants EP/M012646/1 and EP/M012670/1 (iTract).