Query Answering in the Horn Fragments of the Description Logics SHOIQ and SROIQ

1 Introduction

Description Logics (DLs), a family of languages for Knowledge Representation and Reasoning, are applied in many fields and are particularly popular as ontology languages for conceptually describing application domains. In fact, the Web Ontology Languages (OWL) proposed as a standard for writing ontologies on the Web are based on expressive DLs: OWL-DL (a.k.a. OWL 1) is based on the DL SHOIQ, while the more recent OWL 2 standardis based on SROIQ [OWL Working Group, 2009]. Unfortunately, the expressiveness of these DLs comes at the cost of high complexity of reasoning: most of the traditional DL reasoning tasks, like deciding knowledge base satisfiability or concept subsumption, are NExpTime-complete for SHOIQ [Tobies, 2000] and 2NExpTime complete for SROIQ [Kazakov, 2008]. If data complexity is considered (that is, if the complexity is measured in terms of the size of the assertional component while disregarding the size of the terminological component), then both logics are co-NP-hard. As more and more application areas require higher scalability, the study of fragments of expressive DLs with better computational properties has become an important area of research.

∗ This work was partially supported by (†) the Austrian Science Fund (FWF) grant P20840, the Vienna Science and Technology Fund (WWTF) project ICT08-032, and (‡) the project ExpresST funded by the Deutsche Forschungsgemeinschaft (DFG).

Horn fragments of DLs, which are obtained by restricting the syntax of a DL in such a way that disjunction is not expressible, were first considered in [Hustadt et al., 2005] as expressive fragments with tractable data complexity (see also [Kr¨otzsch et al., 2007]). It was later identified that they can also exhibit lower combined complexity when it comes to query answering. Indeed, answering conjunctive queries (CQs), a kind of database-inspired queries that have become the standard for querying DLs, is in ExpTime for the Horn fragment of the prominent SHIQ [Eiter et al., 2008], while it is already 2ExpTime-hard for quite restricted (non Horn) fragments of SHIQ, like ALCI [Lutz, 2008] and SH [Eiter et al., 2009]. It remained open whether this improvement in the combined complexity of query answering extends to more expressive logics, and in particular, to the Horn fragments of the DLs SHOIQ and SROIQ that underlie the OWL standards. A positive answer is given in this paper.

The distinguishing feature of SHOIQ and SROIQ is that they support nominals O, which allow to restrict the cardinality of a concept, inverses I, which allow to navigate roles in both directions, and number restrictions Q, which allow to restrict the number of pairs of objects that may participate in a role. All of these features have been incorporated to satisfy practical modeling requirements posed by knowledge engineers. The interaction of these three constructors constitutes a severe obstacle to establishing the forest model property that is key to the design of algorithms. More often than not, this also causes an increased complexity of reasoning. Some problems that are well understood for most DLs remain open for SHOIQ and SROIQ, most notably the decidability of query answering. It is only known that the problem is decidable (although no complexity bounds are known) for ALCHOIQb [Rudolph and Glimm, 2010], and already undecidable for ALCOIFreg [Ortiz et al., 2010a].

The Horn fragments of SHOIQ and SROIQ remained unexplored until [Ortiz et al., 2010b], where it was established that every satisfiable knowledge base in these languages has a forest-like model that can be represented in a relatively compact way. This and the lack of disjunction allowed the authors to show that traditional reasoning tasks are ExpTime-complete and 2ExpTime-complete in combined complexity for Horn-SHOIQ and Horn-SROIQ, respectively, and are PTime-complete in data complexity.

In this paper we develop an algorithm for answering conjunctive 2-way regular path queries (2CRPQs), a non-trivial generalization of plain CQs that allow for expressing complex navigation in models by means of regular expressions. They also generalize the (2-way) regular path queries used for querying web data and other forms of graph databases, and they constitute a large fragment of the SPARQL 1.1 query language for ontologies that is currently under standardization. 1 We show that a satisfiable KB in the Horn fragments of SHOIQ and SROIQ has a universal model that can be used to answer all queries, and use a combination of query partitioning and tree automata techniques for query answering over a model representation similar to the one in [Ortiz et al., 2010b]. Thereby we show that query answering is not more expensive than standard reasoning: ExpTime-complete for Horn-SHOIQ and 2ExpTime-complete for the more expressive Horn-SROIQ in combined complexity, but PTimecomplete in data complexity for both. Notably, these are the first completeness results for query answering in DLs with inverses, nominals, and counting.

