=Paper=
{{Paper
|id=Vol-2373/paper-19
|storemode=property
|title=A Note on DL-Lite with Boolean Role Inclusions
|pdfUrl=https://ceur-ws.org/Vol-2373/paper-19.pdf
|volume=Vol-2373
|authors=Roman Kontchakov,Vladislav Ryzhikov,Frank Wolter,Michael Zakharyaschev
|dblpUrl=https://dblp.org/rec/conf/dlog/KontchakovRWZ19
}}
==A Note on DL-Lite with Boolean Role Inclusions==
https://ceur-ws.org/Vol-2373/paper-19.pdf
A Note on DL-Lite with Boolean Role Inclusions
Roman Kontchakov1 , Vladislav Ryzhikov1 , Frank Wolter2 , and Michael
Zakharyaschev1
1
Birkbeck, University of London, U.K.
2
University of Liverpool, U.K.
Abstract. 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 in-
teresting findings show that binary disjunctions on roles do not change the com-
plexity of satisfiability if disjunction is allowed on concepts, while still causing
undecidability of UCQ answering.
1 Introduction
Concepts (unary predicates) and roles (binary predicates) are usually treated quite dif-
ferently 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 [9], also denoted DL-LiteH core
in the classification of [1], where concept and role inclusions take the form of binary
Horn (aka core) formulas ϑ1 v ϑ2 or ϑ1 u ϑ2 v ⊥, where the ϑi are either both con-
cepts or both roles. On the other hand, DL-LiteR,u [10], aka DL-LiteH horn [1], allows
arbitrary Horn concept inclusions ϑ1 u · · · u ϑk v ϑk+1 but only core role inclusions.
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 rela-
tives or illegitimate children) and denote the logics in the extended ‘clan’ by DL-Literc ,
where the parameters r, c ∈ {bool, horn, krom, core} define the allowed structure of
role and, respectively, concept inclusions. We present our observations on the com-
plexity of checking satisfiability of DL-Literc knowledge bases and answering (unions
of) conjunctive queries mediated by DL-Literc ontologies. It turns out that the result-
ing languages provide a new way of classifying some fundamental fragments of first-
order logic (FO). Consider first DL-Litebool bool , which is easily seen to be contained in
the two-variable fragment FO2 of FO. Using the fact that ALC >,id,∩,¬,− , the exten-
sion of ALCI with Boolean operations on roles and the identity role, has exactly the
same expressive power as FO2 [16], we show that DL-Litebool bool almost captures FO2 :
it corresponds to ALC >,∩,¬,− , the language ALC >,id,∩,¬,− without the identity role.
DL-Litebool
bool inherits from these languages NE XP T IME -completeness of satisfiability
and undecidability of CQ-answering [17, 15]. Note that DL-Litebool bool also almost cap-
tures the class of linear existential disjunctive rules with two variables [8]. On the other
hand, we show that satisfiability of DL-Literc knowledge bases with r ∈ {horn, krom}
Table 1. Combined complexity of satisfiability checking (all bounds are tight). For the languages
DL-Literc in the grey cells, the complexity is the same as for DL-Literr as concept inclusions in c
can be expressed by means of role inclusions in r.
aa
RIs
CIs aa Bool guarded Bool Horn Krom core
a
Bool NE XP T IME (Th. 3) E XP T IME (Th. 3) NP (Th. 6) NP (Th. 4) NP [1]
Horn P (Th. 6) NP (Th. 4) P [10]
Krom P (Th. 6) NL (Th. 4) NL [1]
core NL [9]
and c ∈ {bool, horn, krom, core} can be encoded in propositional logic (or in the one-
variable 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 dis-
junctions 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-Litekrom
krom knowledge bases is NL-complete, while answering UCQs mediated by
DL-Litekrom
krom 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-Liteg-bool
c , the fragment of DL-Litebool
c in which Boolean role inclu-
sions are guarded. It turns out that DL-Liteg-bool
c approximates the two-variable guarded
fragment GF2 of FO, from which it inherits E XP T IME-completeness of satisfiability
and 2E XP T IME-completeness of UCQ-answering.
Our motivation to investigate the complexity of the family of languages DL-Literc
with r, c ∈ {bool, horn, krom, core} stems from the observation that in the context of
answering queries mediated by temporal DL-Lite ontologies [3, 2] in some cases ad-
mitting the same type of concept and role inclusions does not affect the data complexity
of query answering, while in others the effect is dramatic.
2 DL-Lite with Complex Role Inclusions
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 | Pi− , B ::= Ai | ∃S.
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 ∈ {bool, horn, krom, core}. We denote by DL-Literc 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 ≤ 2,
(bool) k, m ≥ 0.
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 [9,
1] only allow core role inclusions of the form S1 v S2 and S1 u S2 v ⊥. Also,
standard DL-Lite logics often do not admit CIs and RIs with > on the left-hand side,
which are mostly harmless and do not affect the complexity of reasoning and query
answering. Modulo the latter insignificant difference, the logic DL-Litecore core is known
under the names DL-LiteR [9] and DL-LiteH core [1], where the subscript core refers
to concept inclusions and the superscript H stands for ‘role hierarchies’, DL-Litecore horn
goes by the names DL-LiteR,u [10] and DL-LiteH core
horn [1], DL-Litekrom = DL-Litekrom
H
H
and DL-Litecore
bool = DL-Litebool [1]. Note also that the logic DL-Litec
krom
is DL-LiteH c
extended with ‘covering’ role inclusions > v S1 t S2 and, in particular, the inclu-
sions > v P saying that P is the universal role. Finally, in the logic DL-Liteg-bool bool ,
we disallow role inclusions of the form > v S1 t · · · t Sn for n ≥ 1 (g stands for
g-bool
‘guarded’). While DL-Liteboolbool and DL-Litebool turn out to behave radically different,
horn core
for DL-Litehorn and DL-Litecore the restriction to guarded RIs (i.e., excluding universal
roles) would have no effect on the problems we consider.
As usual, an ABox, A, is a finite set of assertions of the form Ai (aj ) and Pi (aj , ak ).
A DL-Literc knowledge base (KB, for short) is a pair K = (O, A), where O is a
DL-Literc ontology and A an ABox. Interpretations are also standard, taking the form
I = (∆I , ·I ), where ∆I 6= ∅, aIi ∈ ∆I , AIi ⊆ ∆I and PiI ⊆ ∆I × ∆I . We call I
a model of a KB K and write I |= 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 computa-
tional (combined) complexity of satisfiability checking for DL-Literc 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-Literc ontologies. A CQ is a first-
order (FO) formula of the form q(x) = ∃y ϕ(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-Literc ontology-mediated query (OMQ) is a pair
Q = (O, q(x)), where O is a DL-Literc 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 |= q(a), for every model I of (O, A); in this case we write
O, A |= 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 |= q, for every model I of (O, A), and ‘no’ otherwise.
The OMQ answering problem for DL-Literc is to check, given an OMQ Q = (O, q(x))
with a DL-Literc ontology O, an ABox A and a tuple a in ind(A), whether a is a certain
answer to Q over A.
3 Relationship to Other Fragments of FO
Every DL-Litebool
bool ontology is easily seen to be equivalent to a sentence in the two-
variable fragment of FO, and every DL-Liteg-bool bool 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
g-bool
description of the expressivity of both DL-Litebool bool and DL-Litebool ontologies within
those more familiar description logics.
Denote by FO2 the fragment of first-order logic with unary and binary relation sym-
bols, the equality symbol, no function symbols, and the individual variables x and y
only. FO2 is well understood [13], in particular, it is known to have the finite model
property, and the satisfiability problem for FO2 -formulas is NE XP T IME-complete. It is
straightforward to show that DL-Liteboolbool is a fragment of FO2 in the sense that every
DL-Litebool
bool CI and RI is equivalent to a sentence in FO2 . Moreover, the translation is
linear, and so the satisfiability problem for DL-Litebool bool KBs is in NE XP T IME . To an-
swer the question how much of FO2 is captured by DL-Litebool bool , we consider another
description logic in which roles have a similar status to concepts.
Denote by ALC id,>,∩,¬,− the DL whose roles are built according to the rule
S, S1 , S2 ::= > | id | Pi | S1 u S2 | ¬S | S − ,
and whose concepts are built according to the rule
C, C1 , C2 ::= > | Ai | ∃S.C | C1 u C2 | ¬C,
where S is an ALC id,>,∩,¬,− -role. An ALC id,>,∩,¬,− -CI takes the form C1 v C2 ,
where C1 , C2 are ALC id,>,∩,¬,− -concepts. The semantics of ALC id,>,∩,¬,− is as ex-
pected, with id interpreted in any interpretation I as the relation {(d, d) | d ∈ ∆I }.
ALC id,>,∩,¬,− was introduced in [16], various fragments had been considered be-
fore [15, 11]. It is easy to see that every ALC id,>,∩,¬,− -CI is equivalent to a sentence in
FO2 , and the translation is linear. The converse inclusion holds as well: every sentence
in FO2 is equivalent to an ALC id,>,∩,¬,− -CI, but the known translation introduces an
exponential blow-up [16]. In fact, despite having exactly the same expressive power,
ALC id,>,∩,¬,− behaves differently from FO2 in that satisfiability is still NE XP T IME-
complete but becomes, in contrast to FO2 , E XP T IME-complete if the signature of unary
and binary relation symbols is fixed.
The relationship between ALC id,>,∩,¬,− and DL-Litebool bool can be stated in a pre-
id,>,∩,¬,−
cise way: DL-Liteboolbool is ALC without the relation id. Observe that we clearly
cannot express ALC id,>,∩,¬,− -CIs such as A v ∃¬id.A in DL-Litebool bool . Denote by
ALC >,∩,¬,− the language ALC id,>,∩,¬,− without the relation id. We say that an ontol-
ogy O is a model conservative extension of an ontology O0 if O |= 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-Litebool
bool 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-Litebool
bool .
>,∩,¬,−
Proof. Clearly, every CI in DL-Litebool
bool is also in ALC (∃S abbreviates ∃S.>).
Every role inclusion S1 u · · · u Sk v Sk+1 t · · · t Sk+m in DL-Litebool
bool is equivalent
to the ALC >,∩,¬,− -CI ∃(S1 u · · · u Sk u ¬(Sk+1 t · · · t Sk+m )).> v ⊥.
Conversely, assume an ALC >,∩,¬,− ontology O is given. Using standard normali-
sation one can construct in linear time an ALC >,∩,¬,− ontology with CIs of the form
A v ∀S.B, ∀S.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 ∀S.B by
S v Q t R, ∃Q− v B, A v ¬∃R,
where Q and R are fresh role names, and any CI ∀S.B v A by
¬A v ∃R, R v S, ∃R− 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-Litebool
bool 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 ∈ {x, y, xy}, ψ is in GF2 , and G is in atomic formula in FO2 containing all
free variables in ψ, then ∃v (G ∧ ψ) is in GF2 .
id,>,∩,¬,−
It is not difficult to see that GF2 corresponds to the fragment ALC guarded of the DL
ALC id,>,∩,¬,− in which every role expression is either > or contains a guard: a top-
level conjunct that is either id, a role name, or the inverse of a role name. The fragment
∩,¬,−
DL-Liteg-bool id,>,∩,¬,−
bool clearly lies within ALC guarded , the fragment of ALC guarded 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-Liteg-bool
bool ontology, one can compute in linear time an
∩,¬,− ∩,¬,−
equivalent ALC guarded ontology. (ii) For every ALC guarded ontology, one can compute
in polynomial time a model conservative extension in DL-Liteg-bool
bool .
4 Complexity of Satisfiability
It is known [9, 1] that satisfiability checking is NP-complete for DL-Litecore
bool KBs, P-
complete for DL-Litecore core core
horn KBs, and NL-complete for DL-Litekrom and DL-Litecore KBs.
Theorem 3. Satisfiability checking is NE XP T IME-complete for DL-Litebool
bool KBs and
E XP T IME-complete for DL-Liteg-bool
bool KBs.
Proof. For DL-Litebool
bool , NE XP T IME -completeness follows from Theorem 1 and [15,
Theorem 14]. For DL-Liteg-bool bool , the E XP T IME upper bound follows from the fact that
satisfiability of DL-Liteg-bool
bool KBs is reducible to satisfiability of guarded FO-formulas
with at most binary predicates, which is known to be in E XP T IME [12]. The matching
lower bound can be established using the encoding of A v ∀S.B given in the proof of
Theorem 1 and the proof of [4, Theorem 3.27].
Now we consider ontologies with Krom and Horn role inclusions. For an ontol-
ogy O, let role± (O) = {P, P − | P is a role name in O}. We also set (P − )− = P .
Suppose J = (∆J , ·J ) is an interpretation. Denote by tJ (x) the concept type of
x ∈ ∆J in J , which comprises all B with x ∈ B J and all ¬B with x ∈ / B J , for basic
concepts B of the form A, for concept names in O, and ∃S, for S ∈ role± (O). Simi-
larly, we denote by r J (x, y) the role type of (x, y) ∈ ∆J × ∆J in J , which comprises
all S with (x, y) ∈ S J and all ¬S with (x, y) ∈ / S J , for S ∈ role± (O).
Lemma 1. For every satisfiable DL-Litekrom
bool KB K = (O, A), there exists a model
I = (∆I , ·I ) of K such that
– ∆I = ind(A) ∪ {wSi | S ∈ role± (O) and 0 ≤ i < 3},
– if a ∈ (∃S)I , then (a, wS0 ) ∈ S I , for any a ∈ ind(A) and any S ∈ role± (O),
– if wRi
∈ (∃S)I , then (wRi
, wSi⊕1 ) ∈ S I , for any R, S ∈ role± (O) and 0 ≤ i < 3,
where ⊕ denotes addition modulo 3. In particular, DL-Litekrom
bool enjoys the linear model
property: |∆I | = |ind(A)| + 3|role± (O)|.
Proof. Suppose DL-Litekrom J J
bool KB K = (O, A) is satisfied in J = (∆ , · ). We con-
struct 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 |= L v L0 .
For each role S in O with S J 6= ∅, we pick wS ∈ ∆J with ∃S − ∈ tJ (wS ); for S
with S J = ∅, 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 ∈ ind(A),
and f (wSi ) = wS , for all S and i. We then set tI (w) = tJ (f (w)), for all w ∈ ∆J .
We now show how to define r I (w, w0 ) for w, w0 ∈ ∆I . The following three cases
need consideration.
– If w = a, w0 = wS0 and ∃S ∈ tJ (w), then we define r I (w, w0 ) by first tak-
ing 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 r J (f (w), f (w0 )). Suppose for definiteness that it is
Sj . Then we add cl(Sj ) to r I (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 r I (w, w0 ) is consistent with O and respects tI (w) and tI (w0 ) in
the sense that R ∈ r I (w, w0 ) implies ∃R ∈ tI (w) and ∃R− ∈ tI (w0 ).
– If w = wR i
, w0 = wSi⊕1 and ∃S ∈ tJ (w), then we define r I (w, w0 ) as above.
– For any other w, w0 not covered above (in particular, if w = a, w0 = wSi and either
i > 0 or ∃S ∈ / tJ (a)), we set r I (w, w0 ) = r J (f (w), f (w0 )).
It is readily checked that the constructed concept types tI (w) and role types r I (w, w0 ),
for w, w0 ∈ ∆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 B † (x), for x ∈ ∆I
and basic concepts B from O, saying that B holds on x in I, and P † (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 ∈ ∆I :
B1† (x) ∧ · · · ∧ Bk† (x) → Bk+1
† †
(x) ∨ · · · ∨ Bk+m (x),
for each CI B1 u · · · u Bk v Bk+1 t · · · t Bk+m in O;
S1† (x, x0 ) ∧ · · · ∧ Sk† (x, x0 ) → Sk+1
† †
(x, x0 ) ∨ · · · ∨ Sk+m (x, x0 ),
for each RI S1 u · · · u Sk v Sk+1 t · · · t Sk+m in O,
†
A (a), for each A(a) ∈ A, and P † (a, b), for each P (a, b) ∈ A,
† † †
(∃S) (a) → S (a, wS0 ) and i
(∃S) (wR ) → S † (x, wSi⊕1 ), for each S and i,
† 0 †
S (x, x ) → (∃S) (x), for each S.
where (Pi− )† (x, x0 ) = Pi† (x0 , x). Note that, if K is a DL-Litekrom
krom 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-Litekrom
bool KB K is satisfiable iff ϕK is satisfiable.
As a consequence, and using the fact that DL-Litekrom krom
horn can express DL-Litebool (as
Krom RIs can simulate Krom CIs, and the latter can express the complements of con-
cepts), we obtain the following complexity results:
Theorem 4. Satisfiability checking is NP-complete for DL-Litekrom krom
bool and DL-Litehorn
krom
KBs, and NL-complete for DL-Litekrom KBs.
Next, we consider DL-Litehorn horn
bool and DL-Litehorn KBs. Note that universal roles de-
fined 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-Litehorn horn .
Lemma 3. Let K = (O, A) be a satisfiable DL-Litehorn
bool KB. Then there is a model
I = (∆I , ·I ) such that
– ∆I ⊆ ind(A) ∪ {aw | a ∈ ind(A), w is a word over wS , for S ∈ role± (O)},
– tI (w1 wS ) = tI (w2 wS ), for any w1 wS and w2 wS in ∆I ,
– if w1 and w2 are not both in ind(A), then (w1 , w2 ) ∈ RI iff there is ∃S ∈ tI (w1 )
such that R ∈ r S , S is minimal with this property w.r.t. v, and w2 = w1 wS , where
r S = {R | O |= S v R}.
I
If K is a DL-Litehorn
horn KB, then B ∈ t (wwS ) iff O |= ∃S
−
v B, for any basic
concept B.
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 ∈ ∆J with {w, w0 } 6⊆ ind(A),
we have
r J (w, w0 ) = r S , for some role S.
Indeed, suppose (w, w0 ) violates this property and w0 ∈ / ind(A). Let r I0 (w, w0 ) =
{S1 , . . . , Sk }. Then we replace w by k copies w1 , . . . , wk0 with the same concept types
0 0
as w0 , and connect w to each wi0 by the roles in r Si 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 ∃R. 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 r Sj . It can be seen that, in the resulting interpretation, the pairs
(wij , wi0 ) satisfy the required property, but now the wij may not satisfy CIs in O (again,
due to some ∃R). 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 {wP , wP − } 6⊆ ind(A) and
r J (wP − , wP ) = r P . 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 uni-
versal 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 [7].
Theorem 5. (i) DL-Litehorn bool satisfiability is poly-time-reducible to FO1 -satisfiability.
(ii) DL-Litehorn
horn satisfiability is poly-time-reducible to Horn-FO1 -satisfiability.
(iii) DL-Litehorn
krom satisfiability is poly-time-reducible to Krom-FO1 -satisfiability.
Proof. (i) Let K = (O, A) be a DL-Litehorn bool KB. We assume without loss of generality
that together with RIs of the form S1 u · · · u Sk v Sk+1 the TBox also contains
S1− u · · · u Sk− v Sk+1
−
, and similarly for S1 u · · · u Sk v ⊥. For each concept A,
fix a unary predicate A and, for each role name P , fix a binary predicate P , two unary
predicates EP and EP − , and two constants wP and wP − . Intuitively, the two constants
are representatives of the range and domain of the role, respectively (if it is non-empty);
the unary predicates of the form A, EP and EP − encode the unary types; the binary
predicate P encodes the binary types of pairs of ABox elements. For a concept C, let
C † (x) be
A(x) if C = A, EP (x) if C = ∃P, EP − (x) if C = ∃P − .
A CI C1 u · · · u Ck v Ck+1 t · · · t Ck+m is then naturally translated into
∀x C1† (x) ∧ · · · ∧ Ck† (x) → Ck+1
† †
(x) ∨ · · · ∨ Ck+m (x) .
We also include the following sentences, for all roles S:
∀x (∃S)† (x) → (∃S − )† (wS ) .
Since we assume that the binary types for (w1 , w2 ) with {w1 , w2 } 6⊆ ind(A) are min-
imal, that is, generated by a single role, RIs are translated into the the following sen-
tences:
∀x (∃S)† (x) → (∃R)† (x) ,
for all roles S and R with O |= S v R;
†
∀x (∃S) (x) → ⊥ , for all roles S with O |= 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 ) → (∃P )† (ai ) ∧ (∃P − )† (aj )
for all pairs ai , aj ∈ ind(A) and all role names P , and
S1 (ai , aj ) ∧ · · · ∧ Sk (ai , aj ) → Sk+1 (ai , aj ), (2)
for all pairs ai , aj ∈ 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-Litehorn horn .
(iii) The translation in (i) for DL-Litehornkrom 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 |= S(ai , aj ) or ⊥ if R, A |= ⊥, 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-Litehorn
bool KBs, and P-comp-
lete for DL-Litehorn
horn and DL-Lite horn
krom KBs.
5 The Complexity of (U)CQ-Answering
In this section, we give a brief survey of results on the combined and data complexity
of answering OMQs with DL-Literc ontologies and (U)CQs, which can mostly be ob-
tained in a rather straightforward way from existing results. We start with undecidability
results, which show that the language DL-Liteboolbool behaves again similarly to the two-
variable fragment of FO and that even in DL-Litekrom krom UCQ answering is undecidable.
The following can be shown using [17, Theorem 1] and the encoding of ∀R.C given in
the proof of Theorem 1:
Theorem 7. Answering OMQs with DL-Litebool
bool ontologies and CQs is undecidable for
combined complexity.
The next result follows from [17, Theorem 3]:
Theorem 8. Answering OMQs with DL-Litekrom
krom ontologies and UCQs is undecidable
for combined complexity.
It remains open whether answering OMQs with DL-Litekrom krom ontologies and CQs is
undecidable. The language DL-Liteg-boolbool can be regarded as a fragment of the guarded
fragment, GF, of FO. Query evaluation for GF was first investigated in [5], where it
was proved that (U)CQ evaluation in GF is in 2E XP T IME for combined complexity. It
follows directly from the results in [8] that a matching lower bound holds already for
DL-Litecore
bool . Thus, we obtain the following:
Theorem 9. Answering OMQs with DL-Liteg-bool bool ontologies and (U)CQs can be done
in 2E XP T IME for combined complexity. It is 2E XP T IME-hard for DL-Litecore
bool ontolo-
gies.
We now sketch the results on data complexity. A coNP-upper bound for (U)CQ eval-
uation in GF for data complexity is proved in [5]. Thus, UCQ answering is in CO NP
for DL-Liteg-bool
bool . A fine-grained analysis of the data complexity at the TBox and even
OMQ level can be obtained from [6, 14]. While the structure of the space of possi-
ble complexity of answering OMQs over GF ontologies and UCQs is wide open (it
corresponds to the complexity of MMSNP2 [6]) and an active area of research in the
constraint satisfaction community, it has recently been proved in the extended version
of [14] that there is a P/CO NP dichotomy for OMQs over the two-variable fragment
GF2 of GF and UCQs (i.e., every such OMQ is either in P or CO NP-complete). As
DL-Liteg-bool
bool is clearly contained in GF2 , we obtain the following:
Theorem 10. Answering any OMQ with a DL-Liteg-bool
bool ontology and a UCQ is either
in P or CO NP-complete for data complexity.
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 appli-
cations 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-Liteg-bool bool lies within
the fragment uGF− 2 (1, =) of GF introduced in [14], we obtain the following analysis
from that paper:
Theorem 11. For every ontology O in DL-Liteg-bool
bool , either every OMQ using O and a
UCQ is datalog-rewritable or there exists such an OMQ for which query answering is
CO NP-hard. Moreover, datalog-rewritability is decidable in NE XP T IME .
We note that a dichotomy between datalog-rewritable and CO NP is quite rare. There
are, for example, ALC TBoxes for which not all OMQs are datalog rewritable but still
in P [14]. Finally, the following (probably folklore) theorem is proved using Lemma 3:
Theorem 12. Every OMQ with a DL-Litehorn horn ontology and a UCQ is FO-rewritable,
and so answering it is in AC0 for data complexity.
Acknowledgements
The work was supported by the EPSRC UK grants EP/S032282/1 and EP/S032207/1.
References
1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and re-
lations. Journal of Artificial Intelligence Research (JAIR) 36, 1–69 (2009)
2. Artale, A., Kontchakov, R., Kovtunova, A., Ryzhikov, V., Wolter, F., Zakharyaschev, M.:
First-order rewritability of temporal ontology-mediated queries. In: Yang, Q., Wooldridge,
M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial In-
telligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. pp. 2706–2712. AAAI
Press (2015), http://ijcai.org/Abstract/15/383
3. Artale, A., Kontchakov, R., Wolter, F., Zakharyaschev, M.: Temporal description logic for
ontology-based data access. In: Rossi, F. (ed.) IJCAI 2013, Proceedings of the 23rd Inter-
national Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013. pp.
711–717. IJCAI/AAAI (2013), http://www.aaai.org/ocs/index.php/IJCAI/
IJCAI13/paper/view/6824
4. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The De-
scription Logic Handbook: Theory, Implementation and Applications. Cambridge University
Press (2003)
5. Bárány, V., Gottlob, G., Otto, M.: Querying the guarded fragment. Logical Methods in Com-
puter Science 10(2) (2014), https://doi.org/10.2168/LMCS-10(2:3)2014
6. Bienvenu, M., ten Cate, B., Lutz, C., Wolter, F.: Ontology-based data access: A study through
disjunctive datalog, CSP, and MMSNP. ACM Transactions on Database Systems 39(4),
33:1–44 (2014)
7. Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Math-
ematical Logic, Springer (1997)
8. Bourhis, P., Manna, M., Morak, M., Pieris, A.: Guarded-based disjunctive tuple-generating
dependencies. ACM Trans. Database Syst. 41(4), 27:1–27:45 (2016), https://doi.
org/10.1145/2976736
9. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning
and efficient query answering in description logics: the DL-Lite family. Journal of Automated
Reasoning 39(3), 385–429 (2007)
10. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Data complexity
of query answering in description logics. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.)
Proceedings, Tenth International Conference on Principles of Knowledge Representation and
Reasoning, Lake District of the United Kingdom, June 2-5, 2006. pp. 260–270. AAAI Press
(2006), http://www.aaai.org/Library/KR/2006/kr06-028.php
11. Gargov, G., Passy, S.: A note on boolean modal logic. In: Petkov, P. (ed.) Mathematical
Logic. Springer, Boston, MA (1990)
12. Grädel, E.: On the restraining power of guards. J. Symb. Log. 64(4), 1719–1742 (1999),
https://doi.org/10.2307/2586808
13. Grädel, E., Kolaitis, P.G., Vardi, M.Y.: On the decision problem for two-variable first-order
logic. Bulletin of Symbolic Logic 3(1), 53–69 (1997), http://www.math.ucla.edu/
\%7Easl/bsl/0301/0301-003.ps
14. Hernich, A., Lutz, C., Papacchini, F., Wolter, F.: Dichotomies in ontology-mediated querying
with the guarded fragment. In: Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI
Symposium on Principles of Database Systems, PODS 2017, Chicago, IL, USA, May 14-19,
2017. pp. 185–199 (2017), https://doi.org/10.1145/3034786.3056108
15. Lutz, C., Sattler, U.: The complexity of reasoning with boolean modal logics. In: Wolter, F.,
Wansing, H., de Rijke, M., Zakharyaschev, M. (eds.) Advances in Modal Logic 3, papers
from the third conference on “Advances in Modal logic,” held in Leipzig, Germany, 4-7
October 2000. pp. 329–348. World Scientific (2000)
16. Lutz, C., Sattler, U., Wolter, F.: Modal logic and the two-variable fragment. In: Fribourg, L.
(ed.) Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Con-
ference of the EACSL, Paris, France, September 10-13, 2001, Proceedings. Lecture Notes
in Computer Science, vol. 2142, pp. 247–261. Springer (2001), https://doi.org/10.
1007/3-540-44802-0\_18
17. Rosati, R.: The limits of querying ontologies. In: Database Theory - ICDT 2007, 11th In-
ternational Conference, Barcelona, Spain, January 10-12, 2007, Proceedings. pp. 164–178
(2007), https://doi.org/10.1007/11965893_12