First Order-Rewritability and Containment of Conjunctive Queries in Horn Description Logics

1 Introduction

When ontologies are used to enrich incomplete and heterogeneous data with a semantics and with background knowledge [Calvanese et al., 2009; Kontchakov et al., 2013; Bienvenu and Ortiz, 2015], efficient query anwering is a primary concern. Since classical database systems are unaware of ontologies and implementing new ontology-aware systems that can compete with these would be a huge effort, a main approach used today is query rewriting: the user query q and the ontology O are combined into a new query qO that produces the same answers as q under O (over all inputs) and can be handed over to a database system for execution. Popular target languages for the query qO include SQL and Datalog. In this paper, we concentrate on ontologies formulated in description logics (DLs) and on rewritability into SQL, which we equate with first-order logic (FO).

FO-rewritability in the context of query answering under DL ontologies was first studied in [Calvanese et al., 2007]. Since FO-rewritings are not guaranteed to exist when ontologies are formulated in traditional DLs, the authors introduce the DL-Lite family of DLs specifically for the purpose of ontologyaware query answering using SQL database systems; in fact, the expressive power of DL-Lite is seriously restricted, in this way enabling existence guarantees for FO-rewritings. While DL-Lite is a successful family of DLs, there are many applications that require DLs with greater expressive power. The potential non-existence of FO-rewritings in this case is not necessarily a problem in practical applications. In fact, ontologies emerging from such applications typically use the available expressive means in a harmless way in the sense that efficient reasoning is often possible despite high worst-case complexity.

Frank Wolter

University of Liverpool, UK frank@csc.liv.ac.uk

One might thus hope that, in practice, FO-rewritings can often be constructed also beyond DL-Lite.

This hope was confirmed in [Bienvenu et al., 2013; Hansen et al., 2015], which consider the case where ontologies are formulated in a DL of the EL family [Baader et al., 2005] and queries are atomic queries (AQs) of the form A(x). To describe the obtained results in more detail, let an ontology-mediated query (OMQ) be a triple (T ↪ ⌃↪ q) with T a description logic TBox (representing an ontology), ⌃ an ABox signature (the set of concept and role names that can occur in the data), and q an actual query. Note that T and q might use symbols that do not occur in ⌃; in this way, the TBox enriches the vocabulary available for formulating q. We use (L↪ Q) to denote the OMQ language that consists of all OMQs where T is formulated in the description logic L and q in the query language Q. In [Bienvenu et al., 2013], FO-rewritability is characterized in terms of the existence of certain tree-shaped ABoxes, covering a range of OMQ languages between (EL↪ AQ) and (Horn-SHI↪ AQ). On the one hand, this characterization is used to clarify the complexity of deciding whether a given OMQ is FO-rewritable, which turns out to be EXPTIME-complete. On the other hand, it provides the foundations for developing practically efficient and complete algorithms for computing FO-rewritings. The latter was explored further in [Hansen et al., 2015], where a novel type of algorithm for computing FO-rewritings of OMQs from (EL↪ AQ) is introduced, crucially relying on the previous results from [Bienvenu et al., 2013]. Its evaluation shows excellent performance and confirms the hope that, in practice, FO-rewritings almost always exist. In fact, rewriting fails in only 285 out of 10989 test cases.

A limitation of the discussed results is that they concern only AQs while in many applications, the more expressive conjunctive queries (CQs) are required. The aim of the current paper is thus to study FO-rewritability of OMQ languages based on CQs, considering ontology languages between EL and Horn-SHIF. In particular, we provide characterizations of FO-rewritability in the required OMQ languages that are inspired by those in [Bienvenu et al., 2013] (replacing treeshaped ABoxes with a more general form of ABox), and we analyze the complexity of FO-rewritability using an automatabased approach. While practically efficient algorithms are out of the scope of this article, we believe that our work also lays important ground for the subsequent development of such algorithms. Our approach actually does allow the construction of rewritings, but it is not tailored towards doing that in a practically efficient way. It turns out that the studied FOrewritability problems are closely related to OMQ containment problems as considered in [Bienvenu et al., 2012; Bourhis and Lutz, 2016]. In fact, being able to decide OMQ containment allows us to concentrate on connected CQs when deciding FOrewritability, which simplifies technicalities considerably. For this reason, we also study characterizations and the complexity of query containment in the OMQ languages considered.