2 Preliminaries

We start by introducing the DLs and the query language considered in this paper.

The Horn Fragments of SHOIQ and SROIQ

We recall the syntax of Horn-SROIQ and Horn-SHOIQ, as defined in [Ortiz et al., 2010b]. 2

We assume countably infinite sets NC ⊃ {⊤, ⊥}, NR and NI of concept names, role names, and individuals respectively. If r ∈ NR, then r and r - are roles, and their respective inverses are inv(r)=r - and inv(r - )=r. We let NR =NR∪{r - | r ∈ NR}. We assume a strict partial order ≺ on the roles such that t ≺ r iff inv(t) ≺ r. Expressions of the forms (i) to (xii) in Table 1 are called axioms; in particular, axioms of the forms (i) to (v) in Table 1 are role inclusion axioms (RIAs). The non-simple roles in a given set R of RIAs are inductively defined: (A) r is non-simple if there is a RIA r1 ◦ . . . ◦ rn ⊑ r in R with n > 1, (B) r is non-simple if R contains a RIA of the form s ⊑ r with s non-simple, and (C) r - is non-simple iff r is non-simple. Then a role occurring in R is simple if it is not non-simple.

A terminology T is a set of axioms. The simple roles in T are the simple roles in {α | α is a RIA in T }. A Horn-SROIQ knowledge base (KB) is a tuple K=(T,A), where T is a terminology and the ABox A is a non-empty set of assertions of the forms (xiii) and (xiv). The DL Horn-SHOIQ results from restricting Horn-SROIQ as follows: (A) allowing only RIAs of the forms (i), (ii') and (v); (B) disallowing disjointness axioms (vi); and (C) disallowing concepts of type ∃t.Self. Further restricting Horn-SHOIQ by allowing only expressions of types (i), (ii'), (vi)-(ix), (xi), (xiii) and (xiv) (marked in boldface in the table) yields the DL that we call Horn-ALCHOIQ Disj Self . Note that in such a KB all roles are simple. The semantics of KBs is defined in the usual, modeltheoretic way via interpretations I = (Δ I , · I ).

1 http://www.w3.org/TR/sparql11-query/

2 Due to space limitations, we focus on the normal form used in [Ortiz et al., 2010b]. As usual, every KB can be polynomially rewritten into a normal one that is equivalent modulo the fresh concept names introduced by the translation, see [Kr¨otzsch et al., 2007].

2-Way Conjunctive Regular Path Queries

The queries we consider use nondeterministic finite state automata (NFAs). Recall that an NFA is a tuple α = (Σ, S, δ, s0, F), where Σ is the alphabet, S is the set of states, δ ⊆ S × Σ × S is the transition relation, s0 ∈ S is the initial state, and F ⊆ S is the set of final states. We use Σ α , S α , δ α , s α 0 and F α to denote the components of α.

Now we define 2-way conjunctive regular path queries (2CRPQ, or simply queries), whose atoms use nondeterministic finite state automata (NFAs) to define regular languages over the alphabet NR. Let V be a countably infinite set of variables. Then a 2CRPQ q is a set of atoms of the form α(x, y), where x, y ∈ V and α is an NFA with Σ α = NR. We use V(q) to denote the set of variables occurring in q.

Let I be an interpretation and α an NFA with Σ α = NR. An α-path (from d0 to dn) in I is a sequence d0, . . . , dn of elements of Δ I such that for each 0 ≤ i < n there is a state si ∈ S α and a role ri ∈ NR such that (di, di+1) ∈ r I i , s0 = s α 0 , sn-1 ∈ F α and (si, ri, si+1) ∈ δ α . We call d ′ an α-successor of d in I if there is an α-path from d to d ′ .

A match for a query q in an interpretation I is a mapping π : V(q) → Δ I such that π(y) is an α-successor of π(x) for each α(x, y) ∈ q. We write I |= q if there is a match for q in I. Given a knowledge base K, we write K |= q if I |= q for every model I of K.

Note that queries are Boolean, i.e. , they do not allow for answer variables. They can simulate the standard (Boolean) conjunctive queries, that use concept and role names instead of NFAs in the atoms, and allow for individuals in the place of variables. 3 As usual, the decision problem associated to answering queries with answer variables can be reduced to the entailment of a Boolean query.

