Finite Model Reasoning in Horn-SHIQ Yazmı́n Ibañez-Garcı́a1 , Carsten Lutz2 , and Thomas Schneider2 1 KRDB Research Centre, Free Univ. of Bozen-Bolzano, Italy,{ibanezgarcia@inf.unibz.it} 2 Univ. Bremen, Germany, {clu, tschneider}@informatik.uni-bremen.de Abstract. Finite model reasoning in expressive DLs such as ALCQI and SHIQ requires non-trivial algorithmic approaches that are substantially differerent from algorithms used for reasoning about unrestricted models. In contrast, finite model reasoning in the inexpressive fragment DL-Lite F of ALCQI and SHIQ is algorithmically rather simple: using a TBox completion procedure that reverses certain terminological cycles, one can reduce finite subsumption to unrestricted subsumption. In this paper, we show that this useful technique extends all the way to the popular and much more expressive Horn-SHIQ fragment of SHIQ. 1 Introduction Description logics (DLs) that include inverse roles and some form of counting such as functionality restrictions lack the finite model property (FMP) and, consequently, reasoning w.r.t. the class of finite models (finite model reasoning) does not coincide with reasoning w.r.t. the class of all models (unrestricted reasoning). On the one hand, this distinction is becoming increasingly important since DLs are nowadays regularly used in database applications, where models are generally assumed to be finite. On the other hand, finite model reasoning is rarely used in practice, mainly because for many popular DLs that lack the FMP, no algorithmic approaches to finite model reasoning are known that lend themselves towards efficient implementation. Typical examples include the expressive DLs ALCQI and SHIQ, which are both a fragment of the OWL2 DL ontology language. While finite model reasoning in ALCQI and SHIQ are known to have the same complexity as unrestricted reasoning, namely E XP T IME-complete [9], the algorithmic approaches to the two cases are rather different. For unrestricted reasoning, there is a wide range of applicable algorithms such as tableau and resolution calculi, which often perform rather well in practical implementations. For finite model reasoning, all known approaches rely on the construction of some system of inequalities [3,9], and then solve this system over the integers; the crux is that the system of inequalities is of exponential size in the best case, and consequently it is far from obvious how to come up with efficient implementations. Note that the same is true for the two-variable fragment of first-order logic with counting quantifiers (C2), into which DLs such as ALCQI and SHIQ can be embedded [12,13], that is, all known approaches to finite model reasoning in C2 rely on solving (at least) exponentially large systems of inequalities. Interestingly, the situation is quite different on the other end of the expressive power spectrum. DL-Lite F is a very inexpressive DL that is used in database applications, but lacks the FMP because it still includes inverse roles and functionality restrictions. Building on a technique that was developed in a database context by Cosmadakis, Kanellakis, and Vardi to decide the implication of inclusion dependencies and functional dependencies in the finite [4], Rosati has shown that finite model reasoning in DL-Lite F can be reduced (in polynomial time) to unrestricted reasoning in DL-Lite F [14]. In fact, the reduction is conceptually simple and relies on completing the TBox by finding certain cyclic inclusions and ‘reversing’ them. For example, the cycle ∃r− v ∃s ∃s− v ∃r (funct r− ) (funct s− ) that consists of existential restrictions in the ‘forward direction’ and functionality state- ments in the ‘backwards direction’ would lead to the addition of the reversed cycle ∃s v ∃r− ∃r v ∃s− (funct r) (funct s). As a consequence, finite model reasoning in DL-LiteF does not require any new algorith- mic techniques and can be implemented as efficiently as unrestricted reasoning. Given that DL-LiteF is a very small fragment of ALCQI and SHIQ, these observations raise the question whether the cycle reversion technique extends also to larger fragments of these DLs. In particular, DL-Lite F is a ‘Horn DL’, and such logics are well-known to be algorithmically more well-behaved than non-Horn DLs such as ALCQI and SHIQ. Maybe this is the reason why cycle reversion works for DL-Lite F ? In this paper, we show that the cycle reversion technique extends all the way to the expressive Horn-SHIQ fragment of SHIQ, which is rather popular in database applications [6,11,5,2] and properly extends DL-Lite F and other relevant Horn fragments such as ELIF. In particular, we show that finite satisfiability in Horn-SHIQ can be reduced to unrestricted satisfiability in Horn-SHIQ by completing the TBox with reversed cycles in the style of Cosmadakis et al. and of Rosati. While the reduction technique is essentially the same as for DL-Lite F , the construction of a finite model in the correctness proof is much more subtle and demanding. Another crucial difference to the DL-Lite F case is that, when completing Horn-SHIQ TBoxes, the cycles that have to be considered can be of exponential length, and thus the reduction is not polynomial. On first glance, this of course casts a doubt on the practical relevance of the proposed reduction. Still, we are confident that our approach will lead to implementable algorithms for finite model reasoning in Horn-SHIQ. Specifically, the state-of-the-art of efficient reasoning in Horn description logics is to use so-called consequence based calculi, as introduced for Horn-SHIQ in [7] and implemented for example in the reasoners CEL, CB, and ELK [1,7,8]. Instead of first completing the TBox and then handing over the completed TBox to a reasoner, it seems well possible to integrate the reversion of cycles directly as an inference rule into such a calculus. This avoids the detection of cycles by uninformed, brute-force search, and instead searches for cycles in the consequences that have already been computed by the calculus, anyway. Since the efficiency of consequence-based calculi are largely due to the fact that, for typical inputs, the set of derived consequences is relatively small, we expect that this will work well in practical applications. For now, though, we leave it as future work to work out the details of such a calculus. Some proof details are deferred to the appendix of the long version of the paper, to be found at http://www.informatik.uni-bremen.de/tdki/research/papers.html 2 Preliminaries The original definition of Horn-SHIQ is based on a notion of polarity and somewhat unwieldy [6]; alternative definitions have been proposed later, see for example [10]. For brevity, we directly introduce Horn-SHIQ TBoxes in a certain normal form similar to the one used in [7]. Let NC and NR be countably infinite and disjoint sets of concept names and role names. A Horn-SHIQ TBox T is a set of concept inclusions (CIs) that can take the following forms: KvA K v ⊥ K v ∃r.K 0 K v ∀r.K 0 K v (6 1 r K 0 ) K v (> n r K 0 ) where K and K 0 denote a conjunction of concept names, A a concept name, r a (po- tentially inverse) role, and n ≥ 1. Throughout the paper, we will deliberately confuse conjunctions of concept names and sets of concept names. The empty conjunction is abbreviated to >. It was observed in [7] that, for the purposes of deciding unrestricted satisfiability, the above form can be assumed without loss of generality; that is, every Horn-SHIQ TBox T conformant with the original definition in [6] can be converted in polynomial time into a TBox T 0 in the above form such that for all concept names A in T , we have that A is satisfiable w.r.t. T iff A is satisfiable w.r.t. T 0 . It is straightforward to verify that all necessary transformations, such as coding out role hierarchies and transitive roles do not rely on unrestricted models to be available and thus, the introduced TBox normal form can be assumed w.l.o.g. also for finite satisfiability. The semantics for Horn-SHIQ is given as usual in terms of interpretations I. For a given TBox T and a concept inclusion C v D, we write T |= C v D if I |= C v D for all models I of T , and T |=fin C v D if the same holds for all finite models. We recall that, in Horn-SHIQ, (un)satisfiability and subsumption can be mutually reduced to each other in polynomial time, and that this also holds in the finite. The following examples show that, in Horn-SHIQ, finite and unrestricted reasoning do not coincide. Example 1. Let T = { A v ∃r.B, B v ∃r.B, B v (6 1 r− >), A u B v ⊥ }. Then A is satisfiable w.r.t. T , but not finitely satisfiable. In fact, when d ∈ AI in some model I of T , then the CI B v ∃r.B and functionality assertion on r− enforces an infinite chain r(d, d1 ), r(d1 , d2 ), . . . with d ∈ AI , d 6∈ B I and d2 , d3 , · · · ∈ B I . Let T 0 = {A1 v ∃r.A2 , A2 v ∃r.(A1 u B), > v (6 1 r− >)}. The reader might want to convince herself that T 0 6|= A1 v B, but T 0 |=fin A1 v B. Eliminating At-Least Restrictions The usual normal form for Horn-SHIQ does not comprise at-least restrictions, that is, CIs of the form K v (> n r K 0 ) are not allowed. This is achieved by replacing each such CI with K v ∃r.Bi , Bi v K 0 , Bi u Bj v ⊥ 1 ≤ i < j ≤ n (1) where each Bi is a fresh concept name. If infinite models are admitted, it is quite easy to see that this translation preserves the satisfiability of all concept names in T , exploiting the tree model property of Horn-SHIQ. For finite satisfiability, the same construction works, but a more refined argument is needed to show this. Proposition 2. Let T 0 be obtained from T by replacing the CI K v (> n r K 0 ) with the CIs (1), and let A be a concept name from T . Then A is finitely satisfiable w.r.t. T iff A is finitely satisfiable w.r.t. T 0 . Proof. The “if” direction is trivial since every model of T 0 is also a model of T . For the “only if” direction, let I be a finite model of T with AI 6= ∅. We construct a finite model J of T 0 with AJ 6= ∅ by taking n copies of I and ‘rewiring’ all role edges across the concept names Bi can be interpreted in a non-conflicting way. Specifically, since I satisfies K v (> n r K 0 ) we can choose a function succ : K × {0, . . . , n − 1} → ∆I such that the following conditions are satisfied: I – for all d ∈ K I and i < n: (d, succ(d, i)) ∈ rI and succ(d, i) ∈ (K 0 )I ; – for all d ∈ K I and i < j < n: succ(d, i) 6= succ(d, j). Then define the desired interpretation J by setting ∆J = {di | d ∈ ∆I and i < n} E J = {di | d ∈ E I and i < n} for all E ∈ NC \ {B0 , . . . , Bn−1 } BiJ = {di | d ∈ ∆I } for all i < n J I s = {(di , ei ) | (d, e) ∈ s and i < n} for all s ∈ NR \ {r} rJ = {(di , ei ) | (d, e) ∈ rI , i < n, and d ∈ / K I or e 6= succ(d, j) for any j} ∪ {(di , e(i+j) mod n ) | (d, e) ∈ rI , i, j < n, and e = succ(d, j)} It remains to verify that J is indeed a model of T 0 . Clearly, the CIs in (1) are satisfied. Moreover, it is not hard to verify that all concept inclusions in T are satisfied by J , using the fact that I is a model of T and the construction of J . o From now on, we can thus safely assume that TBoxes do not contain at-least restrictions. Note that the above translation is polynomial only if the numbers n in at-least restrictions are coded in unary. The same is of course true in unrestricted reasoning with Horn- SHIQ, where typically the same normal form is used. 3 Reduction to Unrestricted Satisfiability We give a reduction of finite satisfiability to unrestricted satisfiability based on the completion of TBoxes with certain reversed cycles. Let T be a Horn-SHIQ TBox. A finmod cycle in T is a sequence K1 , r1 , K2 , r2 , . . . , rn−1 , Kn , with K1 , . . . , Kn conjunctions of concept names and r1 , . . . , rn−1 (potentially inverse) roles that satisfies Kn = K1 and T |= Ki v ∃ri .Ki+1 and T |= Ki+1 v (6 1 ri− Ki ) for 1 ≤ i < n. By reversing a finmod cycle K1 , r1 , K2 , r2 , . . . , rn−1 , Kn in a TBox T , we mean to extend T with the concept inclusions Kj+1 v ∃rj− .Kj and Kj v (6 1 rj Kj+1 ) for 1 ≤ j < n. The completion Tf of a TBox T is obtained from T by exhaustively reversing finmod cycles. Example 3. The TBox T 0 from Example 1 entails (in unrestricted models) A1 uB v ∃r.A2 , A2 v ∃r.(A1 uB), A2 v (6 1 r− A1 uB), A2 uB v (6 1 r− A1 ). Thus, (A1 u B), r, A2 , r, (A1 u B) is a finmod cycle in T 0 , which is reversed to A2 v ∃r− .(A1 uB), A1 uB v ∃r− .A2 , A1 uB v (6 1 r A2 ), A1 v (6 1 r A2 uB). Another finmod cycle in T 0 is A1 , r, A2 , r, A1 , reversed to A2 v ∃r− .A1 , A1 v ∃r− .A2 , A2 v (6 1 r A1 ), A1 v (6 1 r A2 ). Note that Tf0 contains A1 v ∃r− .A2 , A2 v ∃r.(A1 u B), and A2 v (6 1 r A1 ). Consequently Tf0 |= A1 v B, in correspondence with T 0 |=fin A1 v B. The following result is the main result of this paper. It shows that TBox completion indeed provides a reduction from finite satisfiability to unrestricted satisfiability. Theorem 4. Let T be a Horn-SHIQ TBox and A a concept name. Then A is finitely satisfiable w.r.t. T iff A is satisfiable w.r.t. the completion Tf of T . The “only if” direction of Theorem 4 is an immediate consequence of the observation that all CIs added by the TBox completion are actually entailed by the original TBox in finite models. Lemma 5. Let K1 , r1 , . . . , rn−1 , Kn a finmod cycle in T , then for every 1 ≤ i < n, T |=fin Ki+1 v ∃ri− .Ki and T |=fin Ki v (6 1 ri Ki+1 ). Proof. We have to show that, if K1 , r1 , . . . , rn−1 , Kn is a finmod cycle in T and I is a I finite model of T , then KiI ⊆ (6 1 ri Ki+1 ) and Ki+1 I ⊆ (∃ri− .Ki )I for 1 ≤ i < n. We first note that, by the semantics of Horn-SHIQ, we must have |K1I | ≤ · · · ≤ |KnI |, thus Kn = K1 yields |K1I | = · · · = |KnI |. Fix some i with 1 ≤ i < n. Using I |KiI | = |Ki+1 I |, KiI ⊆ (∃ri .Ki+1 )I , and Ki+1 I ⊆ (6 1 ri− Ki ) , it is now easy to I verify that KiI ⊆ (6 1 ri Ki+1 ) and Ki+1 I ⊆ (∃ri− .Ki )I , as required. o The “if” direction of Theorem 4 is much more demanding to prove. It requires to construct a finite model of A and T based on the assumption that there is a (possibly infinite) model of A and Tf . Such a construction is presented in the next section. 4 Constructing Finite Models We show that the completion Tf of T captures all finite entailments of T , that is, we prove the “if” direction of Theorem 4 above. Assume that the concept name A is satisfiable w.r.t. Tf . Let CN(T ) denote the set of concept names used in T . A subset t ⊆ CN(T ) is a type for T if there is a (potentially infinite) model I of T and a d ∈ ∆I such that tpI (d) := {A ∈ CN(T ) | d ∈ AI } is identical with t. We use TP(T ) to denote the set of all types for T . Our aim is to construct a finite model I of Tf (and thus also of T ) that realizes all types in TP(T ). Note that since A is satisfiable w.r.t. Tf , there is a type t for T with A ∈ t. Since this type is realized in the finite model I of T that we construct, it follows that A is finitely satisfiable w.r.t. T as desired. Before we give details of the construction of I, we introduce some relevant notation and preliminary results. For all t, t0 ∈ TP(Tf ) and roles r, we write – t →r t0 if Tf |= t v ∃r.t0 and t0 is maximal with this property; – t →1r t0 if t →r t0 and Tf |= t0 v (6 1 r− t); – t 1↔1r t0 if t →1r t0 and t0 →1r− t. – t ⇒1r t0 if t →1r t0 and there are s ⊆ t and s0 ⊆ t0 such that s 1↔1r s0 , but Tf |= t0 v ∃r− .t does not hold. A type partition is a set P ⊆ TP(T ) that is minimal with the following conditions: – P is non-empty; – if t ∈ P and t 1↔1r t0 , then t0 ∈ P . We set P ≺ P 0 if there are t ∈ P and t0 ∈ P 0 with t0 ( t. We will later be referring to the strict partial order that is obtained by taking the transitive closure of ≺, denoted by ≺+ . A proof of the following observation can be found in the appendix. Lemma 6. ≺+ is a strict partial order. As a last bit of notation, if λ = s 1↔1r s0 , then we use λ− to denote s0 1↔1r− s. 4.1 Constructing the Model We construct I by starting with an initial interpretation and then exhaustively applying four completion steps that we denote with (c1) to (c4). While constructing the sequence, we will make sure that the following invariants are satisfied: (i1) for each d ∈ ∆I , we have tpI (d) ∈ TP(Tf ); (i2) if (d, d0 ) ∈ rI , then tpI (d) →r tpI (d0 ) or tpI (d0 ) →r− tpI (d); (i3) if Tf |= K v (6 1 r K 0 ), then I |= K v (6 1 r K 0 ). We shall prove in Section 4.2 that each of the steps (c1) to (c4) indeed preserves these invariants. The initial interpretation I is defined by introducing an element for every type, intepreting the concept names in the obvious way, and interpreting all role names as empty: ∆I = TP(Tf ); AI = {t ∈ TP(Tf ) | A ∈ t}; rI = ∅. The four completion steps are described in detail below. We prefer to apply rules with smaller numbers, that is, if completion steps (ci) and (cj) are both applicable and i < j, then we apply (ci) first. (c1) Select a d ∈ ∆I such that tpI (d) ⇒1r t, and d ∈ / (∃r.t)I . Add a fresh domain element e, and modify the extension of concept and role names such that tpI (e) = t and (d, e) ∈ rI . (c2) Select a type partition P that is minimal w.r.t. the order ≺+ , a λ = s 1↔1r s0 with s ∈ P , and an element d ∈ ∆I such that d ∈ sI and d ∈ / (∃r.s0 )I . For each s ∈ P , set ns = |{d ∈ ∆I | d ∈ sI }|. Let nmax = max{ns | s ∈ P }. Reserve fresh domain elements ∆ := {ds,i | s ∈ P and ns < i ≤ nmax }. For each s ∈ P , define a set of s-instances Is = {d ∈ ∆I | d ∈ sI } ∪ {ds,i | ns < i ≤ nmax }. To proceed, we treat each λ = s 1↔1r s0 with s, s0 ∈ P separately. Thus, fix such a λ. Define I Rλ := {(d, e) ∈ rI | d ∈ sI and e ∈ s0 }. We first note that it is a consequence of invariant (i3) that (∗) the relation Rλ is functional and inverse functional. In fact, let (d, e1 ), (d, e2 ) ∈ Rλ . Then (d, e1 ), (d, e2 ) ∈ rI , d ∈ sI , and e1 , e2 ∈ I s0 . By λ, we have Tf |= s v (6 1 r s0 ). Thus, (i3) yields e1 = e2 . Inverse functionality can be shown analogously. Let Rλ1 be the domain of Rλ , and let Rλ2 be the range. By (∗), we have |Rλ1 | = |Rλ2 |. By definition of ∆, we have |Is | = |Is0 |. Moreover, Rλ1 ⊆ Is and Rλ2 ⊆ Is0 . We can thus choose a bijection πλ between Is \ Rλ1 and Is0 \ Rλ2 . Now extend I as follows: • add all domain elements in ∆; • extend rI with πλ , for each λ = s 1↔1r s0 ; • extend rI with the converse of πλ , for each λ = s 1↔1r− s0 ; • interpret concept names so that tpI (ds,i ) = s for all ds,i ∈ ∆. (c3) Select a d ∈ ∆I such that tpI (d) →1r t and d ∈ / (∃r.t)I . Add a fresh domain element e, and modify the extension of concept and role names such that tpI (e) = t and (d, e) ∈ rI . (c4) Select a d ∈ ∆I such that tpI (d) →r t and d ∈/ (∃r.t)I . I Add the edge (d, t) to r , where t is the element for the type t introduced in the initial interpretation I. We briefly discuss the main effects of prioritizing the completion steps. It is important to prefer (c1) over (c2): together with the preference of type partitions that are minimal w.r.t. ≺+ in (c2), this ensures that when (c2) is executed on type partition P , λ = s 1↔1r− s0 with s, s0 ∈ P , and d ∈ Is \ Rλ1 , then not only tpI (d) ⊇ s, but actually tpI (d) = s. This central property, put as Lemma 7 below, is essential to guarantee preservation of invariants (i2) and (i3) by execution of (c2). Preferring (c1) and (c2) over (c3) ensures that, when (c3) is executed, then there are no s ⊆ tpI (d) and s0 ⊆ t such that s 1↔1r s0 ; and preferring (c3) over (c4) ensures that, when (c4) is executed, then we have Tf 6|= tpI (d) v (6 1 r t). These statements are provided here only to help in understanding the model construction. A formal proof is omitted at this point, but it can be recovered from the proofs given in the subsequent sections. 4.2 Satisfaction of Invariants Application of (c1) preserves all invariants. It is obvious that the invariants (i1) and (i2) are preserved with each single application of (c1). We have to show that the same is true for (i3). Assume that completion processed d ∈ ∆I with tpI (d) ⇒1r t, and that e is the fresh domain element added. Assume to the contrary of what is to be shown that Tf |= K v (6 1 r K 0 ) and there is a e0 ∈ ∆I distinct from e such that d ∈ K I , I (d, e0 ) ∈ rI , and e, e0 ∈ K 0 . According to (i2), we distinguish the following cases: – tpI (d) →r tpI (e0 ) Then Tf |= tpI (d) v ∃r.tpI (e0 ) and tpI (e0 ) is maximal with this property. Since tpI (d) →r t, we additionally have Tf |= tpI (d) v ∃r.t. Since K ⊆ tpI (d) and I e, e0 ∈ K 0 implies K 0 ⊆ tpI (e0 ) ∩ t, a simple semantic argument shows that Tf |= K v ∃r.(tpI (e0 ) ∪ t). The maximality of tpI (e0 ) thus implies t ⊆ tpI (e0 ), / (∃r.t)I was true before the completion step. in contradiction to the fact that d ∈ – tpI (e0 ) →r− tpI (d). Then Tf |= tpI (e0 ) v ∃r− .tpI (d) and, additionally, we have Tf |= tpI (d) v ∃r.t. Since K ⊆ tpI (d) and K 0 ⊆ tpI (e0 ) ∩ t, a simple semantic argument shows that Tf |= tpI (e0 ) v t. Since tpI (e0 ) is a type for Tf by (i1), it follows that t ⊆ tpI (e0 ). This contradicts the fact that d ∈ / (∃r.t)I was true before the completion step. Application of (c2) preserves all invariants. Invariant (i1) is clearly preserved by each single application of (c2). We have to prove that the same is true for (i2) and (i3). First, we show that the following property holds: Lemma 7. If λ = s 1↔1r s0 and d ∈ Is \ Rλ1 , then tpI (d) = s. To show that (i2) is preserved by step (c2), consider an arbitrary pair (d, d0 ) ∈ rI that has been added in a step (c2). Hence πλ (d) = d0 , i.e., there is some λ = s 1↔1r s0 such that d ∈ Is \ Rλ1 and d0 ∈ Is0 \ Rλ2 . From Lemma 7, we obtain tpI (d) = s. Analogously, considering λ0 = s0 1↔1r− s and the fact d0 ∈ Is0 \ Rλ2 = Is0 \ Rλ1 0 , we obtain from Lemma 7 that tpI (d0 ) = s0 . Consequently, s 1↔1r s0 yields tpI (d) →r tpI (d0 ) and tpI (d0 ) →r− tpI (d). We now show that (i3) is preserved by step (c2). Let Tf |= K v (6 1 r K 0 ), and assume to the contrary of what is to be shown that, after some application of (c2), there I are (d, d1 ), (d, d2 ) ∈ rI with d ∈ K I , d1 , d2 ∈ K 0 , and d1 6= d2 . We distinguish the following cases: – (d, d1 ) was added by an application of (c2), (d, d2 ) was not. By the former, there is λ = s 1↔1r s0 such that d ∈ Is \ Rλ1 , d1 ∈ Is0 \ Rλ2 , and (d, d1 ) ∈ πλ . By Lemma 7, d ∈ Is \ Rλ1 yields tpI (d) = s. Moreover, d1 ∈ Is0 \ Rλ2 implies d1 ∈ Is0 \ Rλ1 − , and thus another application of Lemma 7 yields tpI (d1 ) = s0 . Since (d, d2 ) was not added by step (c2), (i2) gives the following subcases: • tpI (d) →r tpI (d2 ). Thus Tf |= tpI (d) v ∃r.tpI (d2 ) and tpI (d2 ) is maximal with this property. Since tpI (d) = s and by λ, Tf |= tpI (d) v ∃r.tpI (d2 ). Using the facts that Tf |= K v (6 1 r K 0 ), K ⊆ tpI (d) = s, K 0 ⊆ tpI (d2 ), and K 0 ⊆ tpI (d1 ) = s0 , an easy semantic argument shows that Tf |= tpI (d) v ∃r.(tpI (d2 ) ∪ s0 ). The maximality of tpI (d2 ) thus yields s0 ⊆ tpI (d2 ). Thus, d ∈ (∃r.s0 )I was true before step (c2) was applied, which is a contradiction to d∈ / Rλ1 . • tpI (d2 ) →r− tpI (d). Then Tf |= tpI (d2 ) v ∃r− .s. By λ, we have Tf |= s v ∃r.s0 . Since K ⊆ s, K ⊆ tpI (d2 ), K ⊆ tpI (d1 ) = s0 , and Tf |= K v (6 1 r K 0 ), a simple semantic argument shows that s0 ⊆ tpI (d2 ). This again means that d ∈ (∃r.s0 )I was true before step (c2) was applied, in contradiction / Rλ1 . to d ∈ – both (d, d1 ) and (d, d2 ) were added by an application of (c2). Then there are λ1 and λ2 , such that, for i ∈ {1, 2}, we have λi = si 1↔1r s0i , (d, di ) ∈ πλi , d ∈ Isi \ Rλ1 i , di ∈ Is0i \ Rλ2 i . Applying Lemma 7 to λi and d ∈ Isi \ Rλ1 i yields si = tpI (d), for i ∈ {1, 2}. Consequently, s1 = s2 . We next show s01 = s02 , thus λ1 = λ2 . For uniformity, we use s to denote s1 and s2 . From λi , we obtain Tf |= s v ∃r.si and si is maximal with this property, for i ∈ {1, 2}. Note that di ∈ Is0i \ Rλ2 i implies di ∈ Is0i \ Rλ1 − . Applications of Lemma 7 to λ− 1 i and di ∈ Is0i \ Rλ− yield i i tpI (di ) = si . Using the facts that Tf |= s v ∃r.si for i ∈ {1, 2}, K ⊆ tpI (d) = s, K 0 ⊆ tpI (di ) = si for i ∈ {1, 2}, and Tf |= K v (6 1 r K 0 ), an easy semantic argument shows that Tf |= s v ∃r.(s1 ∪ s2 ). The maximality of s1 and s2 thus implies s1 = s2 as desired. Hence, λ1 = λ2 and (d, d1 ), (d, d2 ) ∈ πλ1 . Since πλ1 is a bijection, we obtain d1 = d2 , a contradiction. Application of (c3) and (c4) preserves all invariants. It is obvious that the invariants (i1) and (i2) are preserved with each single application of (c3) or (c4). To show that the same is true for (i3), we can use the same proof as for (c1) because the assumptions of (c3) and (c4) differ from that of (c1) in weakening tpI (d) ⇒1r t to tpI (d) →1r t and tpI (d) →r t, respectively, which is sufficient for that proof. 4.3 Termination of Model Construction We show that the constructed interpretation I is indeed finite. Proposition 8. ∆I is finite. Proof. To analyze the termination of the construction of I, we associate a certain directed tree T = (V, E) with the model I that makes explicit the way in which I was constructed. Note that only the completion steps (c1) to (c3) introduce new domain elements and that (c1) and (c3) introduce a single new element with each application whereas (c2) introduces a whole (finite) set of fresh elements. Also note that each application of a completion step is triggered by a single domain element d for which some existential restriction is not yet satisfied. Now, the tree T is defined as follows: – V consists of all subsets of ∆I that were introduced together by a single application of one of the completion steps (c1) to (c3); additionally, the set of all elements in the initial interpretation I is a node in V (in fact, the root node); – the edge (v, v 0 ) is included in E if the elements in v 0 were introduced by an applica- tion of a completion step to an element d of v. We call this element the trigger of v 0 and denote it with dv0 . To show that ∆I is finite, it clearly suffices to show that V is finite. The outdegree of T is finite since every rule application introduces only finitely many elements. By König’s Lemma, it thus remains to show that T is of finite depth. We first note that an easy analysis of the completion steps (c1) to (c3) reveals the following property: (∗) if (v1 , v2 ), (v2 , v3 ) ∈ E, then there are d0 , . . . , dk ∈ v2 and roles r0 , . . . , rk−1 s.t. • d0 = dv2 ∈ v1 , d1 , . . . , dk ∈ v2 , and dk = dv3 ∈ v2 ; • tpI (di ) →1ri tpI (di+1 ) for all i < k. Now assume towards a contradiction that the depth of T is larger than 2|TP(Tf )| + 1 and choose a concrete path v1 · · · vn with v1 the root of T and n > 2|TP(Tf )| + 1. This path gives rise to a corresponding sequence of triggers dv1 , . . . , dvn . Since the length of this sequence exceeds 2|TP(Tf )|, there must be i, j with 1 ≤ i < j ≤ n and such that tpI (dvi ) = tpI (dvj ) and j > i + 1. By applying (∗) multiple times, we obtain a sequence of domain elements d0 , . . . , dk and roles r0 , . . . , rk−1 such that 1. d0 = dvi ∈ vi−1 , d1 ∈ vi , and dp = dvj ∈ vj−1 ; 2. tpI (d` ) →1r` tpI (d`+1 ) for ` < k. 3. d0 , . . . , dk contains all elements dvi , . . . , dvj . Since tpI (dvi ) = tpI (dvj ) and by Point 2, tpI (d0 ), r0 , . . . , rk−1 , tpI (dk ) is a finmod cycle in Tf . Since all finmod cycles in Tf have been reversed, we have tpI (d0 ) 1↔1r0 tpI (d1 ) 1↔1r1 · · · 1↔1rn−1 tpI (dn ). (†) In the appendix, we prove the following claim: Claim. If step (c1) or step (c3) is triggered by d ∈ ∆I and generates a new element e ∈ ∆I , then there is no role r such that tpI (d) 1↔1r tpI (e). Since dvi ∈ vi−1 and d1 ∈ vi , d1 was generated by the application of a completion step triggered by d0 . By (†) and the claim, this completion step must be (c2). By definition of (c2) and (†), all elements d1 , . . . , dk have been introduced by exactly this application of (c2). This leads to a contradiction: we have d1 ∈ vi and dk ∈ vj−1 , and since j > i + 1, vi 6= vj−1 . Consequently, d1 and dk were introduced by different applications of completion steps. o 4.4 Correctness of Model Construction To complete the proof of the “if” direction of Theorem 4, it remains to show the following. Proposition 9. I is a model of Tf . Proof. We show that for every axiom K v C ∈ Tf , we have that I |= K v C. We distinguish the following cases: – C = A. Let d ∈ K I . Then K ⊆ tpI (d) and by (i1) tpI (d) ∈ TP(Tf ). Since Tf |= K v A, this yields A ∈ tpI (d) and thus d ∈ AI . – C = ⊥. Follows from (i1). Indeed since for every d ∈ ∆I , tp(d) ∈ TP(Tf ), K I = ∅. – C = ∃r.K 0 . Let d ∈ K I . Then we have that K ⊆ tpI (d). Since Tf |= K v ∃r.K 0 , we have that tpI (d) →r t0 for some t0 with K 0 ⊆ t0 . Thus there is some d0 with K 0 ⊆ tpI (d0 ) such that (d, d0 ) ∈ rI was added by an application of (c1), (c2), (c3) or (c4). In fact, if no such d0 is added by (c1) to (c3), then the edge (d, d0 ) ∈ rI will clearly be added by (c4). – C = ∀r.K 0 . Let d ∈ K I and (d, d0 ) ∈ rI , We have that K ⊆ tpI (d). Further, by (i2), we can distinguish the following cases: • tpI (d) →r tpI (d0 ). Then Tf |= tpI (d) v ∃r.tp(d0 ) and tp(d0 ) is maximal with this property. Since Tf |= K v ∀r.K 0 , we have that Tf |= tpI (d) v ∃r.tp(d0 ) ∪ K 0 , and the maximality of tp(d0 ) yields K 0 ⊆ tp(d0 ), and thus d0 ∈ K 0I . • tpI (d0 ) →r− tpI (d). Then Tf |= tpI (d0 ) v ∃r− .tpI (d). Together with Tf |= K v ∀r.K 0 , we obtain Tf |= tpI (d0 ) v K 0 . Since tpI (d0 ) ∈ TP(Tf ) by (i1), we obtain K 0 ⊆ tpI (d0 ) and thus d0 ∈ K 0I . – C = (6 1 r K)0 . Follows from (i3). o 5 Conclusion We have presented a reduction from finite satisfiability in Horn-SHIQ to unrestricted satisfiability, extending the technique introduced for DL-Lite F in [14]. As discussed in the introduction, we believe that our technique is a more suitable basis for efficient implementation than the techniques for full ALCQI and SHIQ based on exponentially large systems of inequalities. As future work, we plan to develop a consequence based calculus for finite satis- fiability in Horn-SHIQ and to extend the results obtained in this paper from finite satisfiability to answering conjunctive queries over ABoxes, assuming finite models. While we believe that the constructions given in this paper can be easily extended to instance query answering over ABoxes, the treatment of full conjunctive queries requires significant modification of the model construction. References 1. F. Baader, C. Lutz, and B. Suntisrivaraporn. CEL – a polynomial-time reasoner for life science ontologies. In Proc. of IJCAR-06, volume 4130 of LNCS, pages 287–291. Springer, 2006. 2. M. Bienvenu, C. Lutz, and F. Wolter. First-order rewritability of atomic queries in Horn description logics. In Proc. of IJCAI-13. IJCAI/AAAI, 2013. 3. D. Calvanese. Finite model reasoning in description logics. In Proc. of KR-96, pages 292–303. Morgan Kaufmann, 1996. 4. S.S. Cosmadakis, P.C. Kanellakis, and M.Y. Vardi. Polynomial-time implication problems for unary inclusion dependencies. J. ACM, 37(1):15–46, 1990. 5. T. Eiter, M. Ortiz, M. Šimkus, T.-K. Tran, and G. Xiao. Towards practical query answering for Horn-SHIQ. In Proc. of DL-12, volume 846 of CEUR-WS.org, 2012. 6. U. Hustadt, B. Motik, and U. Sattler. Reasoning in description logics by a reduction to disjunctive datalog. J. Autom. Reasoning, 39(3), 2007. 7. Y. Kazakov. Consequence-driven reasoning for Horn SHIQ ontologies. In Proc. of IJCAI-09, pages 2040–2045, 2009. 8. Y. Kazakov, M. Krötzsch, and F. Simančı́k. Unchain my EL reasoner. In Proc. of DL-11, volume 745 of CEUR-WS.org, 2011. 9. C. Lutz, U. Sattler, and L. Tendera. The complexity of finite model reasoning in description logics. Information and Computation, 199:132–171, 2005. 10. C. Lutz and F. Wolter. Non-uniform data complexity of query answering in description logics. In Proc. of KR-12. AAAI Press, 2012. 11. M. Ortiz, S. Rudolph, and M. Šimkus. Query answering in the Horn fragments of the descrip- tion logics SHOIQ and SROIQ. In Proc. of IJCAI-11, pages 1039–1044. IJCAI/AAAI, 2011. 12. L. Pacholski, W. Szwast, and L. Tendera. Complexity results for first-order two-variable logic with counting. SIAM J. Comput., 29(4):1083–1117, 2000. 13. I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. J. of Logic, Language and Information, 14(3):369–395, 2005. 14. R. Rosati. Finite model reasoning in DL-Lite. In Proc. of ESWC-08, volume 5021 of LNCS, pages 215–229. Springer, 2008.