Our main complexity results are that FO-rewritability and containment are EXPTIME-complete for OMQ languages between (EL↪ AQ) and (ELHF?↪ CQ) and 2EXPTIMEcomplete for OMQ languages between (ELI↪ CQ) and (Horn-SHIF↪ CQ). The lower bound for containment applies already when both OMQs share the same TBox. Replacing AQs with CQs thus results in an increase of complexity by one exponential in the presence of inverse roles (indicated by I), but not otherwise. Note that the effect that inverse roles can increase the complexity of querying-related problems was known from expressive DLs of the ALC family [Lutz, 2008], but it has not previously been observed for Horn-DLs such as ELI and Horn-SHIF. While 2EXPTIME might appear to be very high complexity, we are fortunately also able to show that the runtime is double exponential only in the size of the actual queries (which tends to be very small) while it is only single exponential in the size of the ontologies. We also show that the complexity drops to NEXPTIME when we restrict our attention to rooted CQs, that is, CQs which contain at least one answer variable and are connected. Practically relevant queries are typically of this kind.

A slight modification of our lower bounds yields new lower bounds for monadic Datalog containment. In fact, we close an open problem from [Chaudhuri and Vardi, 1994] by showing that containment of a monadic Datalog program in a rooted CQ is CONEXPTIME-complete. We also improve the 2EXPTIME lower bound for containment of a monadic Datalog program in a CQ from [Benedikt et al., 2012] by showing that it already applies when the arity of EDB relations is bounded by two, rule bodies are tree-shaped, and there are no constants (which in this case correspond to nominals); the existing construction cannot achieve the latter two conditions simultaneously.

Full proofs are provided at http://www.informatik.unibremen.de/tdki/research/papers.html.

Related work. Pragmatic approaches to OMQ rewriting beyond DL-Lite often consider Datalog as a target language [Rosati, 2007; P´erez-Urbina et al., 2010; Eiter et al., 2012; Kaminski et al., 2014; Trivela et al., 2015]. These approaches might produce a non-recursive (thus FO) rewriting if it exists, but there are no guarantees. FO-rewritability of OMQs based on expressive DLs is considered in [Bienvenu et al., 2014], and based on existential rules in [Baget et al., 2011]. A problem related to ours is whether all queries are FO-rewritable when combined with a given TBox [Lutz and Wolter, 2012; Civili and Rosati, 2015]. There are several related works in the area of Datalog; recall that a Datalog program is bounded if and only if it is FO-rewritable [Ajtai and Gurevich, 1994]. For monadic Datalog programs, boundedness is known to be decidable [Cosmadakis et al., 1988] and 2EXPTIME-complete [Benedikt et al., 2015]; containment is also 2EXPTIME-complete [Cosmadakis et al., 1988; Benedikt et al., 2012]. OMQs from (Horn-SHI↪ CQ) can be translated to monadic Datalog with an exponential blowup, functional roles (indicated by F) are not expressible.

2 Preliminaries and Basic Observations

Let NC and NR be disjoint and countably infinite sets of concept and role names. A role is a role name r or an inverse role r-, with r a role name. A Horn-SHIF concept inclusion (CI) is of the form L v R, where L and R are concepts defined by the syntax rules

with A ranging over concept names and r over roles. In DLs, ontologies are formalized as TBoxes. A Horn-SHIF TBox T is a finite set of Horn-SHIF CIs, functionality assertions func(r), transitivity assertions trans(r), and role inclusions (RIs) r v s, with r and s roles. It is standard to assume that functional roles are not transitive and neither are transitive roles included in them (directly or indirectly). We make the slighty stronger assumption that functional roles do not occur on the right-hand side of role inclusions at all. This assumption seems natural from a modeling perspective and mainly serves the purpose of simplifying constructions; all our results can be extended to the milder standard assumption. An ELIHF? TBox is a Horn-SHIF TBox that contains neither transitivity assertions nor disjunctions in CIs, an ELI TBox is an ELIHF? TBox that contains neither functionality assertions nor RIs, and an ELHF?TBox is an ELIHF? TBox that does not contain inverse roles.

An ABox is a finite set of concept assertions A(a) and role assertions r(a↪ b) where A is a concept name, r a role name, and a↪ b individual names from a countably infinite set NI. We sometimes write r-(a↪ b) instead of r(b↪ a) and use Ind(A) to denote the set of all individual names used in A. A signature is a set of concept and role names. We will often assume that the ABox is formulated in a prescribed signature, which we then call an ABox signature. An ABox that only uses concept and role names from a signature ⌃ is called a ⌃-ABox.