Simplifying Horn-SROIQ and Horn-SHOIQ KBs

Query answering in Horn-SROIQ and Horn-SHOIQ KBs can be reduced to query answering in the simpler Horn-ALCHOIQ Disj Self KBs. The following proposition is an easy consequence of the knowledge base transformation in [Kazakov, 2008]:

3 Individuals and concepts can be eliminated from the query in polynomial time using fresh query atoms and axioms in the KB.

Proposition 1. For every Horn-SROIQ terminology T and query q there exists a Horn-ALCHOIQ Disj Self terminology T ′ and a query q ′ such that:

1. (T,A) |= q iff (T ′ ,A) |= q ′ , for any ABox A;
2. T ′ and q ′ can be effectively constructed from T and q in single exponential time. If T is in Horn-SHOIQ, then T ′ and q ′ can be constructed from T and q in polynomial time (assuming that numbers are encoded unary).

3 Query Answering

Assume in what follows a Horn-ALCHOIQ Disj Self KB K = (T,A) and a query q. Our goal is to provide an algorithm and characterize the combined and data complexity of deciding K |= q. By Proposition 1, such a procedure can be used for Horn-SHOIQ and Horn-SROIQ as well. Without loss of generality we assume that K is satisfiable. 4

3.1 Universal Model Property

Our method builds on the following crucial property: the KB K has a universal model, i.e. there is a model I of K such that K |= q ′ iff I |= q ′ , for any query q ′ . The universality of I is due to the guaranteed existence of a homomorphic embedding ϕ of I into any other model I ′ of K. Intuitively, if I has a match π for q, then the composition ϕ◦π is a match for q in I ′ .

By employing the results in [Ortiz et al., 2010b] we can further show that K has a universal model I with a quite regular structure, which allows to finitely represent it. To this end, we introduce a representation of (possibly infinite) models of K via model descriptions. In the next section, we will see that model descriptions give rise to an optimal algorithm for query answering.

Intuitively, a model description contains a graph part and a successor function. The graph part comprises a finite number of domain elements G that may be arbitrarily interrelated by roles, while the successor function tells us how this finite structure can be expanded into a potentially infinite forestshaped structure.

Definition 1 (Model description). A concept type τ (for T) is any set of concepts occurring in the axioms of T and that does not contain ⊥ and does not contain a pair of concepts of the form {⩽1 t.B, ⩾m t.B} with m > 1. A role-type ρ (for T ) is a set of roles occurring in T. The set of all concept types of T is denoted by TT , and the set of all role types by RT .

A model description for K is a tuple M = (G, θ, f , succs) where:

• (a) G is a set of objects called graph nodes;
• (b) θ is a function that maps each d ∈ G to a concept type θ(d) ∈ TT and each pair (d, d ′ ) ∈ G×G to a role type θ(d, d ′ ) ∈ RT in such a way that θ(d, d ′ ) = {inv(r) | r ∈ θ(d, d ′ )} for each d, d ′ ∈ G;
• (c) f is a function f : NI(A) →G, where NI(A) denotes the set of individuals occurring in A;

4 If K is unsatisfiable, then K |= q for every q. Satisfiability of K within the necessary time bounds can be checked using the algorithm in [Ortiz et al., 2010b].

• (d) succs : G∪ (TT ×RT ×TT ) → 2 RT ×(TT∪G) is a function such that succs(d) ∈ 2 RT ×TT for each d ∈ G.

We use receive(M) to denote the nodes in G that occur in the range of succs.

Intuitively, every model description represents some interpretation IM. Its domain contains the graph nodes G, and each graph node is the root of a possibly infinite tree-shaped structure in which some nodes may be related to graph nodes (the latter 'receiving' nodes are represented by receive(M)). Each d ∈ G is associated to a concept type θ(d) that contains precisely the concepts it satisfies, and each pair d, d ′ to a role type θ(d, d ′ ) containing precisely the roles that relate them. The function f tells which individual names are interpreted as which graph nodes, while succs describes how tree-shaped structures can be generated starting from graph nodes. To understand this, recall that succs is defined for elements in d ∈ G and triplets (τ1, ρ, τ2) ∈ TT ×RT ×TT . This means that succs gives a specific successor configuration for the graph nodes, while for the remaining nodes the children are given based on a concepts-roles-concepts pattern. In particular, the children of a tree node e are determined based on the type of e, the type of its parent and the roles that connect them. The children are given as a set of tuples (ρ, τ) ∈ RT ×TT and (ρ, d) ∈ RT ×G. Intuitively, (ρ, τ) stands for a ρ-child satisfying τ, while (ρ, d) means a ρ-link to the graph node d. We build IM formally as follows:

