We consider the problem of characterising relational constraints under which TBox reasoning in EL is tractable. We obtain P vs. coNP-hardness dichotomies for tabular constraints and constraints imposed on a single re exive role. In recent years, the problem of describing role boxes (aka relational constraints) under which reasoning is within a given complexity class has become an important research topic in description logic (DL). For example, the development of SROIQ from SHIQ has mainly been driven by the desire to allow for more expressive relational constraints for which reasoning is still decidable and tableau decision procedures can be developed. As a result, in SROIQ one can express, among others, role inclusions of the form r s v r and s r v r, re exivity, transitivity and symmetry of roles [6, 7]. For E L, underlying the OWL 2 EL pro le of the OWL 2 Web Ontology Language, the complexity of reasoning under relational constraints was investigated in [1, 2, 9]. For example, the subsumption problem for general TBoxes in E L is tractable for any nite set of constraints of the form r1(x1; x2) ^
^ rn(xn; xn+1) ! rn+1(x1; xn+1)
(1)
(the order of the variables is essential). On the other hand, subsumption becomes
ExpTime-complete in the presence of symmetry or functionality constraints [
The aim of this paper is to take a fresh look at how relational constraints in uence the complexity of DL reasoning: rather than putting forward a new class of role boxes for which reasoning is decidable or within a certain complexity class, we attempt to classify relational constraints according to whether they lead to decidable or undecidable reasoning problems, or to reasoning within a given complexity bound. The ultimate aim of this approach is to obtain a complete map of how relational constraints determine the complexity of reasoning for most important DLs. Apart from its theoretical interest, such a map can also be used for the selection of role boxes with acceptable computational properties in future standardisation e orts.
In this paper, which extends [
Our initial ndings indicate that informative dichotomy results on P versus coNP-hardness can indeed be obtained. For example, we show that (d1) there are only four universal constraints on a single re exive role r under which E L TBox reasoning is in P: (1) r is arbitrary, (2) the domain of r is a singleton, (3) r is transitive, (4) r is an equivalence relation. All other universal constraints are either invisible to E L TBox reasoning or lead to coNP-hard E L subsumption.
Here, by `invisibility' we understand the following. It is well known that many relational constraints do not in uence|or are invisible to|TBox reasoning: for example, for E L (and even ALC), TBox reasoning over irre exive relations coincides with TBox reasoning over arbitrary relations, and similarly for the class of nite and tree-like relational structures. In fact, one can use dichotomy (d1) to show that there are uncountably many `visible' universal relational constraints on a single re exive role for which E L subsumption is coNP-hard, but only four `visible' universal constraints for which E L subsumption is in P.
Another dichotomy we prove in this paper is as follows:
(d2) Consider an arbitrary relational constraint (over a nite number of roles)
such that the size of the domain of all interpretations satisfying this
constraint is bounded by some natural number n > 0. Then E L subsumption
over the interpretations satisfying the constraint is in P if all roles in those
interpretations are functional. Otherwise E L subsumption is coNP-complete.
Currently, not much is known about dichotomies for more expressive languages.
We note, however, recent work on an NP vs. PSpace dichotomy for satis ability
of classical modal formulas over frame classes de nable by Horn sentences [
The paper is structured as follows. In Section 2, we de ne the extension E L? of E L with the concept ? and all the model-theoretic notions we need. We prove our results for E L? rather than E L and show, by a straightforward reduction in Section 6, that they hold for E L as well. In Section 3, we consider the relation between tractability and convexity (the disjunction property) and prove two general su cient conditions for non-tractability. Then, in Sections 4 and 5, we prove the dichotomies (d1) and (d2) mentioned above. 2
Fix two disjoint countably in nite sets NC of concept names and NR of role names. We use arbitrary concept names in NC for constructing concepts, but may restrict the set of available role names to some R NR. Throughout this paper, we work with E L extended with the concept ?, denoting the empty set. Thus, for R NR, the E L?-concepts C over R are de ned inductively as follows: C ::= > j ? j
A j
C1 u C2 j 9r:C; where A 2 NC, r 2 R and C; C1; C2 range over E L?-concepts over R. An RTBox is a nite set of concept inclusions (CIs) C v D, where C and D are E L?-concepts over R. An R-interpretation is of the form I = ( I ; I ), where
I 6= ; and I is an interpretation function for concept names and role names in R. Complex concepts over R are interpreted in I as usual. If CI DI , we say that I satis es C v D and write I j= C v D. I is a model of an R-TBox T , I j= T in symbols, if it satis es all the CIs in T .
We now de ne what we understand by relational constraints on interpretations. An R-frame is a structure F = ( F; F) where F 6= ; and F is a map associating with each r 2 R a relation rF F F. We say that an Rinterpretation I is based on an R-frame F if I = F and rI = rF for all r 2 R. An R-constraint is any class K of R-frames closed under isomorphic copies. For example, a constraint for R = fr1; r2; r3g can consist of all R-frames F = ( F; F) with arbitrary r1F, transitive r2F and functional r3F. An interpretation I satis es an R-constraint K if I is based on some F 2 K.
The subsumption problem for an R-constraint K is to decide, given an RTBox T and two concepts C, D over R, whether I j= C v D for every model I of T based on an R-frame in K, in which case we write T j=K C v D. For singleton K = fFg, we sometimes write T j=F C v D.
+ of E L? [
F j= 8x1 : : : 8xn+1 r1(x1; x2) ^
for all r1 rn v rn+1 in R. According to [
We say that R-constraints K1 and K2 are TBox-equivalent (in E L?) if we have T j=K1 C v D i T j=K2 C v D, for all R-TBoxes T and E L?-concepts C, D over R. For example, as is well-known, the class of all frames is TBox equivalent to the class of all irre exive frames, and to the class of all nite frames. For an R-constraint K, we denote by FrThK the union of all those R-constraints that are TBox equivalent in E L? to K. FrThK and K are TBox equivalent in E L?, and FrThK is the largest class that is TBox equivalent in E L? to K.
An R-constraint K is TBox-de nable (in E L?) if there exists a set of pairs (T ; C v D), where T is an R-TBox and C; D are E L?-concepts over R, such that K = fF j T j=F C v D; for all (T ; C v D) 2 g. Thus, K is TBox-de nable i K = FrThK, and any class of TBox-equivalent constraints contains exactly one TBox-de nable class. In a similar way we can de ne TBox-de nable classes of R-constraints for E L and more expressive DLs, say ALC.
A universal R-constraint is a class of R-frames de nable by universal
rstorder sentences in the signature R. Equivalently, by [
NR. Then We conjecture that Theorem 1 can be generalised to arbitrary (not necessarily rst-order de nable) classes of R-frames closed under subframes. Note that, without the subframe condition, there are classes of frames that are TBox-de nable in ALC but not in E L?. One example is the Church-Rosser property 8x; y1; y2 r(x; y1) ^ r(x; y2) ! 9z(r(y1; z) ^ r(y2; z)) : 3
In this section, we investigate the relationship between convexity (sometimes also called the disjunction property) and tractability. To this end, we need (formally not allowed in E L?) concepts of the form C t D, where C and D are E L?concepts, which are interpreted in the obvious way by the union of the extensions of the disjuncts C and D. An R-constraint K is said to be convex if, for any RTBox T and E L?-concepts F , C, D over R, (conv) if
T j=K F v C t D then
T j=K F v C or
T j=K F v D.
Although convexity is closely related to tractability, they do not imply each
other. It is readily checked that every relational constraint K de ned by Horn
sentences is convex. Thus, symmetry and functionality are examples of relational
constraints that are convex but non-tractable [
We now prove two general conditions, based on non-convexity, that imply
nontractability. The proofs of coNP-hardness are by reduction of the following set
splitting problem, which is known to be NP-complete [
Proof. Consider T , F , C and D over R for which T j=K F v C t D, and there exist an R-frame F 2 K with x 2 F and two models I1 and I2 of T based on F such that x 2 F I1 n DI1 and x 2 F I2 n CI2 . Suppose (S; I) is an instance of the set splitting problem. Denote by Ti, Fi, Ci and Di, for i 2 S, the copies of T , F , C and D obtained by replacing every concept name A in them with Ai. Let TS;I = [ i2S
Ti [ f l (B u Ci) v ? j G 2 Ig [ f l (B u Di) v ? j G 2 Ig;
i2G i2G where B is a fresh concept name. We show now that there exists a splitting of (S; I) i TS;I 6j=K di2S (B u Fi) v ?. ()) Let S1; S2 be a splitting of (S; I). De ne an interpretation I on F by taking AiI = AI1 if i 2 S1, AiI = AI2 if i 2 S2, for all concept names A di erent from B, and BI = fxg. One can readily check that I j= TS;I and I 6j= di2S (B u Fi) v ?. (() Suppose that I j= TS;I and there is y 2 Ti2S (BI \ FiI ). We then set S1 = fi 2 S j y 2 CiI g and S2 = S n S1. It is readily checked that S1, S2 is a splitting of (S; I).
An R-constraint K is closed under disjoint unions if, for any F1; F2 2 K with F1 \ F2 = ;, we have F1 [ F2 2 FrThK, where F1[F2 = F1 [ F2 and rF1[F2 = rF1 [ rF2 . We also say that K has a free role r if, for any F 2 K and any x; y 2 F, the frame obtained by extending rF in F with the pair (x; y) belongs to FrThK. Note that all RBoxes, currently used in DL, correspond to constraints that are closed under disjoint unions and have in nitely many free roles (since typically DLs admit in nitely many role names and have nite RBoxes). The following condition is proved similarly to Theorem 2: Theorem 3. Suppose that an R-constraint K is closed under disjoint unions and has in nitely many free roles. If K is not convex then E L? subsumption over K is coNP-hard. 4
A class K of R-frames is called tabular if there is n > 0 such that j Fj n for all F 2 K. The aim of this section is to characterise the tabular constraints K over which E L? subsumption is tractable, that is, there is an algorithm which, given a TBox T and concepts C, D over R, can decide, in polynomial time, whether T j=K C v D. Clearly, E L? subsumption over any tabular K belongs to coNP.
The characterisation of tabular constraints we are about to prove dichotomises them into functional and non-functional. A class K of R-frames is R-functional if, for any F 2 K, r 2 R and w 2 F, we have jfv 2 F j (w; v) 2 rFgj 1. For R-interpretations I1 and I2 based on a functional frame F, we write I1 I2 if AI1 AI2 for all A 2 NC. Clearly, is a partial order.
Lemma 1. Suppose that I is an interpretation based on a nite R-functional frame F and w 2 I . Given any R-concept C, one can decide in polynomial time in jCj whether there exists an R-interpretation J such that I J and w 2 CJ . If such an interpretation exists, then there is a unique minimal (with respect to ) R-interpretation I(w; C) I with w 2 CI(w;C); moreover, this minimal interpretation can be constructed in polynomial time in jCj.
We are now in a position to prove the main result of this section. Theorem 4. Let K be a tabular class of R-frames for a nite R NR. If K is functional then E L? subsumption over K is in P. Otherwise, E L? subsumption over K is coNP-complete.
Proof. Assume rst that K is functional and we are given a TBox T and a CI C0 v D0 over R. Our polynomial time algorithm checking whether T j=K C0 v D0 runs as follows. Let F1; : : : ; Fn be a list of all frames in K (up to isomorphism). For each Fi and each w 2 Fi, we do the following: 1. Let I be the R-interpretation based on Fi with AI = ; for all A 2 NC. 2. Compute I := I(w; C0) if it exists (cf. Lemma 1). If it does not exist, return `yes' and stop. 3. Apply the following rule exhaustively: for C v D 2 T and v 2 I , if v 2 CI and I(v; D) does not exist, return `yes' and stop; otherwise, if I(v; D) 6= I, set I = I(v; D). 4. If w 2 (D0)I , return `yes.' Otherwise, return `no.' It is easy to see that T j=K C0 v D0 i the output is `yes' for all Fi and w 2 Fi .
Suppose K is not R-functional. Then there exists F 2 K with w 2 F such that jfv j (w; v) 2 rFgj 2. Let m be the maximal number for which there exist r 2 R, F 2 K and w 2 F with jfv j (w; v) 2 rFgj = m. Fix such r, F and w. We prove coNP-hardness of E L? subsumption over K using Theorem 2. To show that K is concept non-convex, consider the frg-TBox T with the following CIs: { A v 9r:Bi, for 1 { Bi u Bj v ?, for 1 { A v 9r:B { Bi v E, for 2 i i
m; i < j Clearly, T j=K A v 9r:(B u B1) t 9r:(B u E). Consider next the interpretations I1 and I2 over F where w1; : : : ; wm are the rF-successors of w in F and { AIi = fwg and BIi = fwig, for i = 1; 2; { BiIi = fwj g, for i = 1; 2 and 1 j m; { EIi = fw2; : : : ; wmg, for i = 1; 2.
Then we have Ii j= T , w 2 AI1 n(9r:(B uE))I1 and w 2 AI2 n(9r:(B uB1))I2 . By Theorem 2, E L? subsumption over K is coNP-hard. And as we have mentioned above, E L? subsumption for tabular constraints is in coNP.
The above proof of coNP-hardness goes through for many other constraints: Theorem 5. Let K be a class of R-frames such that there are r 2 R and n 2 for which (i ) no point in frames from K has > n r-successors, and (ii ) at least one point in a frame from K has 2 r-successors. Then E L? subsumption over K is coNP-hard. 5
In this section, we assume that R = frg and consider universal classes of Rframes F with re exive rF.
Theorem 6. Let K be a universal constraint for a single re exive relation. If K is not TBox equivalent to any of the following classes: (sin) the class of all singleton frames, (tra) the class of all transitive frames, (equ) the class of all equivalence relations, (all) the class of all frames, (sym) the class of all symmetric frames, then K is concept non-convex, and so E L? subsumption over K is coNP-hard. E L? subsumption over K is also coNP-hard if K is TBox equivalent to (sym). However, if K is TBox equivalent to one of (sin), (tra), (equ) or (all), then E L? subsumption over K is in P.
Note that there are uncountably many distinct universal TBox de nable classes
of frames with a single re exive relation (see [
Here we only give a brief sketch of the proof of Theorem 6. Note rst that the
polynomial upper bound follows from [
{ If K is not TBox equivalent to (all), then there exists a nite re exive tree
F such that F 62 FrThK.
{ If K consists of symmetric frames and is not TBox equivalent to (sym), then
there exists a nite re exive and symmetric tree F such that F 62 FrThK.
{ If K consists of transitive frames and is not TBox equivalent to (tra), then
there exists a nite re exive and transitive tree F such that F 62 FrThK.
Proof sketch. We prove the rst claim; the remaining ones are treated similarly.
As K is not TBox equivalent to (all), there are T , C, D such that T j=K C v D
and T 6j=K0 C v D, where K0 is the class of all frames. By applying standard
unravelling to a witness interpretation for T 6j=K0 C v D, we obtain a (possibly
in nite) re exive tree F 62 FrThK. If F is nite, we are done. Otherwise, using
the fact that K is universal and employing Tarski's nite embedding property
[
Having Lemma 2 at hand, we can now proceed with a case distinction. Suppose K is a non-empty universal class of re exive frames that is not TBox equivalent to any of the classes mentioned in Theorem 6. Then, by Lemma 2, there exists a re exive tree F such that F 62 FrThK, F0 2 FrThK, for any proper subframe F0 of F, and one of the following conditions holds: 1. F is the singleton frame; 2. F is the two-element r-chain; 3. F contains a point w with least two r-successors, and all r-successors of w are leaves in F; 4. F contains distinct points w; w1; w2 such that (w; w1) 2 rF, (w1; w2) 2 rF and w2 is a leaf, which is the only r-successor of w1.
Case 1. This case is actually impossible because it implies that K is empty (remember that K is universal, and so closed under subframes). Case 2. In this case, K is a class of symmetric frames. Since we assume that K is not TBox equivalent to (sym), one can apply the second claim of Lemma 2 to obtain a nite re exive and symmetric tree F such that F 2= FrThK. A case distinction (similar to the one we are currently doing) shows that, since K is not TBox equivalent to (sin), K is concept non-convex.
Case 3. Let us remove a proper r-successor of w from F and denote by H the resulting frame, which belongs to FrThK. Let w1 be one of the remaining successors of w in H. Denote by H0 the frame obtained from H by adding a fresh r-successor w2 to w1, and by w0 the root of H0. Two cases are possible now. Case 3.1: either H0 2 FrThK or the expansion of H0 by adding (w; w2) to rH0 is in FrThK. Take additional concept names A and A. To show that K is concept non-convex, we will use C1 = 9r2:(A0 u9r2:A0) and C2 = 9r2:(A0 u9r2:A0), where A0 = Aw1 u A, A0 = Aw1 u A and 9rm:C is an abbreviation de ned inductively by taking 9r0:C = C and 9rm+1:C = 9r:9rm:C.
In addition, we require a generic way of describing frames using TBoxes. Given an R-frame R, let Au be a fresh concept name for every u 2 R. Let TS (R) be the (possibly in nite) TBox with the following CIs: { Au v 9r:Av, for (u; v) 2 rR; { Au u Av v ?, for u 6= v; { Au u 9r:Av v ?, for (u; v) 2= rR.
One can show that, for any R-frame R with root w (from which all other points are reachable via roles) and any R-frame F, we have TS (R) 6j=F Aw v ? i R is a p-morphic image of a subframe of F.
Returning to Case 3.1., de ne T to be the TBox with the following CIs: TS (H);
Aw v 9r2:A0;
Aw v 9r2:A0:
Then T j=K Aw0 v 9rm:(Aw u C1) t 9rm:(Aw u C2), where m is the distance
between w0, w, but T 6j=K Aw0 v 9rm:(Aw u C1), T 6j=K Aw0 v 9rm:(Aw u C2).
Case 3.2: suppose that Case 3.1 does not hold. Denote by w0 the root of H. Take
a fresh concept name A and consider the TBox T with the following CIs:
{ TS (H),
{ A u 9r:Av v ?, for all v with (w; v) 62 rH,
{ Av u 9r:A v ?, for all v with both (v; w) 62 rH and (v; w1) 62 rH,
{ A u 9r:Aw0 v 9r:Aw, for (w; w0) 2 rH, w0 6= w1,
{ Aw v 9r:(A u 9r:Aw1 ),
{ if w has an r-predecessor wp, then Awp u 9r:A v 9r:(Aw u 9r:(A u 9r:Aw)).
Then T j=K Aw0 v 9rm:(Aw u 9r:(A u 9r:Aw)) t 9rm:(Aw u 9r:(Aw1 u 9r:A)),
but T 6j=K Aw0 v B for either of the disjuncts B in the right-hand side.
Case 4. A case distinction similar to, but much more tedious than the previous
ones shows that K is concept non-convex if the constraint K is not transitive.
The case where K is a class of transitive frames has been considered in [
Typically, in DL applications one role is not enough. Therefore, the question
is whether the four universal constraints guaranteeing tractability for a single
re exive relation still ensure tractability if more than one role is considered. This
is well known to be the case for transitivity and re exivity, and this is trivially
the case for the singleton frame. Equivalence relations behave not so well:
Theorem 7. If K is a constraint consisting of two (or more) equivalence
relations, then E L? subsumption over K is NP-hard. In particular, tractability of
E L? subsumption is not preserved under fusions in the sense of [
Fk; X 1^ 2 X 2 v X 1_ 2 :
X 1 u X 2 ; Let T be the TBox containing all the CIs (2){(7), and L2n u X' v ?. One can show that T j=K L0 v ? i ' is satis able. (4) (5) (6) (7) 6
E L and E L? So far, we have considered E L? rather than E L. The main reason is that ? makes proofs more transparent. We now show that Theorems 4{7 above hold for E L.
An R-frame F0 is called a generated subframe of an R-frame F if it is a subframe of F and, for all u; v 2 F and r 2 R, if (u; v) 2 rF and u 2 F0 then v 2 F0 . Given v 2 F, the subframe of F generated by v is the smallest generated subframe of F containing v.
Theorem 8. Let K be an R-constraint closed under generated subframes, for a nite R. Then E L? subsumption over K is polynomially reducible to E L subsumption over K, and, for any R-constraint K0 closed under generated subframes, K0 is TBox-equivalent to K in E L? i K0 is TBox-equivalent to K in E L. Proof. Let T and C v D in E L? be given. We may assume that ? occurs in them only in the form E v ?, with E being an E L-concept. Let B be a fresh concept name, and let T 0 and D0 result from T and D, respectively, by replacing all ? with B. Set T 00 = T 0 [ f9r:B v B j r 2 Rg [ fB v D0g. We claim that T j=K C v D i T 00 j=K C v D0. Clearly, if T 6j=K C v D, then T 00 6j=K C v D0: for if we have a witness model for T 6j=K C v D, then we can interpret B by the empty set to obtain a model of T 00 refuting C v D0. Conversely, if T 00 6j=K C v D0, take an interpretation I based on a frame in K and v 2 I such that I j= T 00 but v 2 CI n (D0)I . Let F be the subframe generated by v in the underlying frame of I. Then F 2 K and BI \ F = ;. Hence T 6j=F C v D, as required.
It follows from Theorem 8 that Theorems 6 and 7 hold for E L in place of E L?. Theorem 4 can be proved for E L as follows. Let K be a non-functional tabular constraint. Then the class K0 of subframes of frames from K is still a non-functional tabular constraint and j=K0 is polynomially reducible to j=K, both for E L and E L? (using relativisation). Thus, by Theorem 4 for E L? and Theorem 8, the E L subsumption problem for K0 is coNP-hard. Hence it is coNP-hard for K. Theorem 5 can be proved similarly. The main open problem in the area is the dichotomy question formulated in the introduction. If the answer to this question is positive, then the proof will probably require some new techniques and a great number of case distinctions.
We conjecture that a transparent dichotomy, possibly more involved than
Theorem 6, can be obtained for arbitrary relational constraints on a single
reexive relation. Of course, an additional problem in this case is how to deal
with non rst-order constraints. A possible approach can be illustrated by the
following result from [
When moving beyond the `bounded' constraints of Theorems 4 and 5, it seems to be much harder to obtain general results for relations that can be nonre exive than for the re exive ones. For example, in contrast to the re exive case, E L? subsumption is now also in P for the constraints Kn consisting of (irre exive) trees of depth n. Thus, there are in nitely many transitive classes with a single relation for which E L? subsumption is tractable.