The semantics of DLs is given in terms of interpretations I = (∆I ↪ ·I ), where ∆I is a non-empty set (the domain) and ·I is the interpretation function, assigning to each A 2 NC a set AI ✓ ∆I and to each r 2 NR a relation rI ✓ ∆I ⇥∆I . The interpretation C I ✓ ∆I of a concept C in I is defined as usual, see [Baader et al., 2003]. An interpretation I satisfies a CI C v D if C I ✓ DI , a functionality assertion func(r) if rI is a partial function, a transitivity assertion trans(r) if rI is transitive, an RI r v s if rI ✓ sI , a concept assertion A(a) if a 2 AI , and a role assertion r(a↪ b) if (a↪ b) 2 rI . We say that I is a model of a TBox or an ABox if it satisfies all inclusions and assertions in it. An ABox A is consistent with a TBox T if A and T have a common model. If ↵ is a CI, RI, or functionality assertion, we write T ♣= ↵ if all models of T satisfy ↵.

A conjunctive query (CQ) takes the form q = 9x'(x↪ y) with x↪ y tuples of variables and ' a conjunction of atoms of the form A(x) and r(x↪ y) that uses only variables from x[y. The variables in y are called answer variables, the arity of q is the length of y, and q is Boolean if it has arity zero. An atomic query (AQ) is a conjunctive query of the form A(x). A union of conjunctive queries (UCQ) is a disjunction of CQs that share the same answer variables. Ontology-mediated queries (OMQs) and the notation (L↪Q) for OMQ languages were already defined in the introduction. We generally assume that if a role name r occurs in q and T ♣= s v r, then trans(s) ◁2 T . This is common since allowing transitive roles in the query poses serious additional complications, which are outside the scope of this paper; see e.g. [Bienvenu et al., 2010; Gottlob et al., 2013].

Let Q = (T ↪ ⌃↪ q) be an OMQ, q of arity n, A a ⌃-ABox and a 2 Ind(A)n . We write A ♣= Q(a) if I ♣= q(a) for all models I of T and A. In this case, a is a certain answer to Q on A. We use cert(Q↪A) to denote the set of all certain answers to Q on A.

For any syntactic object O (such as a TBox, a query, an OMQ), we use ♣O♣ to denote the size of O, that is, the number of symbols needed to write it (concept and role names counted as a single symbol).

A first-order query (FOQ) is a first-order formula ' constructed from atoms A(x), r(x↪ y), and x = y; here, concept names are viewed as unary predicates, role names as binary predicates, and predicates of other arity, function symbols, and constant symbols are not permitted. We write '(x) to indicate that the free variables of ' are among x and call x the answer variables of '. The number of answer variables is the arity of ' and ' is Boolean if it has arity zero. We use ans(I↪ ') to denote the set of answers to the FOQ ' on the interpretation I; that is, if ' is n-ary, then ans(I↪ ') contains all tuples d 2 (∆I )n with I ♣= '(d). To bridge the gap between certain answers and answers to FOQs, we sometime view an ABox A as an interpretation IA, defined in the obvious way.

Definition 1 (FO-rewriting). An FOQ ' is an FO-rewriting of an OMQ Q = (T ↪ ⌃↪ q) if cert(Q↪ A) = ans(IA↪ ') for all ⌃-ABoxes A that are consistent with T. If there is such a ', then Q is FO-rewritable.

Example 2. (1) Let Q0 = (T0↪⌃0↪ q0(x↪ y)), where T0 = ¶9r▷A v A↪B v 8r▷A♦, ⌃0 = ¶r↪A↪B♦ and q0(x↪ y) = B(x) ^ r(x↪ y) ^ A(y). Then '0(x↪ y) = B(x) ^ r(x↪ y) is an FO-rewriting of Q0.

We will see in Example 10 that the query QA obtained from Q0 by replacing q0(x↪ y) with the AQ A(x) is not FOrewritable (due to the unbounded propagation of A via r-edges by T0). Thus, an FO-rewritable OMQ can give raise to AQ 'subqueries' that are not FO-rewritable.

(2) Let Q1 = (T1↪⌃1↪ q1(x)), where T1 = ¶9r▷9r▷A v 9r▷A♦, ⌃1 = ¶r↪ A♦, and q1(x) = 9y(r(x↪ y) ^ A(y)). Then Q1 is not FO-rewritable (see again Example 10), but all AQ subqueries that Q1 gives raise to are FO-rewritable.

The main reasoning problem studied in this paper is to decide whether a given OMQ Q = (T ↪ ⌃↪ q) is FO-rewritable. We assume without loss of generality that every symbol in ⌃ occurs in T or in q. We obtain different versions of this problem by varying the OMQ language used. Note that we have defined FO-rewritability relative to ABoxes that are consistent with the TBox. It is thus important for the user to know whether that is the case. Therefore, we also consider FOrewritability of ABox inconsistency. More precisely, we say that ABox inconsistency is FO-rewritable relative to a TBox T and ABox signature ⌃ if there is a Boolean FOQ ' such that for every ⌃-ABox A, A is inconsistent with T iff IA ♣= '().