Definition 2. Let M = (G, θ, f , succs) be a model description for K. We say that M describes the interpretation IM defined as follows:

The domain Δ IM is the smallest set of words of the form e = dρ1τ2 . . . ρn-1τn ∈ G× (TT ×RT ) ∗ such that:

• G ⊆ Δ IM ,
• if d ∈ G and (ρ ′ , τ ′ ) ∈ succs(d), then dρ ′ τ ′ ∈ Δ I ,
• if eρτ ∈ Δ IM and (ρ ′ , τ ′ ) ∈ succs(last(e), ρ, τ), then eρτρ ′ τ ′ ∈ Δ I ,

where last(e) = θ(e) if e ∈ G, and last(eρτ) = τ otherwise.

Nodes in Δ IM \ G are called tree nodes, and we say that a node eρτ ∈ Δ IM is a child of the node e.

The interpretation function · IM is defined next:

• for each a ∈ NI(A), a IM = f (a);
• for each A ∈ NC, A IM = {e | A ∈ last(e)};
• for each r ∈ NR, r IM is the set of pairs that contains:
• (d, d ′ ) if d, d ′ ∈ G and r ∈ θ(d, d ′ )
• (e, eρτ) whenever e, eρτ ∈ Δ I and r ∈ ρ,
• (eρτ, e) whenever e, eρτ ∈ Δ I and inv(r) ∈ ρ,
• (e, e) whenever ∃r.Self ∈ last(e),
• (eρτ, d) if d ∈ G and (ρ ′ , d)∈succs(last(e), ρ, τ) for a ρ ′ with r ∈ ρ ′ ,
• (d, eρτ) if d ∈ G and (ρ ′ , d)∈succs(last(e), ρ, τ) for a ρ ′ with inv(r) ∈ ρ.

Importantly, there is a model description that represents the desired universal model, and it can be constructed in time that is single exponential in the size ||K|| and only polynomial in ||A|| (for fixed T):

Theorem 2. For the KB K there is a model description M = (G, θ, f, succs) such that:

1. IM |= K;
2. K |= q ′ iff IM |= q ′ , for every query q ′ ;
3. M can be build in time single exponential in ||K|| (and is thus of size at most exponential in ||K||). If T is fixed, thenMcan be obtained in polynomial time in ||A||.
4. If T is fixed, then |receive(M)| is bounded by a constant.

Sketch. In [Ortiz et al., 2010b] it was shown that a model of a given Horn-ALCHOIQ Disj Self KB K can be obtained from the minimal model I of a Datalog program obtained from K. It can be shown in a rather straightforward way that the resulting model is universal. The claim follows from those results, since the I is very closely related to the model descriptions used in this paper. To make this paper as self-contained as possible, we sketch here a direct proof of existence and universality of the mentioned model representation.

Let M be the set of all models of K. We then define M as follows (using τ I as a shortcut for ⋂ A∈τ A I ):

(a) To define G, we first let ˆT denote the set of all τ ∈ TT for which (i) every I ∈ M satisfies |τ I | = 1 and (ii) there is no τ ′ ⊃ τ with the same property (i.e. τ is inclusion-maximal).

We define the equivalence relation ≈ on NI(A) by letting a ≈ b iff a I = b I for all I ∈ M. Now we let G contain all pairs (c, τ ′ ) for which either (i) c is a ≈-equivalence class and, for any b ∈ c, τ ′ = ⋂ I∈M{A | b I ∈ A I } (we call these the named graph nodes) or (ii) c = ∅, τ ′ ∈ ˆT and there is no b ∈ NI(A) such that b I ∈ τ I for all I ∈ M (we call these the anonymous graph nodes).

• (b) For each (c, τ ′ ) ∈ G, we define θ by letting θ((c, τ ′ )) := τ ′ and letting θ((c1, τ1), (c2, τ2)) contain all roles r for which every I ∈ M satisfies that (e1, e2) ∈ r I where ei ∈ Δ I is the domain element with ei ∈ τ I i and ei = d I for all d ∈ ci.
• (c) f is such that every b is mapped to the unique ([b]≈, τ ′ ).

