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-LiteF 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.
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 S HIQ, which are both a
fragment of the OWL2 DL ontology language. While finite model reasoning in ALCQI
and S HIQ are known to have the same complexity as unrestricted reasoning, namely
EXPTIME-complete [
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 [
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 [
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
The original definition of Horn-SHIQ is based on a notion of polarity and somewhat
unwieldy [
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: K v A
K v ?
K v 9r:K0
K v 8r:K0
K v (6 1 r K0)
K v (> n r K0) where K and K0 denote a conjunction of concept names, A a concept name, r a (potentially 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 [
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 j= C v D if I j= C v D for all models I of T , and T j= n 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 = f A v 9r:B; B v 9r:B; B v (6 1 r >); A u B v ? g. Then A is satisfiable w.r.t. T , but not finitely satisfiable. In fact, when d 2 AI in some model I of T , then the CI B v 9r:B and functionality assertion on r enforces an infinite chain r(d; d1); r(d1; d2); : : : with d 2 AI , d 62 BI and d2; d3; 2 BI . Let T 0 = fA1 v 9r:A2; A2 v 9r:(A1 u B); > v (6 1 r >)g. The reader might want to convince herself that T 6j
0 = A1 v B, but T 0 j= n 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 K0) are not allowed. This is achieved by replacing each such CI with
K v 9r:Bi;
Bi v K0;
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 K0) 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 K0) we can choose a function succ : KI f0; : : : ; n 1g ! I such that the following conditions are satisfied: – for all d 2 KI and i < n: (d; succ(d; i)) 2 rI and succ(d; i) 2 (K0)I ; – for all d 2 KI and i < j < n: succ(d; i) 6= succ(d; j).
J = fdi j d 2
I and i < ng EJ = fdi j d 2 EI and i < ng BiJ = fdi j d 2
I g sJ = f(di; ei) j (d; e) 2 sI and i < ng for all E 2 NC n fB0; : : : ; Bn 1g for all i < n for all s 2 NR n frg rJ = f(di; ei) j (d; e) 2 rI ; i < n; and d 2= KI or e 6= succ(d; j) for any jg [ f(di; e(i+j) mod n) j (d; e) 2 rI ; i; j < n; and e = succ(d; j)g 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 HornSHIQ, where typically the same normal form is used. 3
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 j= Ki v 9ri:Ki+1 and T j= 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 9rj :Kj and Kj v (6 1 rj Kj+1) Thus, (A1 u B); r; A2; r; (A1 u B) is a finmod cycle in T 0, which is reversed to
A2 v 9r :A1;
A1 v 9r :A2;
A2 v (6 1 r A1);
A1 v (6 1 r A2): Note that Tf0 contains A1 v 9r :A2, A2 v 9r:(A1 u B), and A2 v (6 1 r A1). Consequently Tf0 j= A1 v B, in correspondence with T 0 j= n 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 T j= n Ki+1 v 9ri :Ki and T j= n Ki v (6 1 ri Ki+1). i < n, jKiI j = jKiI+1j, KI
i verify that KiI (6 1 ri Ki+1)I and KiI+1 Proof. We have to show that, if K1; r1; : : : ; rn 1; Kn is a finmod cycle in T and I is a finite model of T , then KiI (6 1 ri Ki+1)I and KiI+1 (9ri :Ki)I for 1 i < n. We first note that, by the semantics of Horn-SHIQ, we must have jK1I j jKnI j, thus Kn = K1 yields jK1I j = = jKnI j. Fix some i with 1 i < n. Using (9ri:Ki+1)I , and KiI+1 (6 1 ri Ki)I , it is now easy to o (9ri :Ki)I , as required.
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
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 2 I such that tpI (d) := fA 2 CN(T ) j d 2 AI g 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 2 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 2 TP(Tf ) and roles r, we write – t !r t0 if Tf j= t v 9r:t0 and t0 is maximal with this property; – t !r1 t0 if t !r t0 and Tf j= t0 v (6 1 r t); – t 1$r1 t0 if t !r1 t0 and t0 !r1 t. – t )r1 t0 if t !r1 t0 and there are s t and s0
Tf j= t0 v 9r :t does not hold. t0 such that s 1$r1 s0, but A type partition is a set P
– P is non-empty; – if t 2 P and t 1$r1 t0, then t0 2 P .
We set P P 0 if there are t 2 P and t0 2 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$r1 s0, then we use to denote s0 1$r1
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 2 I , we have tpI (d) 2 TP(Tf ); (i2) if (d; d0) 2 rI , then tpI (d) !r tpI (d0) or tpI (d0) !r (i3) if Tf j= K v (6 1 r K0), then I j= K v (6 1 r K0). tpI (d); 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 = ft 2 TP(Tf ) j A 2 tg; 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 2 I such that tpI (d) )r1 t, and d 2= (9r: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) 2 rI . (c2) Select a type partition P that is minimal w.r.t. the order +, a s 2 P , and an element d 2 I such that d 2 sI and d 2= (9r:s0)I . For each s 2 P , set ns = jfd 2 Reserve fresh domain elements
I j d 2 sI gj. Let nmax = maxfns j s 2 P g. := fds;i j s 2 P and ns < i nmaxg:
Is = fd 2
I j d 2 sI g [ fds;i j ns < i
nmaxg: = s 1$r1 s0 with s; s0 2 P separately. Thus, fix such To proceed, we treat each a . Define
R := f(d; e) 2 rI j d 2 sI and e 2 s0I g: 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) 2 R . Then (d; e1); (d; e2) 2 rI , d 2 sI , and e1; e2 2 s0I . By , we have Tf j= s v (6 1 r s0). Thus, (i3) yields e1 = e2. Inverse functionality can be shown analogously.
Let R1 be the domain of R , and let R2 be the range. By ( ), we have jR1 j = jR2 j. By definition of , we have jIsj = jIs0 j. Moreover, R1 Is and R2 Is0 . We can thus choose a bijection between Is n R1 and Is0 n R2 . Now extend I as follows: add all domain elements in ; extend rI with , for each = s 1$r1 s0; extend rI with the converse of , for each = s 1$r1 s0; interpret concept names so that tpI (ds;i) = s for all ds;i 2 . (c3) Select a d 2 I such that tpI (d) !r1 t and d 2= (9r: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) 2 rI . (c4) Select a d 2 I such that tpI (d) !r t and d 2= (9r:t)I .
Add the edge (d; t) to rI , 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$r1 s0 with s; s0 2 P , and d 2 Is n R1 , 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$r1 s0; and preferring (c3) over (c4) ensures that, when (c4) is executed, then we have Tf 6j= 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. 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 2 I with tpI (d) )r1 t, and that e is the fresh domain element added. Assume to the contrary of what is to be shown that Tf j= K v (6 1 r K0) and there is a e0 2 I distinct from e such that d 2 KI , (d; e0) 2 rI , and e; e0 2 K0I . According to (i2), we distinguish the following cases: – tpI (d) !r tpI (e0)
Then Tf j= tpI (d) v 9r:tpI (e0) and tpI (e0) is maximal with this property. Since tpI (d) !r t, we additionally have Tf j= tpI (d) v 9r:t. Since K tpI (d) and e; e0 2 K0I implies K0 tpI (e0) \ t, a simple semantic argument shows that Tf j= K v 9r:(tpI (e0) [ t). The maximality of tpI (e0) thus implies t tpI (e0), in contradiction to the fact that d 2= (9r:t)I was true before the completion step. – tpI (e0) !r tpI (d).
Then Tf j= tpI (e0) v 9r :tpI (d) and, additionally, we have Tf j= tpI (d) v 9r:t. Since K tpI (d) and K0 tpI (e0) \ t, a simple semantic argument shows that Tf j= 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 2= (9r:t)I was true before the completion step.
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:
= s 1$r1 s0 and d 2 Is n R1 , then tpI (d) = s.
To show that (i2) is preserved by step (c2), consider an arbitrary pair (d; d0) 2 rI that has been added in a step (c2). Hence (d) = d0, i.e., there is some = s 1$r1 s0 such that d 2 Is n R1 and d0 2 Is0 n R2 . From Lemma 7, we obtain tpI (d) = s. Analogously, considering 0 = s0 1$r1 s and the fact d0 2 Is0 n R2 = Is0 n R10 , we obtain from Lemma 7 that tpI (d0) = s0. Consequently, s 1$r1 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 j= K v (6 1 r K0), and assume to the contrary of what is to be shown that, after some application of (c2), there are (d; d1); (d; d2) 2 rI with d 2 KI , d1; d2 2 K0I , 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$r1 s0 such that d 2 Is n R1 , d1 2 Is0 n R2 , and (d; d1) 2 . By Lemma 7, d 2 Is n R1 yields tpI (d) = s. Moreover, d1 2 Is0 n R2 implies d1 2 Is0 n R1 , 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 j= tpI (d) v 9r:tpI (d2) and tpI (d2) is maximal with this property. Since tpI (d) = s and by , Tf j= tpI (d) v 9r:tpI (d2). Using the facts that Tf j= K v (6 1 r K0), K tpI (d) = s, K0 tpI (d2), and K0 tpI (d1) = s0, an easy semantic argument shows that Tf j= tpI (d) v 9r:(tpI (d2) [ s0). The maximality of tpI (d2) thus yields s0 tpI (d2). Thus, d 2 (9r:s0)I was true before step (c2) was applied, which is a contradiction to d 2= R1 . tpI (d2) !r tpI (d). Then Tf j= tpI (d2) v 9r :s. By , we have Tf j= s v 9r:s0. Since K s, K tpI (d2), K tpI (d1) = s0, and Tf j= K v (6 1 r K0), a simple semantic argument shows that s0 tpI (d2). This again means that d 2 (9r:s0)I was true before step (c2) was applied, in contradiction to d 2= R1 . – both (d; d1) and (d; d2) were added by an application of (c2). Then there are 1 and 2, such that, for i 2 f1; 2g, we have i = si 1$r1 s0i; (d; di) 2 i ; d 2 Isi n R1i ; di 2 Is0i n R2i : Applying Lemma 7 to i and d 2 Isi n R1i yields si = tpI (d), for i 2 f1; 2g. 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 j= s v 9r:si and si is maximal with this property, for i 2 f1; 2g. Note that di 2 Is0i n R2i implies di 2 Is0i n R1 . Applications of Lemma 7 to i and di 2 Is0i n R1 yield i i tpI (di) = si. Using the facts that Tf j= s v 9r:si for i 2 f1; 2g, K tpI (d) = s, K0 tpI (di) = si for i 2 f1; 2g, and Tf j= K v (6 1 r K0), an easy semantic argument shows that Tf j= s v 9r:(s1 [ s2). The maximality of s1 and s2 thus implies s1 = s2 as desired.
Hence, 1 = 2 and (d; d1); (d; d2) 2 1 . Since 1 is a bijection, we obtain d1 = d2, a contradiction.
(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) )r1 t to tpI (d) !r1 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; v0) is included in E if the elements in v0 were introduced by an application of a completion step to an element d of v. We call this element the trigger of v0 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 Ko¨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) 2 E, then there are d0; : : : ; dk 2 v2 and roles r0; : : : ; rk 1 s.t. tpI (di) !r1i tpI (di+1) for all i < k.
d0 = dv2 2 v1, d1; : : : ; dk 2 v2, and dk = dv3 2 v2; Now assume towards a contradiction that the depth of T is larger than 2jTP(Tf )j + 1 and choose a concrete path v1 vn with v1 the root of T and n > 2jTP(Tf )j + 1. This path gives rise to a corresponding sequence of triggers dv1 ; : : : ; dvn . Since the length of this sequence exceeds 2jTP(Tf )j, 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 2 vi 1, d1 2 vi, and dp = dvj 2 vj 1; 2. tpI (d`) !r1` 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$r10 tpI (d1) 1$r11 1 1 $rn 1 tpI (dn): (y) In the appendix, we prove the following claim: Claim. If step (c1) or step (c3) is triggered by d 2 I and generates a new element e 2 I , then there is no role r such that tpI (d) 1$r1 tpI (e).
Since dvi 2 vi 1 and d1 2 vi, d1 was generated by the application of a completion step triggered by d0. By (y) and the claim, this completion step must be (c2). By definition of (c2) and (y), all elements d1; : : : ; dk have been introduced by exactly this application of (c2). This leads to a contradiction: we have d1 2 vi and dk 2 vj 1, and since j > i + 1, vi 6= vj 1. Consequently, d1 and dk were introduced by different applications of completion steps. o tpI (d) !r tpI (d0). Then Tf j= tpI (d) v 9r:tp(d0) and tp(d0) is maximal with this property. Since Tf j= K v 8r:K0, we have that Tf j= tpI (d) v 9r:tp(d0) [ K0, and the maximality of tp(d0) yields K0 tp(d0), and thus d0 2 K0I . tpI (d0) !r tpI (d). Then Tf j= tpI (d0) v 9r :tpI (d). Together with Tf j= K v 8r:K0, we topbIt(adin0)Tafnjd=thtupsI (dd0 02) vKK0I .0. Since tpI (d0) 2 TP(Tf ) by (i1), we obtain K0 – C = (6 1 r K)0. Follows from (i3). o 5
We have presented a reduction from finite satisfiability in Horn-SHIQ to unrestricted
satisfiability, extending the technique introduced for DL-LiteF in [
As future work, we plan to develop a consequence based calculus for finite satisfiability 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.