We now make two basic observations that we use in an essential way in the remaining paper. We first observe that it suffices to concentrate on ELIHF? TBoxes T in normal form, that is, all CIs are of one of the forms A v ?↪A v 9r▷B↪ > v A↪ B1 u B2 v A↪ 9r▷B v A with A↪ B↪ B1↪ B2 concept names and r a role. We use sig(T ) to denote the concept and role names that occur in T .

Apart from FO-rewritability questions, we will also study OMQ containment. Let Qi = (Ti↪ ⌃↪ qi) be two OMQs over the same ABox signature. We say that Q1 is contained in Q2, in symbols Q1 ✓ Q2, if cert(Q1↪ A) ✓ cert(Q2↪ A) holds for all ⌃-ABoxes A that are consistent with T1 and T2.

Proposition 3. Given a Horn-SHIF (resp. ELHF?) TBox T1 and ABox signature ⌃, one can construct in polynomial time an ELIHF? (resp. ELHF?) TBox T2 in normal form such that for every ⌃-ABox A,

1. A is consistent with T1 iff A is consistent with T2;
2. if A is consistent with T1, then for any CQ q that does not use symbols from sig(T2) ∩ sig(T1), we have cert(Q1↪ A) = cert(Q2↪ A) where Qi = (Ti↪ ⌃↪ q).

Theorem 3 yields polytime reductions of FO-rewritability in (Horn-SHIF↪ Q) to FO-rewritability in (ELIHF?↪ Q) for any query language Q, and likewise for OMQ containment and FO-rewritability of ABox inconsistency. It also tells us that, when working with ELHF? TBoxes, we can assume normal form. Note that transitioning from (Horn-SHF↪Q) to (ELHF?↪Q) is not as easy as in the case with inverse roles since universal restrictions on the right-hand side of concept inclusions cannot easily be eliminated; for this reason, we do not consider (Horn-SHF↪Q). From now on, we work with TBoxes formulated in ELIHF? or ELHF? and assume without further notice that they are in normal form.

Our second observation is that, when deciding FOrewritability, we can restrict our attention to connected queries provided that we have a way of deciding containment (for potentially disconnected queries). We use conCQ to denote the class of all connected CQs.

Theorem 4. Let L 2 ¶ELIHF?↪ ELHF?♦. Then FOrewritability in (L↪ CQ) can be solved in polynomial time when there is access to oracles for containment in (L↪Q) and for FO-rewritability in (L↪ conCQ).

To prove Theorem 4, we observe that FO-rewritability of an OMQ Q = (T ↪⌃↪ q) is equivalent to FO-rewritability of all OMQs Q = (T ↪ ⌃↪ qc) with qc a maximal connected component of q, excluding certain redundant such components (which can be identified using containment). Backed by Theorem 4, we generally assume connected queries when studying FO-rewritability, which allows to avoid unpleasant technical complications and is a main reason for studying FO-rewritability and containment in the same paper.

3 Main Results

In this section, we summarize the main results established in this paper. We start with the following theorem.

Theorem 5. FO-rewritability and containment are

1. 2EXPTIME-complete for any OMQ language between (ELI↪ CQ) and (Horn-SHIF↪ CQ), and
2. EXPTIME-complete for any OMQ language between (EL↪ AQ) and (ELHF?↪ CQ).

Moreover, given an OMQ from (Horn-SHIF↪ CQ) that is FO-rewritable, one can effectively construct a UCQ-rewriting.

Like the subsequent results, Theorem 5 illustrates the strong relationship between FO-rewritability and containment. Note that inverse roles increase the complexity of both reasoning tasks. We stress that this increase takes place only when the actual queries are conjunctive queries, since FO-rewritability for OMQ languages with inverse roles and atomic queries is in EXPTIME [Bienvenu et al., 2013].

The 2EXPTIME-completeness result stated in Point 1 of Theorem 5 might look discouraging. However, the situation is not quite as bad as it seems. To show this, we state the upper bound underlying Point 1 of Theorem 5 a bit more carefully.

Theorem 6. Given OMQs Qi = (Ti↪ ⌃i↪ qi), i 2 ¶1↪ 2♦, from (Horn-SHIF↪ CQ), it can be decided

1. in time 22p(♣q1♣+log(♣T1♣)) whether Q1 is FO-rewritable and
2. in time 22p(♣q1♣+♣q2♣+log(♣T1♣+♣T2♣)) whether Q1 ✓ Q2,