(d) We define succs as follows: For d ∈ G, we let succs(d) contain all (ρ, τ ′ ) where (i) for every I ∈ M and e ∈ τ I there exists some e ′ ∈ τ ′I with (e, e ′ ) ∈ r I for all r ∈ ρ and (ρ, τ ′ ) is inclusion-maximal w.r.t. that property; (ii) there is no d ′ ∈ G with ρ ⊆ θ(d, d ′ ) and τ ′ ⊆ θ(d ′ ); (iii) {∃r.Self | r ∈ ρ}∪τ ′ ⊈ τ. For τ, τ ′ ∈ TT and ρ ∈ RT we let succs(τ, ρ, τ ′ ) contain

• all (ρ ′ , τ ′′ ) where (i) for every I ∈ M and e ∈ τ ′I there exists some e ′ ∈ τ ′′I with (e, e ′ ) ∈ r I for all r ∈ ρ ′ and (ρ ′ , τ ′′ ) is inclusion-maximal w.r.t. that property; (ii) it is not the case that both ρ ′ ⊆ {inv(r) | r ∈ ρ} and τ ′′ ⊆ τ; (iii) there is no (c, τ ′′′ ) ∈ G with τ ′′ ⊆ τ ′′′ ; (iv) {∃r.Self | r ∈ ρ} ∪ τ ′ ⊈ τ;
• all (ρ ′ , (c, τ ′′ )) with (c, τ ′′ ) ∈ G where for every I ∈ M, e ∈ τ ′I , e ′ ∈ τ ′′I and r ∈ ρ ′ holds (e, e ′ ) ∈ r I and τ ′′ ∈ ˆT.

By inspecting each type of axiom that may occur in K (see Table 1), one can show that the interpretation IM defined in Definition 2 is a model of K as claimed in 1.

To prove that IM is universal (Claim 2), one can show that there is a homomorphism ϕ from IM to every model I of K, which can be constructed inductively on the length of the elements of Δ IM as follows:

• We start from G. For each named graph node ([a]≈, τ ′ ), we let ϕ(([a]≈, τ ′ )) := a I . For each anonymous graph node (∅, τ ′ ), we let ϕ((∅, τ ′ )) = w for the unique w with {w} = τ I .
• Let each eρτ ∈ Δ IM for which ϕ(e) has been defined, we set ϕ(eρτ) = w for a w with w ∈ ⋂ A∈τ A I and (ϕ(e), w) ∈ ⋂ r∈ρ r I ; such a w exists in every model of K by the construction of M.

The existence of the homomorphism ϕ into every model I ensures that whenever there is a match π for a 2CRPQ q in IM, then π ◦ ϕ is a match for q in I. This shows that IM is universal, i.e. K |= q iff IM |= q.

To see that M satisfies Claim 4, note that the number of distinct (c, τ) ∈ G satisfying τ ′′ ∈ ˆT for every I ∈ M (let us call these particular elements G s ) is exponentially bounded by T, since there can be only one such element for each τ. Yet, by definition only elements of G s occur in the range of succs and hence in receive(M).

To prove Claim 3 note that the exponential bound on the size of M follows from the fact that there are at most exponentially many different types. Likewise, this gives rise to an exponential time algorithm since all (overall single exponentially many) decisions to define M requiring inspections of the set M of all models can be cast into Horn-ALCHOIQ Disj Self standard reasoning tasks which are known to be ExpTimecomplete.

For the polynomial size bound ofMw.r.t. |A| note that we have by definition |G \ receive(M)| ≤ |NI(A)|, consequently the sizes of the receive(M)-related parts of succs and θ are at most linearly and quadratically bounded by |NI(A)|, respectively. Further, for a fixed T, receive(M) and the respective parts of succs and θ are constant, hence |M| is of polynomial size w.r.t. |A| as claimed. The polynomial bound on the time needed to establish M is a consequence of the known timepolynomial data complexity of Horn-ALCHOIQ Disj Self as the conditions for the definition of G s and the respective parts of succs and θ can be obtained by a polynomial number of Horn-ALCHOIQ Disj Self satisfiability checks on K. □

3.2 Algorithm and Complexity

By Theorem 2, deciding K |= q is equivalent to checking IM |= q, where M is a model description for a universal model of K. We now assume such an M = (G, θ, f , succs), and provide a method to check IM |= q.

