We discuss the complexity of reasoning and ontology-mediated query answering with the logics from the DL-Lite family extended by various types (Horn, Krom and Boolean) of role inclusions. We compare the expressive power of those logics with 1- and 2-variable fragments of first-order logic. Our most interesting findings show that binary disjunctions on roles do not change the complexity of satisfiability if disjunction is allowed on concepts, while still causing undecidability of UCQ answering.
Concepts (unary predicates) and roles (binary predicates) are usually treated quite
differently in description logics (DLs). For example, the basic expressive DL ALC allows
statements about concepts in the form of arbitrary Boolean formulas but disallows any
statements about roles. A notable exception is DL-LiteR [
To explore what happens if concepts and roles are treated equally, we introduce
a few new members to the DL-Lite family (which could be qualified as distant
relatives or illegitimate children) and denote the logics in the extended ‘clan’ by DL-Litecr,
where the parameters r; c 2 fbool; horn; krom; coreg define the allowed structure of
role and, respectively, concept inclusions. We present our observations on the
complexity of checking satisfiability of DL-Litecr knowledge bases and answering (unions
of) conjunctive queries mediated by DL-Litecr ontologies. It turns out that the
resulting languages provide a new way of classifying some fundamental fragments of
firstorder logic (FO). Consider first DL-Litebbooooll, which is easily seen to be contained in
the two-variable fragment FO2 of FO. Using the fact that ALC>;id;\;:; , the
extension of ALCI with Boolean operations on roles and the identity role, has exactly the
same expressive power as FO2 [16], we show that DL-Litebbooooll almost captures FO2:
it corresponds to ALC>;\;:; , the language ALC>;id;\;:; without the identity role.
DL-Litebbooooll inherits from these languages NEXPTIME-completeness of satisfiability
and undecidability of CQ-answering [17, 15]. Note that DL-Litebbooooll also almost
captures the class of linear existential disjunctive rules with two variables [
aCaIs a aRIas
Bool Horn Krom core
Bool
guarded Bool NEXPTIME (Th. 3)
EXPTIME (Th. 3)
Horn NP (Th. 6) P (Th. 6) P (Th. 6)
Krom NP (Th. 4) NP (Th. 4) NL (Th. 4) core and c 2 fbool; horn; krom; coreg can be encoded in propositional logic (or in the onevariable fragment of FO), with the complexity of satisfiability checking ranging from NL to P and NP; see Table 1. Our most interesting findings demonstrate that binary disjunctions on roles do not change the complexity of satisfiability if disjunction is allowed on concepts, while still causing undecidability of UCQ answering. Thus, satisfiability of DL-Litekkrroomm knowledge bases is NL-complete, while answering UCQs mediated by DL-Litekkrroomm ontologies is undecidable.
The logics introduced above leave a huge gap between those having Boolean role inclusions and those that only admit Horn or Krom role inclusions. To ‘complete’ the picture, we add DL-Litegc-bool, the fragment of DL-Litebcool in which Boolean role inclusions are guarded. It turns out that DL-Litegc-bool approximates the two-variable guarded fragment GF2 of FO, from which it inherits EXPTIME-completeness of satisfiability and 2EXPTIME-completeness of UCQ-answering.
Our motivation to investigate the complexity of the family of languages DL-Litecr
with r; c 2 fbool; horn; krom; coreg stems from the observation that in the context of
answering queries mediated by temporal DL-Lite ontologies [
Let a0; a1; : : : be individual names, A0; A1; : : : concept names, and P0; P1; : : : role names. We define roles S and basic concepts B as usual in DL-Lite:
S ::= Pi j Pi ;
B ::=
Ai j 9S: A concept or role inclusion (CI or, respectively, RI) takes the form #1 u u #k v #k+1 t t #k+m; k; m 0; (1) where the #i are all basic concepts or, respectively, roles. As usual, we denote the empty u by > and the empty t by ?. When it does not matter whether we talk about concepts or roles, we refer to the #i as terms. A TBox T and an RBox R are finite sets of concept and, respectively, role inclusions; their union O = T [ R is called an ontology.
We classify ontologies according to the form of their concept and role inclusions. Let r; c 2 fbool; horn; krom; coreg. We denote by DL-Litecr the description logic whose ontologies contain concept and role inclusions of the form (1) satisfying the following constraints for c and r, respectively: (horn) m 1, (krom) k + m 2, (core) m 1 and k + m (bool) k; m 0.
2, Note that all of our logics allow (disjointness) inclusions of the form #1 u #2 v ?.
When defining our DL-Lite logics, we treat concept and role inclusions in a uniform
way, which is usually not the case in standard DLs. In particular, the DL-Lite logics [
As usual, an ABox, A, is a finite set of assertions of the form Ai(aj ) and Pi(aj ; ak). A DL-Litecr knowledge base (KB, for short) is a pair K = (O; A), where O is a DL-Litecr ontology and A an ABox. Interpretations are also standard, taking the form I = ( I ; I ), where I 6= ;, aiI 2 I , AiI I and PiI I I . We call I a model of a KB K and write I j= K if all of the assertions in A and inclusions in O are true in I. If a KB has a model, it is called consistent or satisfiable. The computational (combined) complexity of satisfiability checking for DL-Litecr KBs is one of our concerns in this paper.
The other is the (combined and data) complexity of answering conjunctive queries (CQs) and unions of CQs (UCQs) mediated by DL-Litecr ontologies. A CQ is a firstorder (FO) formula of the form q(x) = 9y '(x; y), where ' is a conjunction of unary or binary atoms Q(z) with z x [ y. A UCQ is a disjunction of CQs with the same answer variables x. A DL-Litecr ontology-mediated query (OMQ) is a pair Q = (O; q(x)), where O is a DL-Litecr ontology and q a (U)CQ.
Given an ABox A, we denote by ind(A) the set of individual names that occur in A. A tuple a in ind(A) is a certain answer to an OMQ Q = (O; q(x)) if x and a are of the same length and I j= q(a), for every model I of (O; A); in this case we write O; A j= q(a). If the set x of answer variables is empty (that is, q is Boolean), a certain answer to Q over A is ‘yes’ if I j= q, for every model I of (O; A), and ‘no’ otherwise. The OMQ answering problem for DL-Litecr is to check, given an OMQ Q = (O; q(x)) with a DL-Litecr ontology O, an ABox A and a tuple a in ind(A), whether a is a certain answer to Q over A. 3
Every DL-Litebbooooll ontology is easily seen to be equivalent to a sentence in the twovariable fragment of FO, and every DL-Litebgo-boolol ontology is equivalent to a sentence in the two-variable guarded fragment of FO. The converse directions do not hold. We show, however, that both languages can be equivalently captured by natural description logics with Boolean operators on roles (and no role inclusions). We give a concise description of the expressivity of both DL-Litebbooooll and DL-Litebgo-boolol ontologies within those more familiar description logics.
Denote by FO2 the fragment of first-order logic with unary and binary relation
symbols, the equality symbol, no function symbols, and the individual variables x and y
only. FO2 is well understood [
Denote by ALCid;>;\;:; the DL whose roles are built according to the rule S; S1; S2 ::=
> j id j Pi j S1 u S2 j :S j S ; and whose concepts are built according to the rule
C; C1; C2 ::=
> j Ai j 9S:C j C1 u C2 j :C;
where S is an ALCid;>;\;:; -role. An ALCid;>;\;:; -CI takes the form C1 v C2,
where C1; C2 are ALCid;>;\;:; -concepts. The semantics of ALCid;>;\;:; is as
expected, with id interpreted in any interpretation I as the relation f(d; d) j d 2 I g.
ALCid;>;\;:; was introduced in [16], various fragments had been considered
before [
The relationship between ALCid;>;\;:; and DL-Litebbooooll can be stated in a precise way: DL-Litebbooooll is ALCid;>;\;:; without the relation id. Observe that we clearly cannot express ALCid;>;\;:; -CIs such as A v 9:id:A in DL-Litebbooooll. Denote by ALC>;\;:; the language ALCid;>;\;:; without the relation id. We say that an ontology O is a model conservative extension of an ontology O0 if O j= O0, the signature of O0 is contained in the signature of O, and every model of O0 can be expanded to a model of O by providing interpretations of the fresh symbols of O and leaving the domain and the interpretation of the symbols in O0 unchanged.
Theorem 1. (i) For every DL-Litebbooooll ontology, one can compute in linear time an equivalent ALC>;\;:; ontology.
(ii) For every ALC>;\;:; ontology, one can compute in polynomial time a model conservative extension in DL-Litebbooooll.
Proof. Clearly, every CI in DL-Litebbooooll is also in ALC>;\;:; (9S abbreviates 9S:>). Every role inclusion S1 u u Sk v Sk+1 t t Sk+m in DL-Litebbooooll is equivalent to the ALC>;\;:; -CI 9(S1 u >;u\;:S;k u :(Sk+1 t t Sk+m)):> v ?.
Conversely, assume an ALC ontology O is given. Using standard normalisation one can construct in linear time an ALC>;\;:; ontology with CIs of the form A v 8S:B; 8S:B v A;
A1 u A2 v B;
A v :B; :A v B; where A; B; A1; A2 range over concept names and >, which is a model conservative extension of O. Now we can replace any CI A v 8S:B by
S v Q t R; 9Q v B;
A v :9R; where Q and R are fresh role names, and any CI 8S:B v A by :A v 9R;
R v S; 9R v :B; where R is a fresh role name. It remains to observe that we can replace the Boolean role S by a role name and DL-Litebbooooll role inclusions to obtain a model conservative extension.
The two-variable guarded fragment of FO, denoted GF2, is the fragment of FO2 defined as follows: – every atomic formula in FO2 is in GF2; – GF2 is closed under ^ and :; – if v 2 fx; y; xyg, is in GF2, and G is in atomic formula in FO2 containing all free variables in , then 9v (G ^ ) is in GF2.
It is not difficult to see that GF2 corresponds to the fragment ALCigdu;a>rd;e\d;:; of the DL ALCid;>;\;:; in which every role expression is either > or contains a guard: a toplevel conjunct that is either id, a role name, or the inverse of a role name. The fragment DL-Litebgo-boolol clearly lies within ALCg\u;a:rd;ed, the fragment of ALCigdu;a>rd;e\d;:; without the roles id and >. In fact, similarly to the proof of Theorem 1, one can show the following: Theorem 2. (i) For every DL-Litebgo-boolol ontology, one can compute in linear time an \;:; \;:; equivalent ALCguarded ontology. (ii) For every ALCguarded ontology, one can compute in polynomial time a model conservative extension in DL-Litebgo-boolol.
It is known [
Proof. For DL-Litebbooooll, NEXPTIME-completeness follows from Theorem 1 and [15,
Theorem 14]. For DL-Litebg-oboolol, the EXPTIME upper bound follows from the fact that
satisfiability of DL-Litebg-oboolol KBs is reducible to satisfiability of guarded FO-formulas
with at most binary predicates, which is known to be in EXPTIME [
Now we consider ontologies with Krom and Horn role inclusions. For an ontology O, let role (O) = fP; P j P is a role name in Og. We also set (P ) = P . Suppose J = ( J ; J ) is an interpretation. Denote by tJ (x) the concept type of x 2 J in J , which comprises all B with x 2 BJ and all :B with x 2= BJ , for basic concepts B of the form A, for concept names in O, and 9S, for S 2 role (O). Similarly, we denote by rJ (x; y) the role type of (x; y) 2 J J in J , which comprises all S with (x; y) 2 SJ and all :S with (x; y) 2= SJ , for S 2 role (O). Lemma 1. For every satisfiable DL-Litekbroooml KB K = (O; A), there exists a model I = ( I ; I ) of K such that – I = ind(A) [ fwSi j S 2 role (O) and 0 i < 3g, – if a 2 (9S)I , then (a; wS0 ) 2 SI , for any a 2 ind(A) and any S 2 role (O), – if wRi 2 (9S)I , then (wRi; wSi 1) 2 SI , for any R; S 2 role (O) and 0 i < 3, where denotes addition modulo 3. In particular, DL-Litekbroooml enjoys the linear model property: j I j = jind(A)j + 3jrole (O)j.
Proof. Suppose DL-Litekbroooml KB K = (O; A) is satisfied in J = ( J ; J ). We construct the required model I as follows. For a role literal L (that is, a role or its negation), we denote by cl(L) the set of all role literals L0 such that O j= L v L0.
For each role S in O with SJ 6= ;, we pick wS 2 J with 9S 2 tJ (wS ); for S with SJ = ;, we pick an arbitrary wS . Without loss of generality, we can assume that all the selected wS are pairwise distinct. The set comprising three copies wS0 ; wS1 ; wS2 of all those wS together with ind(A) is denoted by I (this technique with three copies is similar to the one used in the proof of [7, Proposition 8.1.4] establishing the finite model property of FO2). Define a function f by taking f (a) = a, for all a 2 ind(A), and f (wSi ) = wS , for all S and i. We then set tI (w) = tJ (f (w)), for all w 2 J .
We now show how to define rI (w; w0) for w; w0 2 I . The following three cases need consideration.
– If w = a, w0 = wS0 and 9S 2 tJ (w), then we define rI (w; w0) by first taking cl(S). Suppose now that > v Sj t Sj0 , for 1 j n, are all disjunctions in O such that Sj , Sj0 and their negations are not in cl(S). As J is a model of O, for each j, either Sj or Sj0 must be in rJ (f (w); f (w0)). Suppose for definiteness that it is Sj . Then we add cl(Sj ) to rI (w; w0). Using the main property of Krom formulas (if a contradiction is derivable, then it is derivable from two literals), we can show that the resulting rI (w; w0) is consistent with O and respects tI (w) and tI (w0) in the sense that R 2 riI (1wa;nwd09) Sim2pltieJs(9wR), 2thetnI (wwe)daenfidn9eRrI (w; w0) as above. 2 tI (w0). – If w = wRi, w0 = wS – For any other w, w0 not covered above (in particular, if w = a, w0 = wSi and either i > 0 or 9S 2= tJ (a)), we set rI (w; w0) = rJ (f (w); f (w0)).
It is readily checked that the constructed concept types tI (w) and role types rI (w; w0), for w; w0 2 I , define a model of K.
The existence of a model specified in Lemma 1 can be encoded by an essentially propositional formula 'K with atomic propositions of the form By(x), for x 2 I and basic concepts B from O, saying that B holds on x in I, and P y(x; x0), for a role name P in O, saying that P holds on (x; x0) in I. The formula 'K is a conjunction of the following sentences, for all x; x0 2 I : B1y(x) ^ ^ Bky(x) ! Bky+1(x) _
_ Bky+m(x); for each CI B1 u u Bk v Bk+1 t t Bk+m in O; S1y(x; x0) ^ ^ Sky(x; x0) ! Sky+1(x; x0) _ _ Sky+m(x; x0); Ay(a);
for each A(a) 2 A; (9S)y(a) ! Sy(a; wS0 ) Sy(x; x0) ! (9S)y(x);
for each S: for each RI S1 u u Sk v Sk+1 t
t Sk+m in O; and
P y(a; b);
for each P (a; b) 2 A; and (9S)y(wRi) ! Sy(x; wSi 1); for each S and i; where (Pi )y(x; x0) = Piy(x0; x). Note that, if K is a DL-Litekkrroomm KB, then 'K is a Krom formula, which can be constructed by a logspace transducer. It can now be straightforwardly shown that: Lemma 2. A DL-Litekbroooml KB K is satisfiable iff 'K is satisfiable.
As a consequence, and using the fact that DL-Litekhroormn can express DL-Litekbroooml (as Krom RIs can simulate Krom CIs, and the latter can express the complements of concepts), we obtain the following complexity results: Theorem 4. Satisfiability checking is NP-complete for DL-Litekbroooml and DL-Litekhroormn KBs, and NL-complete for DL-Litekkrroomm KBs.
Next, we consider DL-Litebhooronl and DL-Litehhoorrnn KBs. Note that universal roles defined by RIs such as > v S can be trivially omitted from KBs, so in what follows we assume that our KBs do not contain universal roles. The next lemma is proved by a more or less standard unravelling construction. We need an unravelled infinite forest-shaped model rather than a finite one similar to that in Lemma 1 in order to obtain Theorem 12 on the data complexity of OMQ answering with DL-Litehhoorrnn.
Lemma 3. Let K = (O; A) be a satisfiable DL-Litebhooronl KB. Then there is a model I = ( I ; I ) such that – I ind(A) [ faw j a 2 ind(A); w is a word over wS ; for S 2 role (O)g, – tI (w1wS ) = tI (w2wS ), for any w1wS and w2wS in I , – if w1 and w2 are not both in ind(A), then (w1; w2) 2 RI iff there is 9S 2 tI (w1) such that R 2 rS , S is minimal with this property w.r.t. v, and w2 = w1wS , where rS = fR j O j= S v Rg.
If K is a DL-Litehhoorrnn KB, then B 2 tI (wwS ) iff O j= 9S concept B. v B, for any basic Proof. First, we can show that if K is satisfied in a model I0, then it is satisfied in a model J with minimal role types where, for all w; w0 2 J with fw; w0g 6 ind(A), we have
rJ (w; w0) = rS ; for some role S: Indeed, suppose (w; w0) violates this property and w0 2= ind(A). Let rI0 (w; w0) = fS1; : : : ; Skg. Then we replace w0 by k copies w10; : : : ; wk0 with the same concept types as w0, and connect w to each wi0 by the roles in rSi only. In the resulting interpretation, the pairs (w; wi0) are as required, but the wi0 may not satisfy CIs in O due to missing witnesses for existential concepts 9R. To fix each of these wi0, we create k 1 copies wij of w for j 6= i (again, the wij belong to the same concepts as w) and connect each wij to wi0 by all roles in rSj . It can be seen that, in the resulting interpretation, the pairs (wij ; w0) satisfy the required property, but now the wij may not satisfy CIs in O (again, i due to some 9R). To fix these new elements, we create copies of w0, and so on.
Second, for each role name P such that P J 6 ind(A) ind(A), we can fix two ‘witnesses’ by arbitrarily choosing wP and wP such that fwP ; wP g 6 ind(A) and rJ (wP ; wP ) = rP . Now we can unravel J into the required forest-shaped model I of K by using only witnesses of the form wP and wP .
Using Lemma 3, we now define translations of DL-Lite KBs with Horn RIs into
universal sentences in FO1 (FO-sentences with one variable), Horn-FO1 and Krom-FO1,
the satisfiability problems for which are known to be NP-, P- and NL-complete [
A(x) if C = A;
EP (x) if C = 9P;
EP (x) if C = 9P : A CI C1 u u Ck v Ck+1 t
t Ck+m is then naturally translated into 8x C1y(x) ^ ^ Cky(x) ! Cky+1(x) _ _ Cky+m(x) : We also include the following sentences, for all roles S:
8x (9S)y(x) ! (9S )y(wS ) : Since we assume that the binary types for (w1; w2) with fw1; w2g 6 ind(A) are minimal, that is, generated by a single role, RIs are translated into the the following sentences: 8x (9S)y(x) ! (9R)y(x) ; 8x (9S)y(x) ! ? ; for all roles S and R with O j= S v R; for all roles S with O j= S v ?: Assertions of the form A(ai) are translated into A(ai) and of the form P (ai; aj ) into P (ai; aj ). We also add
P (ai; aj ) ! (9P )y(ai) ^ (9P )y(aj ) for all pairs ai; aj 2 ind(A) and all role names P , and
S1(ai; aj ) ^ ^ Sk(ai; aj ) ! Sk+1(ai; aj ); (2) for all pairs ai; aj 2 ind(A) and RIs S1 u u Sk v Sk+1 and similarly for RIs S1 u u Sk v ?, with ? in the conclusion, where P (ai; aj ) is a shortcut for P (aj ; ai). It can easily be seen that K is satisfiable iff the translation is consistent. (ii) We observe that the translation above is in Horn-FO1 if K is in DL-Litehhoorrnn. (iii) The translation in (i) for DL-Litekhroormn is not in Krom-FO1. However, since the translation works in polynomial time, we can modify it so that instead of (2) it produces all S(ai; aj ) such that R; A j= S(ai; aj ) or ? if R; A j= ?, where R is the RBox of O.
As a consequence, we obtain the following complexity results: Theorem 6. Satisfiability checking is NP-complete for DL-Litebhooronl KBs, and P-complete for DL-Litehhoorrnn and DL-Litekhroormn KBs. 5
In this section, we give a brief survey of results on the combined and data complexity of answering OMQs with DL-Litecr ontologies and (U)CQs, which can mostly be obtained in a rather straightforward way from existing results. We start with undecidability results, which show that the language DL-Litebbooooll behaves again similarly to the twovariable fragment of FO and that even in DL-Litekkrroomm UCQ answering is undecidable. The following can be shown using [17, Theorem 1] and the encoding of 8R:C given in the proof of Theorem 1: Theorem 7. Answering OMQs with DL-Litebbooooll ontologies and CQs is undecidable for combined complexity.
The next result follows from [17, Theorem 3]: Theorem 8. Answering OMQs with DL-Litekkrroomm ontologies and UCQs is undecidable for combined complexity.
It remains open whether answering OMQs with DL-Litekkrroomm ontologies and CQs is
undecidable. The language DL-Litebgo-boolol can be regarded as a fragment of the guarded
fragment, GF, of FO. Query evaluation for GF was first investigated in [
We now sketch the results on data complexity. A coNP-upper bound for (U)CQ
evaluation in GF for data complexity is proved in [
We conjecture that important properties such as datalog rewritability and first-order
rewritability of such OMQs are decidable as well, but this remains open. In many
applications of ontology-mediated query answering, only the TBox is known in advance, but
not the relevant queries. In this case, investigating the complexity at the level of OMQs
is not appropriate, but instead one is interested in an upper bound for the complexity of
query evaluation for all OMQs based on the given TBox. As DL-Litebgo-boolol lies within
the fragment uGF2 (1; =) of GF introduced in [
We note that a dichotomy between datalog-rewritable and CONP is quite rare. There
are, for example, ALC TBoxes for which not all OMQs are datalog rewritable but still
in P [