for some polynomial p.

Note that the runtime is double exponential only in the size of the actual queries q1 and q2, while it is only single exponential in the size of the TBoxes T1 and T2. This is good news since the size of q1 and q2 is typically very small compared to the sizes of T1 and T2. For this reason, it can even be reasonable to assume that the sizes of q1 and q2 are constant, in the same way in which the size of the query is assumed to be constant in data complexity. Note that, under this assumption, Theorem 6 yields EXPTIME upper bounds.

One other way to relativize the seemingly very high complexity stated in Point 1 of Theorem 5 is to observe that the lower bound proofs require the actual query to be Boolean or disconnected. In practical applications, though, typical queries are connected and have at least one answer variable. We call such CQs rooted and use rCQ to denote the class of all rooted CQs. Our last main result states that, when we restrict our attention to rooted CQs, then the complexity drops to CONEXPTIME.

Theorem 7. FO-rewritability and containment are CONEXPTIME-complete in any OMQ language between (ELI↪ rCQ) and (Horn-SHIF↪ rCQ).

4 Semantic Characterization

The upper bounds stated in Theorems 5 and 6 are established in two steps. We first give characterizations of FO-rewritability in terms of the existence of certain (almost) tree-shaped ABoxes, and then utilize this characterization to design decision procedures based on alternating tree automata. The semantic characterizations are of independent interest.

An ABox A is tree-shaped if the undirected graph with nodes Ind(A) and edges ¶¶a↪ b♦ ♣ r(a↪ b) 2 A♦ is acyclic and connected and r(a↪ b) 2 A implies that (i) s(a↪ b) ◁2 A for all s 6= r and (ii) s(b↪ a) ◁2 A for all role names s. For treeshaped ABoxes A, we often distinguish an individual used as the root, denoted with ⇢A. A is ditree-shaped if the directed graph with nodes Ind(A) and edges ¶(a↪ b) ♣ r(a↪ b) 2 A♦ is a tree and r(a↪ b) 2 A implies (i) and (ii). The (unique) root of a ditree-shaped ABox A is also denoted with ⇢A.

1. A1↪ ▷ ▷ ▷ ↪Ak are tree-shaped;

An ABox A is a pseudo tree if it is the union of ABoxes A0↪ ▷ ▷ ▷ ↪Ak that satisfy the following conditions:

1. k  ♣Ind(A0)♣;
2. Ai \ A0 = ¶⇢Ai ♦ and Ind(Ai) \ Ind(Aj) = ;, for 1  i < j  k.

We call A0 the core of A and A1↪ ▷ ▷ ▷ ↪ Ak the trees of A. The width of A is ♣Ind(A0)♣, its depth is the depth of the deepest tree of A, and its outdegree is the maximum outdegree of the ABoxes A1↪ ▷ ▷ ▷ ↪Ak. For a pseudo tree ABox A and ` ≥ 0, we write A♣` to denote the restriction of A to the individuals whose minimal distance from a core individual is at most `, and analogously for A♣>`. A pseudo ditree ABox is defined analogously to a pseudo tree ABox, except that A1↪ ▷ ▷ ▷ ↪Ak must be ditree-shaped.

When studying FO-rewritability and containment, we can restrict our attention to pseudo tree ABoxes, and even to pseudo ditree ABoxes when the TBox does not contain inverse roles. The following statement makes this precise for the case of containment. Its proof uses unraveling and compactness.

Proposition 8. Let Qi = (Ti↪⌃↪ qi), i 2 ¶1↪ 2♦, be OMQs from (ELIHF?, CQ). Then Q1 6✓ Q2 iff there is a pseudo tree ⌃-ABox A of outdegree at most ♣T1♣ and width at most ♣q1♣ that is consistent with both T1 and T2 and a tuple a from the core of A such that A ♣= Q1(a) and A 6♣= Q2(a).

If Q1↪Q2 are from (ELHF?↪ CQ), then we can find a pseudo ditree ABox with these properties.

We now establish a first version of the announced characterizations of FO-rewritability. Like Proposition 8, they are based on pseudo tree ABoxes.

Theorem 9. Let Q = (T ↪ ⌃↪ q) be an OMQ from (ELIHF?, conCQ). If the arity of q is at least one, then the following conditions are equivalent:

1. Q is FO-rewritable;
2. there is a k ≥ 0 such that for all pseudo tree ⌃-ABoxes A that are consistent with T and of outdegree at most ♣T ♣ and width at most ♣q♣: if A ♣= Q(a) with a from the core of A, then A♣k ♣= Q(a);

If q is Boolean, this equivalence holds with (2.) replaced by