First we define the tree-shaped parts of IM.

Definition 3. For each d ∈ G the d-tree of IM, denoted IM,d, is obtained from IM in two steps by (1) restricting IM to the domain Δ IM,d that contains (a) each e ∈ Δ IM of the form dρτ . . . ρ ′ τ ′ , and (b) each d ′ ∈ G such that (e, d ′ ) ∈ r IM for some e = dρτ . . . ρ ′ τ ′ as above and some r ∈ NR; and (2) setting {r | (d, d ′ ) ∈ r I } = ∅ for all d, d ′ ∈ Δ IM,d ∩G.

To find a match π for q in IM, we first consider a function δ that 'guesses' for each variable x of q whether π(x) is a graph node d = δ(x), or a tree node inside a d-tree (indicated by δ(x) = d↓). Based on δ, we decompose q into several queries, additionally guessing for each α(x, y) of q which of three kinds of paths exists between π(x) and π(y): a path of type p that starts and ends in a graph node, a path t that is entirely inside a d-tree and does not pass any other graph node, or a path that starts or ends inside a tree, but passes at least one other graph node on the way.

Definition 4 (Query Partition). Let S = ⋃ α(x,y)∈q S α , and let G ′ = G ∪ {d↓ | d ∈ G}. A partition Π of q is a pair (δ, Γ) where δ : Vars(q) → G ′ and Γ : q → (G × S) 2 ∪ {p, t} such that one of the following holds for each α(x, y) ∈ q:

• δ(x), δ(y) ∈ G and Γ(α(x, y)) = p, or
• there is some d ∈ G such that δ(x), δ(y) ∈ {d, d↓}, and Γ(α(x, y)) = t,
• {δ(x), δ(y)} ⊈ G and Γ(α(x, y)) = 〈(d1, s1), (d2, s2)〉 ∈ (G × S) 2 with s1, s2 ∈ Qα, and δ(y) ∈ {d2, d2↓}.

For the parts of the paths that start or end inside the trees, we build queries that are evaluated over the d-trees. We consider atoms α(t, t ′ ) with t, t ′ ∈ G ∪ V. A match π for such a query q in a part of IM is defined analogously as in Section 2, but it must additionally map each d ∈ G occurring in q to itself. For an NFA α, s ∈ S α and S ⊆ S α , we define αs,S = (Σ α , S α , δ α , s, S ), that is, αs,S is obtained by making s the initial state and S the set of final states of α.

Definition 5. For each d ∈ G, the d-query of Π is the set tq(Π, d) containing

• each α( f (x), f (y)) such that α(x, y) ∈ q, δ(x), δ(y) ∈ {d, d↓}, and Γ(α(x, y)) = t;
• each αs α 0 ,{s1}( f (x), d1) such that α(x, y) ∈ q, δ(x) ∈ {d, d↓}, and Γ(α(x, y)) = 〈(s1, d1), (s2, d2)〉; and
• each αs2,F α(d2, f (y)) such that α(x, y) ∈ q, δ(y) ∈ {d2, d2↓}, and Γ(α(x, y)) = 〈(s1, d1), (s2, d2)〉,

where, for a variable x, f (x) = δ(x) if δ(x) ∈ G, and f (x) = x otherwise.

For the remaining parts of the paths, we rely on a relation paths(M) that contains all the relevant paths between graph nodes. We will show later how this relation can be effectively computed.

Definition 6. We define paths(M) = {〈(s, d)(s ′ , d ′ )〉 ∈ (G × S) 2 | d ′ is an αs,{s ′ }-successor of d in IM }. Let Π = (δ, Γ) be a partition of q. Then we say that paths(M) satisfies the graph paths of Π if the following hold:

• for each α(x, y) ∈ q such that {δ(x), δ(y)} ⊆ G and Γ(α(x, y)) = p, there is some s f ∈ F α such that 〈(δ(x), s α 0 ), (δ(y), s f )〉 ∈ paths(M), and
• for each α(x, y) ∈ q such that Γ(α(x, y)) = 〈(d, s)(d ′ s ′ )〉, 〈(d, s)(d ′ s ′ )〉 ∈ paths(M).

We write M |= Π if paths(M) satisfies the graph paths of Π, and IM,d |= tq(Π, d) for every d ∈ G.

