We present a decidability result for entailment of conjunctive queries (CQs) in the very expressive Description Logic (DL) ALCHOIQb [1] by establishing nite representability of countermodels in the case of non-entailment. Our result also generalizes to unions of conjunctive queries and SHOIQ provided the query contains only simple roles, and we are con dent that the technique extends to SROIQ under the simple roles restriction as well. Full proofs and additional material can be found in the accompanying technical report [2]. Throughout the paper, we use the DL ALCOIF b, where b stands for safe Boolean role expressions. Any ALCHOIQb knowledge base (KB) can be polynomially reduced to an ALCOIF b KB with extended signature, while preserving query (non-)entailment [3].W.l.o.g., we assume that KBs contain an empty ABox (with nominals the ABox can be internalized) and that all GCIs are simpli ed to one of the following forms:
l Ai v
G Bj j A
fog j A v 8U:B j A v 9U:B j func(f );
(
Let NV be a countably in nite set of variables, A a concept name, r a role name, and x; y 2 NV variables. An atom is an expression A(x) or r(x; y). A Boolean conjunctive query q is a non-empty set of atoms. We use var(q) to denote the set of (existentially quanti ed) variables occurring in q and ](q) for the number of atoms in q. For I = ( I ; I ) an interpretation, A(x); r(x; y) atoms, and : var(q) ! I a total function, we write (i) I j= A(x) if (x) 2 AI and (ii) I j= r(x; y) if h (x); (y)i 2 rI . If I j= At for all atoms At 2 q, we write I j= q and say that I satis es q. We write I j= q if there exists a function such that I j= q and call a match for q in I. If I j= K implies I j= q, we say that K entails q and write K j= q. W.l.o.g., we assume that queries are connected. Given a KB K and a CQ q, the query entailment problem is to decide whether K j= q.
As a running example, we use a KB K containing the axioms fog v 9r:A; A v 9r:A; A v 9s:B; B v CtD; C v 9f:E; D v 9g:E; E v Btfog; func(f ); func(g ). The left hand side of Fig. 1 (p. 6) displays a model for K.
Unless stated otherwise, we use A for a concept name, r for a role, f for a functional or inverse functional role, U for a safe Boolean role expression, o for a nominal, q for a connected Boolean conjunctive query, K for a simpli ed ALCOIF b knowledge base, and I for an interpretation ( I ; I ).
We show decidability by proving that non-entailment is always witnessed by a regular model which is nitely representable. Our procedure enumerates these nite representations and terminates if the entailment does not hold. If it holds, termination can be ensured because rst-order logic is recursively enumerable [4]. To construct nitely representable models, we rst \unravel" models into interpretations, called forest quasi-models, that have a real forest shape. We then provide a way of \collapsing" such forest quasi-models back into real models that still have a kind of forest shape, called forest model, but which have a possibly in nite set of roots. Finally, we introduce transformations that work on the unraveled forest quasi-models, and the resulting interpretations can be collapsed into forest models with only a nite set of roots. We can then adapt standard cycle detection techniques such as (tree) blocking to obtain the desired nite representations. 2
We rst introduce interpretations and models that have a kind of forest shape. Please note that, unless we call a forest strict, our notion of a forest is very weak since we do also allow for arbitrary relations between tree elements and roots. De nition 1. A tree T is a non-empty, pre x-closed subset of IN . A forest F is a subset of R IN , where R is a non-empty, countable, possibly in nite set of elements f 1; : : : ; ng such that, for each 2 R, the set fw j ( ; w) 2 F g is a tree. Each pair ( ; ") 2 F is called a root of F . For ( ; w); ( 0; w0) 2 F , we call ( 0; w0) a successor of ( ; w) if 0 = and w0 = w c for some c 2 IN, where \ " denotes concatenation; ( 0; w0) is a predecessor of ( ; w) if 0 = and w = w0 c for some c 2 IN; ( 0; w0) is a neighbor of ( ; w) if ( 0; w0) is a successor of ( ; w) or vice versa. A node ( ; w) is an ancestor of a node ( 0; w0) if = 0 and w is a pre x of w0 and it is a descendant if = 0 and w0 is a pre x of w. We use jwj to denote the length of w. The branching degree d(w) of a node w in a tree T is the number of successors of w.
A forest interpretation of K is an interpretation I that satis es: FI1 I is a forest with roots R; FI2 there is a total and surjective function : nom(K) ! R f"g s.t. (o) = ( ; ") i oI = ( ; "); FI3 for each role r 2 rol(K), if h( ; w); ( 0; w0)i 2 rI , then either (a) w = " or w0 = ", or (b) ( ; w) is a neighbor of ( 0; w0).
If I j= K we say that I is a forest model for K. With nomFree(K), we denote a knowledge base obtained from K by replacing each nominal concept fog with o 2 nom(K) with a fresh concept name No. A forest quasi-interpretation for K is an interpretation J that satis es FI1 and FI3, and the adapted version FI20 of FI2 that there is a total and surjective function : nom(K) ! R f"g s.t.
(o) = ( ; ") i ( ; ") 2 NoJ (there might be other ( ; w) 2 J with w 6= " s.t. ( ; w) 2 NoJ ). If J j= nomFree(K) we say that J is a forest quasi-model for K. A forest (quasi) interpretation I is a strict forest (quasi) interpretation if, in condition FI3, only (b) is allowed; it is a tree interpretation, if it has a single root. If there is a k such that d(w) k for each ( ; w) 2 I , then we say that I has branching degree k.
Let I; I0 be two forest interpretations of K with 1; 2 2 I ; 10; 20 2 I0 . The pairs h 1; 2i; h 10; 20i are isomorphic w.r.t. K, written h 1; 2i =K h 10; 20i i { h 1; 2i 2 rI i h 10; 20i 2 rI0 for each r 2 rol(K), { i 2 AI i i0 2 AI0 for i 2 f1; 2g and each A 2 con(K), { i = oI i i0 = oI0 for i 2 f1; 2g and each o 2 nom(K).
We say that I and I0 are isomorphic w.r.t. K, written: I =K I0, if there is a
bijection ' : I ! I0 such that, for each 1; 2 2 I , h 1; 2i =K h'(
If clear from the context, we omit the subscript K of =K and we extend the de nition to forest quasi-interpretations in the obvious way. Forest quasi-models represent, intuitively, an intermediate step between arbitrary models of K and forest models of K.
Since KBs are assumed to be simpli ed, it can be checked locally (by looking at an element of the domain and its direct neighbors) whether an interpretation I is a model of K. We call an element 2 I locally K-consistent if it satis es each GCI in K (a functionality restriction func(f ) is satis ed if has at most one f -neighbor); I is a model of K if each 2 I is locally K-consistent. Deciding whether a quasi interpretation is a model for K cannot be decided locally since nominals impose a global restriction on the cardinality of concepts. Therefore, a quasi interpretation J for K is a model for K if, additionally, for each o 2 nom(K), NoJ is a singleton set. We now show how we can obtain a forest quasi-model from a model of K by using an adapted version of unraveling. De nition 2. Let I be a model for K and choose a function that returns, for a concept C = 9U:B 2 cl(K) and 2 CI some C; 2 I s.t. h ; C; i 2 U I and C; 2 BI . W.l.o.g., we assume that if 2 C1I \ C2I with Ci = 9Ui:Bi 2 cl(K); choose(Ci; ) = i for i 2 f1; 2g and h ; 1i = h ; 2i, then 1 = 2.
An unraveling for some 2 I , denoted #(I; ), is an interpretation obtained from I and as follows: we de ne the set S ( I ) of sequences to be the smallest set such that is a sequence and 1 n n+1 is a sequence, if { 1 n is a sequence, { if n > 2 and h n; n 1i 2 f I for some functional role f , then n+1 6= n 1, { n+1 = choose(C; n) for some C = 9U:B 2 cl(K).
Now x a set F f g IN and a bijection : F ! S such that (i) F is a forest, (ii) ( ; ") = , (iii) if ( ; w); ( ; w c) 2 F with w c a successor of w, then ( ; w c) = ( ; w) n+1 for some n+1 2 I . For each ( ; w) 2 F , set Tail( ; w) = n if f ( ; w) = 1 n. The unraveling for is the interpretation J with J = F and, for each ( ; w) 2 J : (a) for each o 2 nom(K); NoJ = f( ; w) 2 J j Tail( ; w) 2 oI g for No 2 NC a fresh concept name; (b) for each concept name A 2 con(K), ( ; w) 2 AJ i Tail( ; w) 2 AI ; (c) for each role name r 2 rol(K), h( ; w); ( ; w0)i 2 rJ i ( ; w0) is a neighbor of ( ; w), and hTail( ; w); Tail( ; w0)i 2 rI .
Let R I contain each s.t. oI = for some o 2 nom(K). The union of all #(I; ) with 2 R is called an unraveling for I, denoted #(I), where unions of interpretations are de ned in the natural way.
Please note that the function Tail can also be seen as a homomorphism (up to signature extension) from the elements in the unraveling to elements in the original model. Fig. 1b shows the unraveling for our example KB and model. The dotted lines for the non-root elements labeled No indicate that a copy of the whole tree should be appended.
Unravelings are the rst step in the process of transforming an arbitrary model of K into a forest model since the resulting interpretation is a strict forest quasi-model of K.
Lemma 1. Let I be a model of K, then J =#(I) is a strict forest quasi-model for K with branching degree bounded in jcl(K)j.
In the following steps, we traverse a forest quasi-model in an order in which elements with smaller tree depth are always of smaller order than elements with greater tree depth. Elements with the same tree depth are ordered lexicographically. The bounded branching degree of unravelings then guarantees that, after a nite number of steps, we go on to the next level in the forest and process all nodes eventually.
De nition 3. Let be a total order over NI , K a consistent ALCOIF b KB, and J a forest quasi-interpretation for K. We extend the order to elements in
J as follows: let w1 = wp c11 c1n; w2 = wp c21 c2m 2 IN where wp 2 IN is the longest common pre x of w1 and w2, then w1 < w2 if either jw1j < jw2j or both jw1j = jw2j and c11 < c12. For i 2 f1; 2g and ( i; ") 2 J , let oi 2 nom(K) be the smallest nominal such that ( i; ") 2 NoJi . Now ( 1; w1) < ( 2; w2) if either (i) jw1j < jw2j or (ii) jw1j = jw2j and o1 < o2 or (ii) jw1j = jw2j; o1 = o2 and w1 < w2. When collapsing, we create new elements of the form ( w; w0) from ( ; ww0). We extend, therefore, the order as follows: ( 1w1; w10) < ( 2w2; w20) if ( 1; w1w10) < ( 2; w2w20).
During the traversal, we merge nodes such that, nally, all nominal placeholders can be interpreted as singleton sets. To satisfy functionality restrictions, we merge not only nominal placeholders, but also elements that are related to a nominal placeholder by an inverse functional role since, by de nition of the semantics, these elements have to correspond to the same element in a model. In order to identify such elements, we de ne backwards counting paths as follows: De nition 4. Let I be a (quasi) forest model for K. We call p = 1 : : : n a path from 1 to n if, for each i with 1 i < n, h i; i+1i 2 riI for some role ri 2 rol(K). The length jpj of a path p is n 1. We write 1 !U1 2 : : : U!n1 n to denote that h i; i+1i 2 UiI for each 1 i < n. The path p is a descending path if there is some ( ; ") 2 I s.t., for each 1 i n; i = ( ; wi) and, for each 1 i < n; jwij < jwi+1j; p is a backwards counting path (BCP) in I if n 2 oI ( n 2 NoI ) for some o 2 nom(K) and, for each 1 i < n, h i; i+1i 2 fiI for some inverse functional role fi; p is a descending BCP if it is descending and a BCP. Given a BCP p = 1 !f1 2 : : : !fn n+1 with n+1 2 oJ ( n+1 2 NoJ ), we call the sequence f1 fno a path sketch of p.
Please note that ( ; w) is already a descending BCP if ( ; w) 2 oI (NoI ). We now show how we can \collapse" a forest quasi-model into a forest model provided it satis es some admissibility restrictions. During the traversal, we distinguish two situations: (i) we encounter an element ( ; w) that starts a descending BCP and we have not seen another element before that starts a descending BCP with the same path sketch. In this case, we promote ( ; w) to become a new root node of the form ( w; ") and we shift the subtree rooted in ( ; w) with it; (ii) we encounter a node ( ; w) that starts a descending BCP, but we have already seen a node ( 0; w0) that starts a descending BCP with that path sketch and which is now a root of the form ( 0w0; "). In this case, we delete the subtree rooted in ( ; w) and identify ( ; w) with ( 0w0; "). If ( ; w) is an f -successor of its predecessor for some inverse functional role f , we delete all f -successors of ( 0w0; ") and their subtrees in order to satisfy the functionality restriction. We use a notion of collapsing admissibility to characterize models s.t. the the predecessor of ( ; w) satis es the same atomic concepts as the deleted successor of ( 0; w0), which ensures that local consistency is preserved.
De nition 5. Let K0 = nomFree(K) and J be a forest quasi-interpretation for K, then J is collapsing-admissible if there exists a function ch : (cl(K) J ) ! J s.t., for each C = 9U:B 2 cl(K) and 2 CJ , 1. h ; ch(C; )i 2 U J ; ch(C; ) 2 BJ and, if there is no functional role f s.t.
h ; ch(C; )i 2 f J , then ch(C; ) is a successor of , 2. if there is some 0 2 CJ s.t. and 0 start descending BCPs with identical path sketches, then h ; ch(C; )i = h 0; ch(C; 0)i.
We de ne as the smallest equivalence relation on J that satis es 1 2 if 1; 2 start descending BCPs with identical path sketches.
If J is a strict forest quasi-model for K, we call J0 = J an initial collapsing for J and the smallest element ( 0; w0) 2 J0 with w0 6= " that starts a descending BCP the focus of J0. Let Ji be a collapsing for J and ( i; wi) 2 Ji the focus of Ji. We obtain a collapsing Ji+1 for J from Ji with focus ( i+1; wi+1) A r A r A r A r fog E s s s s f g f g
CBE DBE CBE DBE
A r
No E A r
A r
A
r A
r the smallest element starting a descending BCP and ( i+1; wi+1) > ( i; wi) according to the following two cases: 1. There is no element ( ; ") 2 Ji s.t. ( ; ") < ( i; wi) and ( ; ") ( i; wi).
Then Ji+i is obtained from Ji by renaming each element ( i; wiwi0) 2 Ji to ( iwi; wi0). 2. There is an element ( ; ") 2 Ji s.t. ( ; ") < ( i; wi) and ( ; ") ( i; wi).
Let ( ; ") be the smallest such element. (a) Ji+1 = Ji n (f( i; wiwi0) j wi0 2 IN g [ f( ; w) j w = c w0; c 2 IN; w0 2 IN ; ( i; wi) has a predecessor ( i; w0) such that h( i; wi0); ( i; wi)i 2 f Ji i for an inverse functional role f in rol(K) and h( ; c); ( ; ")i 2 f Ji g); (b) for each A 2 con(K); 2 Ji+1 , 2 AJi+1 i 2 AJi ; (c) for each r 2 rol(K); 1; 2 2 Ji+1 , h 1; 2i 2 rJi+1 i (a) h 1; 2i 2 rJi or (b) 1 is the predecessor of ( i; wi) in Ji; 2 = ( ; "), and h 1; ( i; wi)i 2 rJi .
For a collapsing Ji, safe(Ji) is the restriction of Ji to elements ( ; w) s.t. ( ; w) 2 Jj for all j i. With J! we denote the non-disjoint union of all interpretations safe(Ji) obtained from subsequent collapsings Ji for J . The interpretation obtained from J! by interpreting each o 2 nom(K) as ( ; ") 2 NoJ! is denoted by collapse(J ) and called a puri ed interpretation w.r.t. J. If collapse(J ) j= K, we call collapse(J ) a puri ed model of K.
Since, in unravelings, elements that start (desccending) BCPs with identical path sketches have been generated from the same element in the unravelled model, collapsing-admissibility is immediate and the function ch can be de ned using the function choose from the unraveling. Using collapsing-admissibility, we can show that, whenever we delete an element and the subtree rooted in it during the collapsing, the predecessor of the focus is a suitable replacement. Lemma 2. Let J be a strict forest quasi-model for K with branching degree b that is collapsing-admissible. Then collapse(J ) is a forest model for K that still has branching degree b.
By Lemma 1 and since unravelings are collapsing-admissible, we immediately get that collapsing an unraveling yields a forest model with bounded branching degree. At this point, the number of roots might still be in nite and we could have obtained the same result by unraveling an arbitrary model, where we take all elements on BCPs as roots instead of taking just the nominals and creating new roots in the collapsing process. In the next sections, however, we show how we can transform an unraveling of a counter-model for the query such that it remains collapsing-admissible and such that it can in the end be collapsed into a forest model with a nite number of roots that is still a counter model for the query. For this transformation it is much more convenient to work with real trees and forests, which is why we work with strict forest quasi-interpretations. 3
In this section, we provide a characterization for query entailment in forest quasimodels that mirrors query entailment for the corresponding \proper models". In our further argumentation, we talk about the initial part of a tree, i.e., the part that remains if one cuts branches down to a xed length. For a forest interpretation I and some n 2 IN, we denote, therefore, with cutn(I) the interpretation obtained from I by restricting I to those pairs ( ; w) for which jwj n. One can show that, in the case of puri ed models, we nd only nitely many unraveling trees of depth n that \look di erent" (i.e., that are non-isomorphic).
For our further considerations, we introduce the notion of \anchored n-components". These are certain substructures of forest quasi-interpretations that we use to de ne a notion of quasi entailment.
De nition 6. Let J be a forest quasi-interpretation and 2 J . An interpretation C is called anchored n-component of J with witness if C can be created by restricting J to a set W J obtained as follows: { Let J be the subtree of J that is started by and let J ;n := cutn(J ). Select a subset W 0 J ;n that is closed under predecessors. { For every 0 2 W 0, let P be a nite set (possibly empty) of descending BCPs p starting from 0 and let W 0 contain all nodes from all p 2 P . { Set W = W 0 [ S 02W 0 W 0 .
The following de nition and lemma employ the notion of anchored n-components to come up with the notion of quentailment (short for quasi-entailment), a criterion that re ects query-entailment in the world of forest quasi-models. Fig. 2 illustrates this correspondence.
De nition 7. Let J be a forest quasi-model for K and q a CQ with ](q) = n and V = var(q). We say that J quentails q, written J j q, if J contains connected anchored n-components C1; : : : ; C` and there are variable assignment functions i : V ! 2 Ci such that: Q1 For every x 2 V , there is at least one Ci, such that i(x) 6= ; fEog r f (x1) r (x2) r
(x5) r A s
BEC g
A s
BEC (x3) f
A s
BEC (x4) g
A s
BEC C1 A r 1(x1) A r s B C
E f C2 1(x2)
A r 1(sx3) B DE g B C
E f 2(x5) A r s
2(x4) B CE A r s B DE 2(fx3) B DE g B C g B C
E E f B D f
E A r s B D
E A r s B C
E f B D
E
No E No E No E
Q2 For all A(x) 2 q, we have i(x) AJ for some i.
Q3 For every r(x; y) 2 q there is a Ci such that there are 1 2 i(x) and 2 2 i(y) such that h 1; 2i 2 rJ .
Q4 If, for some x 2 V , there are connected anchored n-components Ci and Cj with 2 i(x) and 0 2 j (x), then there is { a sequence Cn1 ; : : : ; Cnk with n1 = i and nk = j and { a sequence 1; : : : ; k with 1 = and k = 0 as well as m 2 nm (x) for all 1 m < k, such that, for every m with 1 m < k, we have that { Cnm contains a descending BCP p1 started by m, { Cnm+1 contains a descending BCP p2 started by m+1, { p1 and p2 have the same path sketch.
Note that an anchored component may contain none, one or several instantiations of a variable x 2 V . Intuitively, the de nition ensures, that we nd matches of query parts which when tted together by identifying BCP-equal elements yield a complete query match.
Lemma 3. For any model I of K, #(I) j q implies I j= q and, for any collapsingadmissible strict forest quasi-model J of K, collapse(J ) j= q implies J j q. 4
One of the major obstacles for a decision procedure for CQ entailment is that for DLs including inverses, nominals, and cardinality restrictions (or alternatively functionality), there are potentially in nitely many new roots. If we want to eliminate new roots such that only nitely many remain, they have to be replaced by \uncritical" elements. We will construct such elements as \environment-limits" { new domain elements which can be approximated with arbitrary precision by A r
A r
A r
A A r
A r s B CE s B DE g B CE A r already present domain elements { possibly without themselves being present in the domain.3 De nition 8. Let I with 2 I be a model of K. A tree interpretation J is said to be generated by , written: J C , if it is isomorphic to the restriction of #(I; ) to elements of f( ; cw) j ( ; cw) 2 #(I; ); c 62 Hg for some H IN. The set of limits of I, written lim I, is the set of all tree interpretations J s.t., for every k 2 IN, there are in nitely many 2 I with cutk(L) = cutk(J ) for some L C .
The right hand side of Fig. 3 displays one limit element of our example model. The following lemma gives some useful properties of limits.
Lemma 4. Let K0 = nomFree(K), I a puri ed model of K, and n some xed natural number. Then the following hold: 1. Let L0 be a tree interpretation such that there are in nitely many 2 I with L0 = cutn(L) for some L C . Then, there is at least one limit J 2 lim I such that cutn(J ) = L0. 2. Every J 2 lim I is locally K0-consistent apart from its root ( ; "). 3. For every J 2 lim I, every root ( ; ") in J has no BCP to any ( ; w) 2 J . 4. Every J 2 lim I is collapsing-admissible.
Having de ned and justi ed limit elements as convenient building blocks for restructuring forest quasi-interpretations, the following de nition states how this restructuring is carried out.
De nition 9. Let I be a model for K and J some forest quasi-model for K with 2 J . A strict tree quasi-interpretation J 0 2 lim I is called an n-secure replacement for if (i) cutn(#(J ; )) is isomorphic to cutn(J 0) and (ii) for every anchored n-component of J 0 with witness 0, there is an isomorphic anchored n-component of J with witness . If 2 J has an n-secure replacement in lim I, is n-replaceable w.r.t. I and it is n-irreplaceable w.r.t. I otherwise. 3 As an analogy, consider the fact that any real number can be approximated by a sequence of rational numbers, even if it is itself irrational.
A r
For J =#(I), an interpretation J 0 is called an n-secure transformation of J if it is obtained by (possibly in nitely) repeating the following step:
Choose one unvisited w.r.t. tree-depth minimal node ( ; w) that is n-replaceable w.r.t. I. Replace ( ; w) with one of its n-secure replacements from lim I and mark ( ; w) as visited. Lemma 5. Every puri ed model I of K contains only nitely many distinct elements that start a BCP and are the cause for n-irreplaceable nodes in the unraveling of I.
Next, we can show that the process of unraveling, n-secure transformation and collapsing preserves the property of being a model of a knowledge base and (with the right choice of n) also preserves the property of not entailing a conjunctive query. Moreover, this model conversion process ensures that the resulting model contains only nitely many new nominals (witnessed by a bound on the length of BCPs). Fig. 4b illustrates these properties for our example model. Note that only two new nominals are left whereas collapsing the original unraveling yields in nitely many.
Lemma 6. Let I be a puri ed model of K, J =#(I), and J 0 an n-secure transformation of J . Then the following hold:
Now we are able to establish our rst milestone on the way to showing nite representability of countermodels.
Theorem 1. For every ALCOIF b KB K and CQ q s.t. K 6j= q, there is a forest model I of K with nitely many roots and bounded branching degree s.t. I 6j= q. 5
We can now use standard techniques from tableau algorithms (adapted to work on models) to construct nite representations for a forest model of K with nitly many roots. In particular the tableau algorithm with n-tree-blocking, n ](q), for deciding CQ entailment in SHIQ, SHOQ, and SHOI with only simple roles in the query [5, 6] works exactly like that. We call an interpretation on which we applied n-tree-blocking and discarded all blocked elements an n-representation. Such an n-representation corresponds to a complete and clash-free completion graph in tableau algorithms. Since we xed a bound on the number of roots in Theorem 1 and otherwise only consider the closure cl(K) of K, one can show that there are only nitely many non-isomorphic n-blocking-trees even though we take links back to roots into account. Similarly, we can now use an adapted version of the technique for building a tableau from a complete and clash-free completion graph to show that we can obtain a model for K from an n-representation. Lemma 7. Let n ](q). If K 6j= q, then there is an n-representation R of K s.t. R 6j= q, and from R one can build a model I of K such that I 6j= q.
Thus, we can enumerate all ( nite) n-representations for K and check whether they entail q. Together with the semi-decidability result for FOL [4], we get the desired theorem.
Theorem 2. It is decidable whether K j= q for K an ALCOIF b knowledge base and q a Boolean conjunctive query.
This solves the long-standing open problem of deciding conjunctive query entailment in the presence of nominals, inverse roles, and quali ed number restrictions. Since the approach is purely a decision procedure, the computational complexity of the problem remains open and will be part of our future work. Similarly, we will embark on extending our results to SHOIQ with non-simple roles as query predicates.
Acknowledgements. Sebastian Rudolph was supported by a scholarship of the German Academic Exchange Service (DAAD) and Birte Glimm is funded by the EPSRC project HermiT: Reasoning with Large Ontologies.