• 20 . there is a k ≥ 0 such that for all pseudo tree ⌃-ABoxes A that are consistent with T and of outdegree at most ♣T ♣ and of width at most ♣q♣: if A ♣= Q, then A♣>0 ♣= Q or A♣k ♣= Q.

If Q is from (ELHF?↪ conCQ), then the above equivalences hold also when pseudo tree ⌃-ABoxes are replaced with pseudo ditree ⌃-ABoxes.

The proof of Proposition 8 gives a good intuition of why FO-rewritability can be characterized in terms of ABoxes that are pseudo trees. In fact, the proof of "2 ) 1" of Theorem 9 is similar to the proof of Proposition 8. The proof of "1 ) 2" uses locality arguments in the form of Ehrenfeucht-Fra¨ıss´e games. The following examples further illustrate Theorem 9.

Example 10. (1) Non FO-rewritability of the OMQs QA and Q1 from Example 2 is shown by refuting Condition 2 in Theorem 9: let Ak = ¶r(a0↪ a1)↪ ▷ ▷ ▷ ↪ r(ak↪ ak+1)↪ A(ak+1)♦, for all k ≥ 0. Then Ak ♣= Q(a0) but Ak♣k 6♣= Q(a0) for Q 2 ¶QA↪ Q1♦.

(3) The modification 20 of Condition 2 is needed to characterize FO-rewritability of Boolean OMQs: obtain QB from Q2 by replacing q2 with 9xB(x). Then QB is FO-rewritable, but the ABoxes Bk show that Condition 2 does not hold.