Every match for q in IM can be used to define a partition such that M |= Π. Conversely, if M |= Π then there is a match for the full q in IM. Hence we have:

Theorem 3. IM |= q iff there exists query partition Π of q such that M |= Π.

Consequently, IM |= q (and K |= q), reduces to finding a query partition Π such that M |= Π. We first note that the number of distinct partitions Π of q is O ( |G| |Vars(q)| · (|G| · |S|) 2|q| ) . Keeping in mind Theorem 2, the number of distinct partitions Π to be traversed is exponential in ||K|| + ||q||, but polynomial in ||A|| if T and q are fixed.

It remains to see how to decide M |= Π. To this aim, we first show how IM,d |= tq(Π, d) can be checked for a given partition Π and a d ∈ G. We employ automata over infinite trees, which are a generalization of finite state automata over finite words [Vardi, 1998]. Recall that an infinite k-ary tree over an alphabet Σ is a pair (T,L), where (a) T is the set of all finite words over {1, . . . , k}; (b) L : T → Σ is the labeling function that assigns to each node in T a symbol from Σ. Each tree automaton A is defined for some alphabet Σ and accepts some set L(A) of infinite trees over Σ. The basic reasoning problem is to decide given an automaton A whether A accepts at least one tree, i.e. that L(A) nequal ∅. Various operations on automata can be performed, e.g. for a pair of automata A1, A2, one can build the intersection automaton A1 ∩ A2 such that L(A1 ∩ A2) = L(A1) ∩ L(A2).

Let q ′ = tq(Π, d). It is not too difficult to build a tree automaton A ∗ such that (a) IM,d |= q ′ iff L(A ∗ ) nequal ∅, i.e. to reduce our problem to testing nonemptiness of the language of a tree automaton, (b) L(A ∗ ) nequal ∅ can be checked in time exponential in ||K||+||q||, and in polynomial time in ||A|| if T and q are fixed. Naturally, such a reduction involves an encoding of (tree-shaped) interpretations as labeled trees. The automaton A ∗ is defined as the intersection automaton A ∗ = AM,d ∩ Aq ′ , where AM,d accepts exactly one labeled tree that encodes the interpretation IM,d, and Aq ′ accepts labeled trees that encode interpretations with a match for q ′ . We next describe the languages L(AM,d) and L(Aq ′ ), and discuss the relevant properties of AM,d and Aq ′ , but omit their explicit construction.

The language L(AM,d) consists of exactly one labeled tree (T,L) which represents IM,d. The alphabet is Σ M =Σ M 1 ∪ Σ M 2 ∪{nil}, where Σ M 1 =RT ×TT and Σ M 2 =RT ×receive(M). Intuitively, a node w ∈ T labeled with (ρ, τ) ∈ Σ M 1 corresponds to a tree node ew in IM,d with type τ and which is connected to its parent via the roles in ρ. On the other hand, a node w·c ∈ T labeled with (ρ, d) ∈ Σ M 2 reflects the roles connecting the tree node ew in IM,d to the graph node d. Technically, all nodes of T must have the same number of children, and thus we may need to use the nil label to nodes that do not correspond to elements in IM,d. AM,d can be built as a deterministic 1-way tree automaton with state set Q = TT ×RT ×TT ∪ {d} whose transition function δ is a notational reformulation of succs.

The language L(Aq ′ ) consists of trees over Σ M that encode tree-shaped interpretations with a match for q ′ . To this end, let X be the set of variables in q ′ . Then the automaton Aq ′ can be built in two stages. First, we can build automaton A ′ that accepts trees (T,L) over an extended alphabet Σ ′ = 2 X × Σ M with the following properties: (a) for each x ∈ X there is exactly one node w ∈ T with L(w) = (V, N) and x ∈ V, i.e. each variable x ∈ X occurs in exactly one node of (T,L) and thus (T,L) encodes an interpretation together a variable assignment π; (b) the variable assignment π witness a match for q ′ in the encoded interpretation. By exploiting the bound (4) in Theorem 2, we can implement A ′ as an alternating 2-way automaton whose state set is linear in ||K|| + ||q||, but which is constant if T and q are fixed. The automaton Aq ′ is then obtained from A ′ by transforming A ′ into a nondeterministic 1-way automaton [Vardi, 1998] and projecting away the first component in the labels of nodes, i.e. L(Aq ′ ) is the set of trees (T,L) over Σ M which can be endowed with a variable assignment such that resulting tree is accepted by A ′ .

