Berman and Paterson proved that Test-Free PDL is weaker than PDL. As the description logics ALCtrans and ALCreg are, respectively, variants of Test-Free PDL and PDL, there is a concept of ALCreg that is not equivalent to any concept of ALCtrans. Generalizing this, we show that there is a concept of ALCreg that is not equivalent to any concept of the logic that extends ALCtrans with inverse roles, nominals, quali ed number restrictions, the universal role and local re exivity of roles. We also provide some results for the case with RBoxes and TBoxes. One of them states that tests can be eliminated from TBoxes of the deterministic Horn fragment of ALCreg.
Propositional Dynamic Logic (PDL) is a well-known modal logic for reasoning
about computer programs [
Generalizing the result and method of Berman and Paterson, in Section 3 we
prove that there is a concept of ALCreg that is not equivalent to any concept
of the DL ALCIOQU Selftrans, which extends ALCtrans with inverse roles (I),
nominals (O), quali ed number restrictions (Q), the universal role (U ) and local
re exivity of roles (Self ) as of the DL SROIQ [
In Section 4, we provide a result stating that using regular RBoxes and acyclic TBoxes for ALCIOQU Selftrans does not help in expressing tests, but using simple strati ed TBoxes under the strati ed semantics on the background allows us to express every concept by another without tests. A further result states that tests can be eliminated from TBoxes of the deterministic Horn fragment of ALCreg. This suggests that tests can be eliminated from tractable1 Horn fragments of PDL-like logics. 2
This section provides notions and de nitions related with syntax and semantics
of DLs [
Let fI; O; Q; U ; Self g, where the symbols mean inverse roles, nominals, quali ed number restrictions, the universal role and local re exivity of roles, respectively. Roles and concepts of the DLs ALC, ALC + , (ALC + )trans and (ALC + )reg are de ned as follows.
If L = ALC, then: { if r 2 R+, then r is a role of L, { if A 2 C, then A is a concept of L, { > and ? are concepts of L, { if C and D are concepts of L and R is a role of L,
then :C, C t D, C u D, 9R:C and 8R:C are concepts of L.
If L = ALC + , then additionally: { if I 2 and R is a role of L, then R is a role of L, { if O 2 and a 2 I, then fag is a concept of L, { if Q 2 , n 2 N, C is a concept of L, R is a simple role of L (i.e., a simple role that is a role of L), then n R:C and n R:C are concepts of L, { if U 2 , then U is a role of L, { if Self 2 and r 2 R+, then 9r:Self is a concept of L.
If L = (ALC + )trans, then additionally: { " is a role of L, { if R and S are roles of L and are di erent from U ,
then R t S, R S and R are roles of L. 1 I.e., with a PTime or lower data complexity. I n CI ng ng
RI = (RI ) 1 "I = fhx; xi j x 2 (R S)I = RI SI (R t S)I = RI [ SI (R )I = (RI )
I g (C?)I = fhx; xi j x 2 CI g U I = I I A nite set S of context-free production rules over R is called a context-free semiThue system over R. It is symmetric if R ! Sk : : : S1 belongs to S for every production rule R ! S1 : : : Sk of S.2 It is regular if the language consisting of words derivable from any R 2 R is regular. Assume that R is derivable from itself. 2 If k = 0, then the RHS (right hand side) of each of the rules represents the empty word ".
A role inclusion axiom (RIA) has the form S1 Sk v R, where k 0 and S1; : : : ; Sk; R are basic roles. If k = 0, then the LHS (left hand side) of the inclusion stands for ".
A (regular) RBox is a nite set R of RIAs such that S = fR ! S1 : : : Sk j (S1 Sk v R) 2 Rg is a regular and symmetric semi-Thue system with the property that only " and words with length 1 can be derived from any simple role R 2 R. An RBox is allowed for a DL L if it uses inverse roles only when they are allowed for L. Since it is undecidable whether a context-free semi-Thue system is regular, we assume that each RBox R is accompanied by a mapping
R that associates each R 2 R with a regular expression R(R) that generates the set of words derivable from R using the rules of the corresponding semi-Thue system.
If S1 Sk v R is a RIA of R, then we call R an intensional predicate speci ed by R. An interpretation I validates a RIA S1 Sk v R if (S1 Sk)I RI . It is a model of an RBox R if it validates all RIAs of R. 2.2
TBoxes A TBox axiom (or terminological axiom) is either a general concept inclusion : : (GCI) C v D or a concept equivalence C = D. A concept equivalence A = D (where A 2 C) is called a concept de nition. A TBox is a nite set of TBox axioms. It is allowed for a D L: L if it uses only concepts of L. An interpretation I validates C v D (resp. C = D) if CI DI (resp. CI = DI ). It is a model of a TBox T if it validates all axioms of T .
A TBox T is acyclic if there exist concept names A1; : : : ; An: such that T consists of n axioms and the i-th axiom of T is of the form Ai = C, C v Ai or Ai v C, where C does not use the concept names Ai; : : : ; An. The concept names A1; : : : ; An are called intensional predicates speci ed by T .
A TBox T is called a simple strati ed TBox if there exists a partition (T1; : : : ; Tn) of T , called a strati cation of T , such that, for each 1 i n, Ti = fCi;j v Ai;j j 1 j nig, where each Ai;j is a concept name that does not occur in T1; : : : ; Ti 1 and may occur at the LHS of v in the axioms of Ti only under the scope of u, t and 9. The concept names Ai;j , for 1 i n and 1 j ni, are called intensional predicates speci ed by T .
Note that negation (:) is allowed at the LHS of v in GCIs of a simple strati ed TBox, but it can be applied only to concepts that do not use the predicates de ned in the current or later strata. 3
In this section, we prove the following theorem: Theorem 1. There is no alent to the concept C = 9((r A?) r (:A)? r concept of ALCIOQU Selftrans
C = 9((r A?) r B? r A?):> A?):> of ALCreg.
To prove this theorem we will use a family of interpretations Im = h Im ; Im i, m > 1, illustrated and speci ed as follows: w1 r / B A r / wm 1 r / wm r / wm+1 r /
A B A w0
r B ^== == r =w 1
A o r o r w m+1
A o r w m
B o r w m 1
A o r o r w 2m+1
A o r w 2m
B
{ Im = fw 2m; w 2m+1; : : : ; w2mg,
{ rIm = fhwi; wi+1i; hw2m; w 2mi j 2m
{ sIm = ; for s 2 R+ frg,
{ BIm = fw 2m; w m; w0; wm; w2mg,
{ AIm = Im BIm ,
{ CIm = ; for C 2 C fA; Bg,
{ aIm = w2m for a 2 I.
i < 2mg,
Note that j Im j = 4m + 1. Comparing Im with the structure Am used in [
Observe that, for C being one of the two concepts mentioned in Theorem 1, w0 2 CIm but wm 2= CIm . The structure of the proof of Theorem 1 is as follows. Given any concept D of ALCIOQU Selftrans, we rst transform it to a concept D2 of ALCIOtrans over the signature fr; A; B; ag such that D2Im = DIm for all m > 1 (see Lemma 1). We then transform D2 to a concept D3 such that D3Im = D2Im for all m > 1, the operator is used only for rn and rn for some n (see Lemma 2), and for every subconcept 9R:D30 or 8R:D30 of D3, R is of the form r, r, (rn) or (rn) for some n 1 (see Lemma 3). Next, we show that there exists m > 1 such that w0 2 D3Im , wm 2 D3Im (see Lemma 4). Thus, for that m, CIm 6= D3Im , and therefore, C is not equivalent to D (since D3Im = D2Im = DIm ).
Lemma 1. For any concept C of ALCIOQU Selftrans, there exists a concept D of ALCIOtrans over the signature fr; A; B; ag such that DIm = CIm for all m > 1.
Proof. Let D be the concept obtained from C by:
{ replacing every subconcept n R:E, where n 1 R:E by 9R:E, 0 R:E by >, n R:E, where n 2, by ?, 1, by >,
0 R:E by 8R::E, 9U:E by 9r :E, 8U:E by 8r :E, 9R:Self by ?, { replacing every concept name di erent from A and B by ?, { replacing every nominal fbg, where b 6= a, by fag, { replacing every role name s di erent from r by ;, { repeatedly replacing every role ; t R or R t ; by R, every role ; by ", and every role ;, ; R or R ; by ;, { replacing every subconcept 9;:E by ?, and every 8;:E by >. It is easy to see that D satis es the properties mentioned in the lemma.
We treat a word R1 : : : Rk over the alphabet fr; rg as the role R1 Rk, and by Rn we denote the composition of n copies of R. Thus, R0 = ". Conversely, a role R without tests that uses only basic roles r and r is treated as a regular expression over the alphabet fr; rg (where t stands for [, and for ;). For such a role R, by L(R) we denote the regular language generated by R. For a word R over the alphabet fr; rg, by jRj we denote the length of R (de ned in the usual way), and by jjRjj we denote the norm of R, which is de ned as follows: jj"jj = 0, jjrjj = 1, jjrjj = 1, jjRSjj = jjRjj + jjSjj. Observe that, for words R and S over the alphabet fr; rg, if jjRjj = jjSjj, then RIm = SIm for all m > 1. Lemma 2. Let R be a role without tests that uses only basic roles r and r. Then, there exists a role S such that SIm = RIm for all m > 1 and the operator can be used in S only for rn and rn for some n.
Proof. Since L(R) is a regular language, by the pumping lemma, there exists an integer p > 0 such that every word from L(R) of length at least p can be represented as xyz such that jyj > 0, jxyj p and xyiz 2 L(R) for all i 0.
Let n = p(p 1) 2 1 and let L0 be the language obtained from L(R) by deleting all words y such that there exists x 2 L(R) with jxj < jyj and jjxjj = jjyjj. By pumping(x; y; z) we denote the formula xyz 2 L0 ^ jyj > 0 ^ jxyj p ^ 8i 0 xyiz 2 L(R): Observe that, if w0 = xyz 2 L0 and pumping(x; y; z) holds, then: { jjyjj 6= 0 because otherwise we would have xz 2 L(R), jxzj < jw0j and jjxzjj = jjw0jj, which contradict the de nition of L0; { if jjyjj > 0 then, for all i 0, there exists u 2 L(R) with jjujj = jjw0(rn)ijj; { if jjyjj < 0 then, for all i 0, there exists u 2 L(R) with jjujj = jjw0(rn)ijj. Denote this observation by (?). For each integer j, 0 j < n, let Kj+ = fjjxyzjj : pumping(x; y; z); n j (jjxyzjj Kj = fjjxyzjj : pumping(x; y; z); n j (jjxyzjj j) and jjyjj > 0g j) and jjyjj < 0g: For intuition, informally, we intend to de ne S to be the role
G S1 t ((G S2) (rn) ) t ((G S3) (rn) ); (1) where S1, S2 and S3 are the nite sets of words over the alphabet fr; rg constructed as follows: { S1 := fx 2 L0 : jxj < pg, S2 := ;, S3 := ;; { for each j from 0 to n 1 do if K+ = ; then
j 6 - if Kj+ does not have a minimum then add rj to both S2 and S3; - else: let k = min Kj+, if k 0 then S2 := S2 [ frkg else S2 := S2 [ f(r) kg (for this second case, notice that k is a positive integer); if Kj 6= ; then - if Kj does not have a maximum then add rj to both S2 and S3; - else: let k = max Kj , if k 0 then S3 := S3 [ frkg else S3 :=
S3 [ f(r) kg.
Formally, we de ne S to be the role obtained from (1) by deleting any i-th main disjunct such that Si is empty, for i 2 f1; 2; 3g. To prove that SIm = RIm for all m > 1 it is su cient to show that: 1. if w 2 L(S), then there exists u 2 L(R) such that jjujj = jjwjj, 2. if w 2 L(R), then there exists u 2 L(S) such that jjujj = jjwjj.
Consider the assertion (1) and let w 2 L(S). There are the following cases: { Case w 2 S1: We have that w 2 L0 L(R). Just take u = w. { Case w = rj(rn)h, Kj+ 6= ; and Kj+ does not have a minimum: Thus, there exists w0 = xyz 2 L0 such that pumping(x; y; z) holds, jjyjj > 0 and jjw0jj = j + n h0 for some h0 < h. By (?), there exists u 2 L(R) such that jjujj = jjwjj. { Case w = rk(rn)h, Kj+ 6= ;, k = min Kj+ and k 0: Thus, there exists w0 = xyz 2 L0 such that pumping(x; y; z) holds, jjyjj > 0 and jjw0jj = k.
By (?), there exists u 2 L(R) such that jjujj = jjwjj. { Case w = (r) k(rn)h, K+ = ;, k = min K+ and k < 0: Thus, there exists j 6 j xyz 2 L0 such that pumping(x; y; z) holds, jjyjj > 0 and jjw0jj = k. Notice that jj(r) kjj = k. By (?), there exists u 2 L(R) such that jjujj = jjwjj. { Case w = rj(rn)h, Kj 6= ; and Kj does not have a maximum: Thus, there exists w0 = xyz 2 L0 such that pumping(x; y; z) holds, jjyjj < 0 and jjw0jj = j + n h0 for some h0 > h. By (?), there exists u 2 L(R) such that jjujj = jjwjj. { The four previous cases are related to S2. The four remaining cases, which are related to S3, can be dealt with in a similar way.
Consider the assertion (2) and let w 2 L(R). There exists w0 2 L0 such that jjw0jj = jjwjj. If jw0j < p, then w0 2 S1 and we can just take u = w0. Suppose jw0j p. Thus, w0 can be represented as xyz such that pumping(x; y; z) holds. There are the following cases: { Case jjyjj > 0: There exists 0 j < n such that jjw0jj 2 Kj+ and jjw0jj = j + n i for some integer i. Consider the following subcases.
Case Kj+ does not have a minimum: Thus, rj 2 S2. Taking u = rj(rn)i, we have that u 2 L(S) and jjujj = jjw0jj = jjwjj.
Case k = min Kj+ and k 0: Thus, rk 2 S2. Observe that jjw0jj k k). Taking u = rjjw0jj, we have that u 2 L(S) and jjujj = and n j (jjw0jj jjw0jj = jjwjj.
Case k = min Kj+ and k < 0: Thus, (r) k 2 S2. Observe that jjw0jj k and n j (jjw0jj k). Taking u = (r) k(rjjw0jj k), we have that u 2 L(S) and jjujj = jjw0jj = jjwjj. { The case when jjyjj < 0 is dual to the above case and can be dealt with analogously.
Let C denote the set of concepts C of ALCIOtrans over the signature fr; A; B; ag such that, for every subconcept 9R:D or 8R:D of C, R is of the form r, r, (rn) or (rn) for some n 1.
Lemma 3. For any concept C of ALCIOtrans over the signature fr; A; B; ag, there exists a concept D 2 C such that DIm = CIm for all m > 1. Proof. Let E be the concept obtained from C by replacing every role R by a role S that satis es the conditions mentioned in Lemma 2. We have EIm = CIm for all m > 1. Then, let D be obtained from E by repeatedly applying the following transformations: It is clear that D 2 C and DIm = EIm = CIm for all m > 1.
For a concept C 2 C, by nr(C) we denote the number of occurrences of 9r, 9r, 8r and 8r in C.
Lemma 4. For any concept C 2 C and integers m and k such that m > 1, 4m + 1 is prime and nr(C) < m jkj, we have wk 2 CIm , wk+m 2 CIm . Proof. This proof is similar to the one of [2, Lemma 3]. The intuition is as follows: { a concept C0 can distinguish wk and wk+m only if nr(C0) is large enough so that the checking can recognize that the neighborhood of wk di ers from the corresponding neighborhood of wk+m, in particular, to recognize that the rst one contains wm+1 (resp. w m 1) and the second one contains w 2m (resp. w2m); the reason is that, since 4m + 1 is prime, either ((rn) )Im =
Im Im or hwi; wji 2 ((rn) )Im i j = i; { since nr(C) < m jkj, C cannot distinguish wk and wk+m.
Observe that m < k < m. We prove this lemma by induction on the structure of C. The cases when C is A, B, > or ? are trivial. The cases when C is of the form D u E or 8R:D are reduced to the cases of :(:D t :E) and :9R::D, respectively.
{ Case C = fag: Since aIm = w2m, wk 2= CIm and wk+m 2= CIm . { Case C = :D: We have nr(D) = nr(C). By induction, wk 2 DIm , wk+m 2
DIm , and hence, wk 2 CIm , wk+m 2 CIm . { Case C = D tE: We have nr(D) nr(C) and nr(E) nr(C). By induction, wk 2 DIm , wk+m 2 DIm and wk 2 EIm , wk+m 2 EIm , which imply that wk 2 CIm , wk+m 2 CIm . { Case C = 9r:D: We have nr(D) = nr(C) 1 < m jkj 1 m jk + 1j.
By induction, wk+1 2 DIm , wk+1+m 2 DIm . Hence, wk 2 (9r:D)Im , wk+m 2 (9r:D)Im , which means wk 2 CIm , wk+m 2 CIm . { Case C = 9r:D: We have nr(D) = nr(C) 1 < m jkj 1 m jk 1j.
By induction, wk 1 2 DIm , wk 1+m 2 DIm . Similarly to the previous case, this implies that wk 2 (9r:D)Im , wk+m 2 (9r:D)Im , which means { Case C = 9,(rnw)k+:Dm 2anCdI(m4m. + 1)jn : We have hwi; wji 2 ((rn) )Im i j = i. wk 2 CIm Hence,
wk 2 (9(rn) :D)Im , wk 2 DIm wk+m 2 (9(rn) :D)Im , wk+m 2 DIm : We have nr(D) = nr(C). By induction, wk 2 DIm , wk+m 2 DIm . Therefore, wk 2 CIm , wk+m 2 CIm . { Case C = 9(rn) :D and (4m + 1)6 j n : Since 4m + 1 is prime, 0; n; 2n; 3n; : : : ; (4m)n have all 4m + 1 di erent residues modulo 4m + 1. Hence, hwi; wji 2 ((rn) )Im for all wi; wj 2 Im , and
wk 2 (9(rn) :D)Im , wk+m 2 (9(rn) :D)Im ; because they are both equivalent to that there exists wj 2 DIm . Therefore, wk 2 CIm , wk+m 2 CIm : { The case C = 9(rn) :D is similar to the two previous cases.
We now recall and prove Theorem 1.
Theorem 1 alent to C = 9((r A?)
There is no concept of the concept C = 9((r A?) r (:A)? r A?):> of ALCreg.
ALCIOQU Selftrans r B? r A?):> Proof. For a contradiction, suppose D is a concept of ALCIOQU Selftrans equivalent to C. By Lemma 1, there exists a concept D2 of ALCIOtrans over the signature fr; A; B; ag such that D2Im = DIm for all m > 1. By Lemma 3, there exists a concept D3 2 C such that D3Im = D2Im for all m > 1. Let m be an integer such that m > nr(D3) and 4m + 1 is prime. By Lemma 4, w0 2 D3Im , wm 2 D3Im . This contradicts the facts that D3Im = D2Im = DIm = CIm , w0 2 CIm and wm 2= CIm . Corollary 1. For any fI; O; Q; U ; Self g, (ALC + )trans is weaker than (ALC + )reg in expressing concepts. 4
The result of the previous section roughly states that, without using RBoxes and
TBoxes, it is hard to eliminate tests, at least it is impossible to eliminate tests
from ALCIOQU Selfreg without decreasing the expressive power. As expected,
using acyclic TBoxes that consist only of concept de nitions do not help in
expressing tests. The rst result of this section states that using RBoxes and
acyclic TBoxes that are de ned more liberally as in Section 2 does not help either.
The second result states that, however, using simple strati ed TBoxes under the
strati ed semantics on the background, it is possible to express every concept by
another without tests. The third result states that tests can be eliminated from
the deterministic Horn fragment of ALCreg. Due to the lack of space, proofs of
these results are provided only in the long version [
The Case with RBoxes and Acyclic TBoxes We say that a concept C is inexpressible in a DL L even when using RBoxes and acyclic TBoxes if, for every concept D, every RBox R and every acyclic TBox T of L such that the intensional predicates speci ed by R and T do not occur in C, there exists a model I of R and T such that CI 6= DI .
Proposition 1. The concept C = 9((r A?) r B? r A?):> C = 9((r A?) r (:A)? r A?):> of ALCreg is inexpressible ALCIOQU Selftrans even when using RBoxes and acyclic TBoxes. or in 4.2
Eliminating Tests from Concepts by Simple Strati ed TBoxes Let T be a simple strati ed TBox. An interpretation I is called a standard model of T (under the strati ed semantics) if there exist a partition (T1; : : : ; Tn) of T and interpretations J0; : : : ; Jn such that: { Ti = fCi;j v Ai;j j 1 j nig for 1 i { Jn = I and Ji = I for all 0 i < n, { xJ0 = xI for all x 2 fAi;j j 1 i { for each 1 i n, xJi = xJi 1 for all x 2 and AiJ;ji , for 1 j n, n and 1
j fAi0;j j i n; 1 j ni0 g ni, are the smallest subsets of Ji such that AiJ;ji = CiJ;ji .
nig, i0 It can be shown that, for every interpretation J0, there exists a unique standard model I of T such that I = J0 and xI = xJ0 for all x 2 fAi;j j 1 i n and 1 j nig. We call it the standard model of T based on J0.
In what follows, let fI; O; Q; U ; Self g (in general, extending with other features does not a ect Proposition 2 given below). Let C be a concept of (ALC + )reg, D a concept and T a simple strati ed TBox of (ALC + )trans such that the intensional predicates speci ed by T do not occur in C. We say that C is expressed by D and T under the strati ed semantics if, for every standard model I of T , CI = DI.
Proposition 2. Every concept of (ALC + )reg can be expressed by a concept and a simple strati ed TBox of (ALC + )trans under the strati ed semantics. The previous subsection deals with eliminating tests from a standing alone concept by using a simple strati ed TBox under the strati ed semantics. Roughly speaking, it suggests that tests in PDL-like roles can be eliminated by using xpoints outside roles. The result of this subsection states that tests can be eliminated from TBoxes of the deterministic Horn fragment of ALCreg. This is possible because the traditional semantics of such TBoxes has a xpoint characterization.
A role can be treated as a regular expression over the alphabet R+[fC? j C is a conceptg, where t and stand for [ and semicolon, respectively. Conversely, a word over this alphabet can be treated as a role. Given a role R, let L(R) denote the regular language generated by R and let 89R:C be a new concept constructor whose semantics in an interpretation I is speci ed as follows: (89R:C)I = \f(8S:9S0:C)I j SS0 2 L(R)g: Observe that, if R 2 R+, then 89R:C 8R:C u 9R:C.
The deterministic Horn fragment of ALCreg, denoted by D-Horn-ALCreg, is designed with the intention to be (probably) the most expressive fragment of ALCreg that has a PTime data complexity (under the traditional semantics).
A D-Horn-ALCreg TBox axiom is an expression of the form Cl v Cr, where Cl and Cr are concepts de ned by the following BNF grammar, with A 2 C and s 2 R+:
Cl ::= > j A j Cl u Cl j Cl t Cl j 9Rl:Cl j 89Rl:Cl Rl ::= s j Rl Rl j Rl t Rl j Rl j Cl? Cr ::= > j ? j A j :Cl j Cr u Cr j :Cl t Cr j 9Rr:Cr j 8Rl:Cr Rr ::= s j Rr Rr j Cr? (2) (3) (4) (5)
A D-Horn-ALCreg TBox is a nite set of D-Horn-ALCreg TBox axioms. Remark 1. A (reduced) ABox is a nite set of assertions of the form A(a), :A(a) or r(a; b) (where A 2 C and r 2 R+). A knowledge base in D-Horn-ALCreg is a pair hT ; Ai consisting of a D-Horn-ALCreg TBox T and an ABox A. The notion of whether an interpretation is a model of an ABox or a knowledge base is de ned in the usual way. A knowledge base is satis able if it has a model. It can be proved that checking whether a given knowledge base hT ; Ai in D-Horn-ALCreg is satis able is solvable in polynomial time in the size of the ABox A.3 That is, D-Horn-ALCreg has a PTime data complexity. If 89 in (2) is replaced by 8, then instead of D-Horn-ALCreg we obtain the general Horn fragment of ALCreg with a NP-hard data complexity for the satis ability problem.4
The following theorem D-Horn-ALCreg.
states that tests can be eliminated from Theorem 2. For every D-Horn-ALCreg TBox T over a signature ists a D-Horn-ALCreg TBox T 0 without tests over a signature that: 0 1. for every model I of T , there exists a model I0 of T 0 such that and xI = xI0 for all x 2 , 2. for every model I0 of T 0, the interpretation I over speci ed by and xI = xI0 for all x 2 is a model of T .
I = I =
I0 I0 5
Generalizing the result and method of Berman and Paterson [
The other results of this paper state that, on the other hand, using simple
strati ed TBoxes under the strati ed semantics on the background, it is
possible to express every concept by another without tests. Furthermore, tests can
be eliminated from the deterministic Horn fragment D-Horn-ALCreg of ALCreg.
If one extends D-Horn-ALCreg with other features (e.g., I, O, Q, U and Self )
appropriately so that the resulting language still has a PTime data complexity
(cf. Horn-SHIQ [
D-Horn-ALCreg with inverse roles and regular RBoxes.
4 The hardness was shown for the general Horn fragment of ALC [