(2) Theorem 9 only holds for connected CQs: consider Q2 = (T2↪⌃2↪ q2), where T2 is the empty TBox, ⌃2 = ¶A↪ B♦, and q2 = 9x9y(A(x) ^ B(y)). Q2 is FO-rewritable (q2 itself is a rewriting), but Condition 20 does not hold: for Bk = ¶A(a0)↪ R(a0↪ a1↪ ▷ ▷ ▷ ↪ R(ak↪ ak+1)↪ B(ak+1)♦ we have Bk ♣= Q2 but Bk♣>0 6♣= Q2 and Bk♣k 6♣= Q2.

Theorem 9 does not immediately suggest a decision procedure for FO-rewritability since there is no bound on the depth of the pseudo tree ABoxes A used. The next result establishes such a bound.

Theorem 11. Let T be an ELIHF? TBox. Then Theorem 9 still holds with the following modifications:

1. if q is not Boolean or T is an ELHF? TBox, "there is a k ≥ 0" is replaced with "for k = ♣q♣ + 24(♣T ♣+♣q♣)2 ";
2. if q is Boolean, "there is a k ≥ 0" is replaced with "for k = ♣q♣ + 24(♣T ♣+2♣q♣ )2 ".

The proof of Theorem 11 uses a pumping argument based on derivations of concept names in the pumped ABox by T . Due to the presence of inverse roles, this is not entirely trivial and uses what we call transfer sequences, describing the derivation history at a point of an ABox. Together with the proof of Theorem 9, Theorem 11 gives rise to an algorithm that constructs actual rewritings when they exist.

5 Constructing Automata

We show that Proposition 8 and Theorem 11 give rise to automata-based decision procedures for containment and FOrewritability that establish the upper bounds stated in Theorems 5 and 6. By Theorem 4, it suffices to consider connected queries in the case of FO-rewritability. We now observe that we can further restrict our attention to Boolean queries. We use BCQ (resp. conBCQ) to denote the class of all Boolean CQs (resp. connected Boolean CQs).

Lemma 12. Let L 2 ¶ELIHF?↪ ELHF?♦. Then

1. FO-rewritability in (L↪ conCQ) can be reduced in polytime to FO-rewritability in (L↪ conBCQ);
2. Containment in (L↪ CQ) can be reduced in polytime to containment in (L↪ BCQ).

The decision procedures rely on building automata that accept pseudo tree ABoxes which witness non-containment and non-FO-rewritability as stipulated by Proposition 8 and Theorem 11, respectively. We first have to encode pseudo tree ABoxes in a suitable way.

A tree is a non-empty (and potentially infinite) set T ✓ ⇤ closed under prefixes. We say that T is m-ary if for every x 2 T , the set ¶i ♣ x · i 2 T♦ is of cardinality at most m. For an alphabet Γ, a Γ-labeled tree is a pair (T↪ L) with T a tree and L : T ! Γ a node labeling function. Let Q = (T ↪ ⌃↪ q) be an OMQ from (ELIHF?↪ conBCQ). We encode pseudo tree ABoxes of width at most ♣q♣ and outdegree at most ♣T ♣ by (♣T ♣ · ♣q♣)-ary ⌃" [⌃N-labeled trees, where ⌃" is an alphabet used for labeling root nodes and ⌃N is for non-root nodes.

The alphabet ⌃" consists of all ⌃-ABoxes A such that Ind(A) only contains individual names from a fixed set Indcore of size ♣q♣ and A satisfies all functionality statements in T . The alphabet ⌃N consists of all subsets ⇥ ✓ (NC \ ⌃) ] ¶r↪ r- ♣ r 2 NR \ ⌃♦ ] Indcore that contain exactly one (potentially inverse) role and at most one element of Indcore. A (♣T ♣ · ♣q♣)- ary ⌃"[⌃N-labeled tree is proper if (i) the root node is labeled with a symbol from ⌃", (ii) each child of the root is labeled with a symbol from ⌃N that contains an element of Indcore, (iii) every other non-root node is labeled with a symbol from ⌃N that contains no individual name, and (iv) every non-root node has at most ♣q♣ successors and (v) for every a 2 Indcore, the root node has at most ♣q♣ successors whose label includes a.

A proper ⌃" [ ⌃N-labeled tree (T↪ L) represents a pseudo tree ABox A(T↪L) whose individuals are those in the ABox A that labels the root of T plus all non-root nodes of T , and whose assertions are

A [ ¶A(x) ♣ A 2 L(x)♦ [ ¶r(b↪ x) ♣ ¶b↪ r♦ ✓ L(x)♦ [ ¶r(x↪ b) ♣ ¶b↪ r-♦ ✓ L(x)♦ [ ¶r(x↪ y) ♣ r 2 L(y)↪ y is a child of x↪ L(x) 2 ⌃N♦ [ ¶r(y↪ x) ♣ r- 2 L(y)↪ y is a child of x↪ L(x) 2 ⌃N♦▷

As the automaton model, we use two-way alternating parity automata on finite trees (TWAPAs). As usual, L(A) denotes the tree language accepted by the TWAPA A. Our central observation is the following.

Proposition 13. For every OMQ Q = (T ↪⌃↪ q) from (ELIHF?↪ BCQ), there is a TWAPA

AQ has at most 2p(♣q♣+log(♣T ♣)) states, and at most p(♣q♣+ ♣T ♣) states if T is an ELHF? TBox, p a polynomial.

1. AQ that accepts a (♣T ♣ · ♣q♣)-ary ⌃" [⌃N-labeled tree (T↪L) iff it is proper, A(T↪L) is consistent with T, and A(T↪L) ♣= Q;
2. AT that accepts a (♣T ♣ · ♣q♣)-ary ⌃" [⌃N-labeled tree

We can construct AQ and AT in time polynomial in their size.

• (T↪ L) iff it is proper and A(T↪L) is consistent with T . AT has at most p(♣T ♣) states, p a polynomial.

The construction of the automata in Proposition 13 uses forest decompositions of the CQ q as known for example from [Lutz, 2008]. The difference in automata size between ELIHF? and ELHF? is due to the different number of tree-shaped subqueries that can arise in these decompositions.

To decide Q1 ✓ Q2 for OMQs Qi = (Ti↪ ⌃↪ qi), i 2 ¶1↪ 2♦, from (ELIHF?↪ BCQ), by Proposition 8 it suffices to decide whether L(AQ1 ) \ L(AT2 ) ✓ L(AQ2 ). Since this question can be polynomially reduced to a TWAPA emptiness check and the latter can be executed in time single exponential in the number of states, this yields the upper bounds for containment stated in Theorems 5 and 6.

To decide non-FO-rewritability of an OMQ Q = (T ↪ ⌃↪ q) from (ELIHF?↪ conBCQ), by Theorem 11 we need to decide whether there is a pseudo tree ⌃-ABox A of outdegree at most ♣T ♣ and width at most ♣q♣ that is consistent with T and satisfies (i) A ♣= Q, (ii) A♣>0 6♣= Q, and (iii) A♣k 6♣= Q where k = ♣q♣ + 24(♣T ♣+2♣q♣ )2 . For consistency with T and for (i), we use the automaton AQ from Proposition 13. To achieve (ii) and (iii), we amend the tree alphabet ⌃" [⌃n with additional labels that implement a counter which counts up to k and annotate each node in the tree with its depth (up to k). We then complement AQ (which for TWAPAs can be done in polynomial time), relativize the resulting automaton to all but the first level of the input ABox for (ii) and to the first k levels for (iii), and finally intersect all automata and check emptiness. This yields the upper bounds for FO-rewritability stated in Theorems 5 and 6.

As remarked in the introduction, apart from FO-rewritability of an OMQ (T ↪⌃↪ q) we should also be interested in FOrewritability of ABox inconsistency relative to T and ⌃. We close this section with noting that an upper bound for this problem can be obtained from Point 2 of Proposition 13 since TWAPAs can be complemented in polynomial time. A matching lower bound can be found in [Bienvenu et al., 2013].

Theorem 14. In ELIHF?, FO-rewritability of ABox inconsistency is EXPTIME-complete.

6 Rooted Queries and Lower Bounds

We first consider the case of rooted queries and establish the upper bound in Theorem 7.

Theorem 15. FO-rewritability and containment in (ELIHF?↪ rCQ) are in CONEXPTIME.

Because of space limitations, we confine ourselves to a brief sketch, concentrating on FO-rewritability. By Point 1 of Theorem 11, deciding non-FO-rewritability of an OMQ Q = (T ↪ ⌃↪ q) from (ELIHF?↪ rCQ) comes down to checking the existence of a pseudo tree ⌃-ABox A that is consistent with T and such that A ♣= Q(a) and A♣k 6♣= Q(a) for some tuple of individuals a from the core of A, for some suitable k. Recall that A ♣= Q(a) if and only if there is a homomorphism h from q to the pseudo tree-shaped canonical model of T and A that takes the answer variables to a. Because a is from the core of A and q is rooted, h can map existential variables in q only to individuals fromA♣♣q♣ and to the anonymous elements in the subtrees below them. To decide the existence of A, we can thus guess A♣♣q♣ together with sets of concept assertions about individuals in A♣♣q♣ that can be inferred fromA and T , and from A♣k and T . We can then check whether there is a homomorphism h as described, without access to the full ABoxes A and A♣k. It remains to ensure that the guessed initial part A♣q♣ can be extended to A such that the entailed concept assertions are precisely those that were guessed, by attaching tree-shaped ABoxes to individuals on level ♣q♣. This can be done by a mix of guessing and automata techniques.

We next establish the lower bounds stated in Theorems 5 and 7. For Theorem 5, we only prove a lower bound for Point 1 as the one in Point 2 follows from [Bienvenu et al., 2013].

Theorem 16. Containment and FO-rewritability are

1. CONEXPTIME-hard in (ELI↪ rCQ) and
2. 2EXPTIME-hard in (ELI↪ CQ).

The results for containment apply already when both OMQs share the same TBox.

Point 1 is proved by reduction of the problem of tiling a torus of exponential size, and Point 2 is proved by reduction of the word problem of exponentially space-bounded alternating Turing machines (ATMs). The proofs use queries similar to those introduced in [Lutz, 2008] to establish lower bounds on the complexity of query answering in the expressive OMQ languages (ALCI↪ rCQ) and (ALCI↪ CQ). A major difference to the proofs in [Lutz, 2008] is that we represent torus tilings / ATM computations in the ABox that witnesses noncontainment or non-FO-rewritability, instead of in the 'anonymous part' of the model created by existential quantifiers.

The proof of Point 2 of Theorem 16 can be modified to yield new lower bounds for monadic Datalog containment. Recall that the rule body of a Datalog program is a CQ. Treeshapedness of a CQ q is defined in the same way as for an ABox in Section 4, that is, q viewed as an undirected graph must be a tree without multi-edges.

Theorem 17. For monadic Datalog programs which contain no EDB relations of arity larger than two and no constants, containment

1. in a rooted CQ is CONEXPTIME-hard;
2. in a CQ is 2EXPTIME-hard, even when all rule bodies are tree-shaped.

Point 1 closes an open problem from [Chaudhuri and Vardi, 1994], where a CONEXPTIME upper bound for containment of a monadic Datalog program in a rooted UCQ was proved and the lower bound was left open. Point 2 further improves a lower bound from [Benedikt et al., 2012] which also does not rely on EDB relations of arity larger than two, but requires that rule bodies are not tree-shaped or constants are present (which, in this case, correspond to nominals in the DL world).

7 Conclusion

A natural next step for future work is to use the techniques developed here for devising practically efficient algorithms that construct actual rewritings, which was very successful in the AQ case [Hansen et al., 2015].

An interesting open theoretical question is the complexity of FO-rewritability and containment for the OMQ languages considered in this paper in the special case when the ABox signature contains all concept and role names.

Acknowledgements. Bienvenu was supported by ANR project PAGODA (12-JS02-007-01), Hansen and Lutz by ERC grant 647289, Wolter by EPSRC UK grant EP/M012646/1.