Since the size of q ′ = tq(Π, d) is polynomial in q, the number of states in the automata AM,d, Aq ′ and A ∗ is exponential in ||K|| + ||q||, however it is bounded by a constant if T and q are fixed. Using well-known algorithms we obtain that testing non-emptiness of A ∗ is feasible in time exponential in ||K|| + ||q||, and polynomial in ||A|| if T and q are fixed.

To obtain an algorithm for M |= Π, it is only left to show how to decide whether paths(M) satisfies the graph paths of a given Π. We start by providing an effective construction of paths(M), which can be obtained as the smallest set of pairs that satisfies the following:

• (a) For each d, d ′ ∈G, α(x, y) ∈q, s, s ′ ∈S α , and r ∈NR, if r ∈ θ(d, d ′ ) and (s, r, s ′ ) ∈ δ α then 〈(d, s), (d ′ , s ′ )〉 ∈ paths(M).
• (b) For each d, d ′ ∈ G, α(x, y) ∈ q, and s, s ′ ∈ S α , if IM,d |= αs,{s ′ }(d, d ′ ), then 〈(d, s), (d ′ , s ′ )〉 ∈ paths(M).
• (c) For d, d ′ , d ′′ ∈G, α(x, y) ∈q and s, s ′ , s ′′ ∈S α , if 〈(s, d)(s ′ , d ′ )〉 ∈paths(M) and 〈(s ′ , d ′ )(s ′′ , d ′′ )〉 ∈ paths(M), then 〈(s, d)(s ′′ , d ′′ )〉 ∈ paths(M).

There are at most (|G| · |S|) 2 cases for which we have to test the conditions (a) and (b). Each test of the first kind can be done with a simple inspection of M and the NFAs in q, and for each test of the second type we can use the same automatabased decision procedure that we use for the d-queries above. Hence each test can be done in time that is exponential in ||K|| + ||q||, and in polynomial time in ||A|| if T and q are fixed. Finally, we close the table under condition (c) by a simple iterative procedure that reaches a fixed-point after at most (|G| · |S|) |q| steps. Hence paths(M) can be effectively constructed in time that is exponential in ||K|| + ||q||, and in polynomial time in ||A|| if T and q are fixed.

Simple look-ups on this table allow us to decide whether paths(M) satisfies the graph paths of Π for any given Π. Hence, putting the above pieces together, we get:

Lemma 4. Entailment of 2CRPQs in Horn-ALCHOIQ Disj Self is in ExpTime w.r.t. combined complexity and in PTime w.r.t. data complexity.

We can now show the main complexity result of this paper:

Theorem 5. Entailment of 2CRPQs in Horn-SHOIQ is ExpTime-complete, while the problem in Horn-SROIQ is 2ExpTime-complete with respect to combined complexity. The data complexity of both problems is PTime-complete.

Proof. (Sketch) Let K = (T,A) be a Horn-SHOIQ (resp. Horn-SROIQ) KB and q a query. Then the upper bounds follow from Lemma 4 and Proposition 1, which states that we can obtain a Horn-ALCHOIQ Disj Self KB K ′ = (T ′ ,A) and a query q ′ such that: (a) K |= q iffK ′ |= q ′ ; (b) ||K ′ || + ||q ′ || is polynomial (resp., exponential) in ||K|| + ||q||; (c) if ||T|| + ||q|| is fixed, then ||T ′ || + ||q ′ || is fixed.

The lower bounds follow from the complexity of standard reasoning: the ExpTime and the PTime lower bounds can be found in [Hustadt et al., 2005], while the 2ExpTime lower bound follows from [Ortiz et al., 2010b]. □

4 Discussion and Conclusion

Our results show that answering complex queries like 2CRPQs in Horn-SHOIQ and Horn-SROIQ is not just decidable but in fact even not any harder than standard reasoning, both in combined and data complexity. That CQ entailment checking is significantly easier in the Horn fragments than in the full DLs is arguably due to the existence of a universal model which can be conveniently represented and harnessed for efficient algorithms. We believe that the techniques to establish the result and the insights thus obtained will pave the way toward more efficient querying algorithms for the Horn restriction of OWL and might prove useful to tackle the problem of CQ entailment for full SROIQ and SHOIQ.