=Paper=
{{Paper
|id=None
|storemode=property
|title=DL-Lite with Attributes and Sub-Roles (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-745/paper_42.pdf
|volume=Vol-745
|dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleIKR11
}}
==DL-Lite with Attributes and Sub-Roles (Extended Abstract)==
DL-Lite with Attributes and Sub-Roles
(Extended Abstract)
A. Artale,1 A. Ibáñez Garcı́a,1 R. Kontchakov,2 and V. Ryzhikov1
1 2
KRDB Research Centre Dept. of Comp. Science and Inf. Sys.
Free University of Bozen-Bolzano, Italy Birkbeck College, London, UK
{lastname }@inf.unibz.it roman@dcs.bbk.ac.uk
1 Introduction
The DL-Lite family of description logics has recently been proposed and investi-
gated in [5–7] and later extended in [1, 8, 3]. The relevance of the DL-Lite family
is witnessed by the fact that it forms the basis of OWL 2 QL, one of the three
profiles of OWL 2 (http://www.w3.org/TR/owl2-profiles/). According to the offi-
cial W3C profiles document, the purpose of OWL 2 QL is to be the language of
choice for applications that use very large amounts of data.
This paper extends the DL-Lite languages of [3] by relaxing the restriction
on the interaction between cardinality constraints (N ) and role inclusions (or
hierarchies, H). We also introduce a new family of languages, DL-LiteHN α
A
,
α ∈ {core, krom, horn, bool}, extending DL-Lite with attributes (A).
The notion of attributes, borrowed from conceptual modeling formalisms,
introduces a distinction between (abstract) objects and application domain val-
ues, and consequently, between concepts (sets of objects) and datatypes (sets of
values), and between roles (relating objects to objects) and attributes (relating
objects to values). The advantage of the presented languages over DL-LiteA [8]
is that the range restrictions for attributes can be local (and not only global as
in DL-LiteA ). Indeed, DL-LiteHN α
A
has a possibility to express concept inclusion
axioms of the form C v ∀U.T , for an attribute U and its datatype T . In this
way, we allow re-use of the very same attribute associated to different concepts
with different range restrictions. For example, we can say that employees’ salary
is of type Integer, researchers’ salary is in the range 35,000–70,000 (enumeration
type) and professors’ salary in the range 55,000–100,000—while both researchers
and professors are employees. Note that local attributes are strictly more expres-
sive than global ones. For example, concept disjointness (or unsatisfiability) can
be inferred just from datatype disjointness for the same (existentially qualified)
attribute. Since DL-Lite languages have been proved useful in capturing concep-
tual data models [8, 4, 2], the extension with attributes, as presented here, will
generalize their use even further.
We aim at establishing computational complexity of knowledge base satisfi-
ability in these new DLs. In particular we prove the following results:
1. We can relax the restrictions presented in [3] limiting the interaction between
sub-roles and number restrictions without increasing the complexity of rea-
soning as far as the problem is limited to TBox satisfiability checking. As
for KB satisfiability, the presence of the ABox should be taken into account
if we want to preserve the complexity results.
2. The introduction of local range restrictions for attributes is for free for the
languages DL-LiteN A NA NA
bool , DL-Litehorn and DL-Litecore .
2 The Description Logic DL-LiteHN
bool
A
The language of DL-LiteHN bool
A
contains object names a0 , a1 , . . ., value names
v1 , v2 , . . ., concept names A0 , A1 , . . ., role names P0 , P1 , . . ., attribute names
U0 , U1 , . . ., and datatype names T0 , T1 , . . .. Complex roles R and concepts C
are defined below:
R ::= Pi | Pi− ,
B ::= > | ⊥ | Ai | ≥ q R | ≥ q Ui
C ::= B | ¬C | C1 u C2 ,
where q is a positive integer. The concepts of the form B are called basic concepts.
A DL-LiteHN bool
A
TBox, T , is a finite set of concept, role, attribute and
datatype inclusion axioms of the form:
C1 v C2 , C v ∀U. T, R1 v R2 , U v U 0, T v T 0, T u T 0 v ⊥,
and an ABox, A, is a finite set of assertions of the form:
Ak (ai ), ¬Ak (ai ), Pk (ai , aj ), ¬Pk (ai , aj ), Uk (ai , vj ) and Tk (vj ).
We standardly abbreviate ≥ 1 R and ≥ 1 U by ∃R and ∃U , respectively. Absence
of an attribute (i.e., C v ∀U. ⊥) can be expressed as C u ∃U v ⊥.
Together, a TBox T and an ABox A constitute the DL-LiteHN bool
A
knowledge
base (KB) K = (T , A). In the following, we denote by role(K) and att(K) the
sets of role and attribute names occurring in K, respectively; role ± (K) denotes
the set {Pk , Pk− | Pk ∈ role(K)}.
Semantics. As usual in description logic, an interpretation, I = (∆I , ·I ), con-
sists of a nonempty domain ∆I and an interpretation function ·I . The interpre-
tation domain ∆I is the union of two non-empty disjoint sets: the domain of
objects ∆IO and the domain of values ∆IV . We assume that all interpretations
agree on the semantics assigned to each datatype Ti , as well as on each constant
vi . In particular, TiI = val(Ti ) ⊆ ∆IV is the set of values of datatype Ti , and each
vi is interpreted as one specific value, denoted val(vi ), i.e., viI = val(vi ) ∈ val(Ti ).
Furthermore, ·I assigns to each object name ai an element aIi ∈ ∆IO , to each
concept name Ak a subset AIk ⊆ ∆IO of the domain of objects, to each role
name Pk a binary relation PkI ⊆ ∆IO × ∆IO over the domain of objects, and to
each attribute name Uk a binary relation UkI ⊆ ∆IO × ∆IV . We adopt here the
unique name assumption (UNA): aIi 6= aIj , for all i 6= j. The role and concept
constructs are interpreted in I in the standard way:
(Pk− )I = {(y, x) ∈ ∆IO × ∆IO | (x, y) ∈ PkI }, (inverse role)
I
> = ∆IO , (domain of objects)
I
⊥ = ∅, (the empty set)
I
= x ∈ ∆IO | ]{y | (x, y) ∈ RI } ≥ q ,
(≥ q R) (at least q R-successors)
I
= x ∈ ∆IO | ]{v | (x, v) ∈ U I } ≥ q ,
(≥ q U ) (at least q U -attributes)
I
= x ∈ ∆IO | ∀v. (x, v) ∈ U I → v ∈ T I ,
(∀U. T ) (attribute value restriction)
I
(¬C) = ∆IO \ C I , (not in C)
I
(C1 u C2 ) = C1I ∩ C2I , (both in C1 and in C2 )
where ]X is the cardinality of X. The satisfaction relation |= is also standard:
I |= C1 v C2 iff C1I ⊆ C2I , I |= R1 v R2 iff R1I ⊆ R2I ,
I |= T1 v T2 iff T1I ⊆ T2I , I |= U1 v U2 iff U1I ⊆ U2I ,
I |= T1 u T2 v ⊥ iff T1I ∩ T2I = ∅, I |= Pk (ai , aj ) iff (aIi , aIj ) ∈ PkI ,
I |= Ak (ai ) iff aIi ∈ AIk , I |= ¬Pk (ai , aj ) iff (aIi , aIj ) ∈
/ PkI
I |= ¬Ak (ai ) iff aIi ∈
/ AIk , I |= Uk (ai , vj ) iff (aIi , vjI ) ∈ UkI ,
I |= Tk (vj ) iff vjI ∈ TkI .
A KB K = (T , A) is said to be satisfiable (or consistent) if there is an interpre-
tation, I, satisfying all the members of T and A. In this case we write I |= K
(as well as I |= T and I |= A) and say that I is a model of K (of T and A).
2.1 Fragments of DL-LiteHN
bool
A
We consider various syntactical restrictions on the language of DL-LiteHN bool
A
along two axes: (i) the Boolean operators (bool ) on concepts, (ii) the role and
attribute inclusions (H). Similarly to classical logic, we adopt the following def-
initions. A TBox T will be called a Krom TBox 1 if its concept inclusions are
restricted to:
B1 v B2 , B1 v ¬B2 and ¬B1 v B2 , (Krom)
(here and below all the Bi and B are basic concepts). T will be called a Horn
TBox if its concept inclusions are restricted to:
l
Bk v B. (Horn)
k
Finally, we call T a core TBox if its concept inclusions are restricted to:
B1 v B2 and B1 u B2 v ⊥. (core)
1
The Krom fragment of first-order logic consists of all formulas in prenex normal form
whose quantifier-free part is a conjunction of binary clauses.
As B1 v ¬B2 is equivalent to B1 u B2 v ⊥, core TBoxes can be regarded as
sitting in the intersection of Krom and Horn TBoxes. In this paper we study the
following logics, for α ∈ {core, krom, horn, bool}:
DL-LiteHN A HN A
krom , DL-Litehorn , DL-Litecore
HN A
are the fragments of DL-LiteHN
bool
A
with Krom, Horn, and core TBoxes, respectively;
DL-LiteHN α is the fragment of DL-LiteHN
α
A
without attributes and datatypes;
DL-LiteN
α
A
is the fragment of DL-LiteHN
α
A
without role and attribute inclu-
sions.
As shown in [3], reasoning in DL-LiteHN α is already rather costly (ExpTime-
complete) due to the interaction between role inclusions and number restrictions.
However, both of these constructs turn out to be useful for the purposes of
conceptual modeling. By limiting their interplay one can get languages with
a better computational properties [8, 3]. Before presenting such limitations we
need to introduce some notation. For a role R, let inv (R) = Pk− if R = Pk and
inv (R) = Pk if R = Pk− . Given a TBox T we denote by v∗T the reflexive and
transitive closure of the relation {(R, R0 ), (inv(R), inv(R0 )) | R v R0 ∈ T }. We
say that R ≡∗T R0 iff R v∗T R0 and R0 v∗T R. Say that R0 is a proper sub-role
of R in T if R0 v∗T R and R 6v∗T R0 . A proper sub-role R0 of R is said to be a
direct sub-role of R if there is no other proper sub-role R00 of R such that R0 is
a proper sub-role of R00 ; the set of direct sub-roles of R is denoted as dsub T (R).
The language DL-Lite(HN α
)
[3] is the result of imposing the following syntactic
HN
restriction on DL-Liteα TBoxes T :
(inter) if R has a proper sub-role in T then T contains no negative occurrences
of number restrictions ≥ q R or ≥ q inv (R) with q ≥ 2
(an occurrence of a concept on the right-hand (left-hand) side of a concept
inclusion is called negative if it is in the scope of an odd (even) number of
negations ¬; otherwise it is called positive). We will formulate two alternative
versions of restriction (inter).
Definition 1. Given a TBox T and a role R ∈ role ± (T ), we define the following
parameters:
ubound (R, T ) = min {∞} ∪ {q − 1 | q ≥ 2 and ≥ q R occurs negatively in T } ,
lbound (R, T ) = max {0} ∪ {q | ≥ q R occurs positively in T } ,
rank (R, T ) = max lbound (R, T ), R0 ∈dsub T (R) rank (R0 , T ) ,
P
rank (R, A) = max {0}∪{n | Ri (a, ai ) ∈ A, Ri v∗T R, for distinct a1 , . . . , an } .
Consider the languages obtained from DL-LiteHN
α by imposing one of the fol-
lowing two restrictions:
(inter1) for every R ∈ role ± (T ), if R has a proper sub-role in T then
ubound (R, T ) ≥ rank (R, T );
(inter2) for every R ∈ role ± (T ), if R has a proper sub-role in T then
ubound (R, T ) ≥ rank (R, T ) + max{1, rank (R, A)}.
language (inter) [3] (inter1) (inter2) non-restrict.
DL-LiteHN
core NLogSpace [3] NLogSpace [Th.1]
DL-LiteHN
horn PTime [3] PTime [Th.1]
DL-LiteHN NLogSpace [3] ≥NP [Th.2] NLogSpace [Th.1] ExpTime [3]
krom
HN
DL-Litebool NP [3] NP [Th.1]
DL-LiteHN
core
A
NLogSpace [Th.3] NLogSpace [Th.3]
DL-LiteHN
horn
A
PTime [Th.3] PTime [Th.3]
DL-LiteHN A
NP [Th.4] ≥NP [Th.2] NP [Th.4] ExpTime
krom
HN A
DL-Litebool NP [Th.3] NP [Th.3]
DL-LiteN A
core NLogSpace [Th.3]
DL-LiteN A
horn PTime [Th.3]
DL-LiteN A NA NA NA NP [Th. 4]
krom
DL-LiteN A
bool NP [Th.3]
Table 1: Complexity of DL-Lite logics (NA = Non-Applicable).
These new restrictions are in some way weaker than (inter) and, for ex-
ample, allow for the specialization of functional roles: KB K = (T , A) with
T = {≥ 2 R v ⊥, R1 v R2 , R2 v R}, and A = {R(a, b), R1 (a1 , b1 ), R2 (a2 , b2 )}
does not satisfy (inter), but it satisfies both (inter1) and (inter2). Finally,
the above restrictions can also be applied to sub-attributes in the languages
DL-LiteHN
α
A
. Table 1 summarizes the obtained complexity results (with numer-
ical parameters q coded in binary).
3 Reasoning in DL-LiteHN
α
In this section, we investigate the complexity of deciding KB satisfiability in
languages DL-LiteHNα under the restrictions (inter1) and (inter2), respectively.
We adapt the proof presented in [3], where a DL-LiteHN bool KB K = (T , A)
is encoded into a sentence K‡e in the one-variable first-order logic QL1 . We
use a slightly longer but simpler encoding. Every ai ∈ ob(A) is associated to the
individual constant ai of QL1 , and every concept name Ai to the unary predicate
Ai (x). For each concept ≥ q R in K we introduce a fresh unary predicate Eq R(x).
For each role name Pk ∈ role ± (K), two individual constants dpk and dp− k are
introduced, as representatives of the objects in the domain and range of Pk ,
respectively. The encoding C ∗ of a concept C is defined inductively:
⊥∗ = ⊥, (Ai )∗ = Ai (x), (≥ q R)∗ = Eq R(x),
>∗ = >, (¬C)∗ = ¬C ∗ (x), (C1 u C2 )∗ = C1∗ (x) ∧ C2∗ (x).
The QL1 sentence encoding the knowledge base K is defined as follows:
^
K ‡e ∀x T ∗ (x) ∧ T R (x) ∧ ∧ A‡e .
= R (x) ∧ δR (x)
R∈role ± (K)
Formulas T ∗ (x), the δR (x), for R ∈ role± (K), and T R (x) encode the TBox T :
^ ^
T ∗ (x) = C1∗ (x) → C2∗ (x) ,
δR (x) = Eq0 R(x) → Eq R(x) ,
C1 vC2 ∈T q,q 0 ∈QR
T, q 0 >q
^ ^
T R (x) = Eq R(x) → Eq R0 (x) ,
Rv∗ 0 R
T R q∈QT
0
0 ∗
where QR R
T contains 1, all q such that ≥ q R occurs in T and all QT , for R vT R.
‡e
Sentence A encodes the ABox A:
^ ^ ^ ^
A‡e = Ak (ai ) ∧ ¬Ak (ai ) ∧ EqR,a
e R(a) ∧ ⊥,
Ak (ai )∈A ¬Ak (ai )∈A a,a0 ∈ob(A) ¬Pk (ai ,aj )∈A
R 0 v∗ 0 0
T R, R (a,a )∈A
R(ai ,aj )∈A, Rv∗ T Pk
e
where qR,a is the maximum number in QR e
T such that there are qR,a many distinct
ai with Ri (a, ai ) ∈ A and Ri v∗T R. For each R ∈ role ± (K), we also need the
following formula expressing the fact that the range of R is not empty whenever
its domain is non-empty:
R (x) = E1 R(x) → inv (E1 R(dr)),
where inv (E1 R(dr)) is E1 Pk− (dp− −
k ) if R = Pk and E1 Pk (dpk ) if R = Pk .
Lemma 1. A DL-LiteHN bool knowledge base under restriction (inter2) is satisfi-
able iff the QL1 -sentence K‡e is satisfiable.
Proof. (Sketch) The only challenging direction is (⇐). To prove it, we adapt the
proofs of Theorem 5.2 and Lemma 5.14 in [3]. The idea of the proof is to construct
a DL-LiteHN ‡e
bool interpretation I, from M, the minimal Herbrand model of K . We
1
denote the interpretations of unary predicates P and constants a of QL in M
by P M and aM , respectively. Let D = ob(A) ∪ {dpk , dp−
k | Pk ∈ Srole(K)} be the
∞
domain of M. Then I = (∆I , ·I ) is defined inductively: ∆I = m=0 Wm , such
I
that W0 is the set D0 = ob(A), and for every ai ∈ ob(A), ai = aM i . Each set
Wm+1 , m ≥ 0, is constructed by adding to Wm fresh copies of certain elements
from D \ ob(A). The extensions AIk of concept names Ak are defined by taking
AIk = {w ∈ ∆I | M |= A∗k [cp(w)]}, (1)
where cp(w) is the element d ∈ D of which w is a copy. S∞
The interpretation for each role Pk , is defined inductively as PkI = m=0 Pkm ,
where Pkm ⊆ Wm × Wm , along with the construction of ∆I . The initial interpre-
tation for each role name Pk is defined as follows:
∗
Pk0 = {(aM M
i , aj ) ∈ W0 × W0 | R(ai , aj ) ∈ A and R vT Pk }. (2)
For every R ∈ role ± (K), the required R-rank r(R,
d) of d ∈ D is defined by taking
r(R, d) = max {0} ∪ {q ∈ QR T | M |= Eq R[d]} . The actual R-rank rm (R, w) of
a point w ∈ ∆I at step m is
(
]{w0 ∈ Wm+1 | (w, w0 ) ∈ Pkm+1 }, if R = Pk ,
rm (R, w) =
]{w0 ∈ Wm+1 | (w0 , w) ∈ Pkm+1 }, if R = Pk− .
Assume that Wm and Pkm , m ≥ 0, have been already defined. Let Wm+1 = ∅ and
Pkm+1 = ∅, for each role name Pk . If we had rm (R, w) = r(R, cp(w)), for each role
R and w ∈ Wm , then the interpretation we need would be constructed. However,
the actual rank of some points could still be smaller than the required rank. We
cure these defects by adding R-successors for them. Note that the ‘curing’ process
for a given w and R, not only increases the actual R-rank of w, but also all its
R0 -ranks, for all R v∗T R0 . At this point we adapt the construction in [3] to
obtain the interpretation I we are intending. For each Pk ∈ role(K), we consider
two sets of defects in Pkm : Λmk = {w ∈ Wm \ Wm−1 | rm (Pk , w) < r(Pk , cp(w))}
and Λm−k = {w ∈ W m \ W m−1 | rm (Pk− , w) < r(Pk− , cp(w))}.
In each equivalence class [R] = {S | S ≡∗T R} we select a single role, a
representative. Let G = (Rep ∗T , E) be a directed graph such that Rep ∗T is the
set of representatives and (R, R0 ) ∈ E iff R is a proper sub-role of R0 . Clearly, G
is a directed acyclic graph and so, by a topological sort, one can assign to each
representative a unique number smaller than the number of all its descendants in
G. We use the ascending total order induced on G when choosing an element Pk
in Rep ∗T , and extend in that way Wm and Pkm to Wm+1 and Pkm+1 , respectively.
0
(Λm m
k ) Let w ∈ Λk , q = r(Pk , cp(w)) − rm (Pk , w), d = cp(w). There is q ≥ q > 0
− −
with M |= Eq0 Pk [d]. Then, M |= E1 Pk [d] and M |= E1 Pk [dpk ]. In this
case we take q fresh copies w10 , . . . , wq0 of dp−k , add them to Wm+1 and for
each 1 ≤ i ≤ q, set cp(wi0 ) = dp−k , add the pairs (w, wi0 ) to each Pjm+1 with
Pk v∗T Pj and the pairs (wi0 , w) to each Pjm+1 with Pk− v∗T Pj (note that by
adding pairs to Pjm+1 we change its the actual rank);
m− − −
(Λk ) This rule is the mirror image of (Λm k ): Pk and dpk are replaced with Pk
and dpk , respectively.
We need to show that, for all w ∈ ∆I and all ≥ q R in T ,
(a1 ) if ≥ q R occurs positively in T then M |= Eq R[cp(w)] implies w ∈ (≥ q R)I ;
(a2 ) if ≥ q R occurs negatively in T then w∈(≥ q R)I implies M |= Eq R[cp(w)].
Consider first w ∈ W0 . It should be clear that actual R-rank of w
r0 (R, w) ≤ rank(R, A) + R0 ∈dsubT (R) rank(R0 , T )
P
and so, by (inter2), the total number of R-successors before we cure the de-
fects does not exceed ubound(R, T ). If ubound(R, T ) = ∞ then there are no
negative occurrences of ≥ q R with q ≥ 2 and, although may have rm (R, w) ≥
r(R, cp(w)) after curing the defects of R, both (a1 ) and (a2 ) hold. Otherwise,
we have ubound(R, T ) + 1 ∈ QR R
T and so, by (inter2), max QT > rank(R, T ) +
R
rank(R, A), whence r0 (R, w) < max QT . So, as r(R, cp(w)) ≤ lbound(R, T ) and
lbound(R, T ) < ubound(R, T ) < max QR T , after curing the defect, we will have
rm (R, w) = r(R, cp(w)), for all m > 0, and both (a1 ) and (a2 ) hold. The case
with w ∈ Wm0 \ Wm0 −1 , for m0 > 0 is similar, only now
rm0 (R, w) ≤ 1 + R0 ∈dsubT (R) rank(R0 , T ).
P
Finally, we show that I |= ϕ for each ϕ ∈ K. For ϕ = Ak (ai ), ϕ = ¬Ak (ai )
the claim is by the definition of AIk . For ϕ = ¬Pk (ai , aj ), we have (ai , aj ) ∈ PkI
iff (ai , aj ) ∈ Pk0 iff R(ai , aj ) ∈ A and R v∗T Pk . By induction on the structure
of concepts and (a1 ) and (a2 ), one can show that I |= C1 v C2 whenever
M |= ∀x(C1∗ (x) → C2∗ (x)), for each ϕ = C1 v C2 . Finally, I |= ϕ holds by
definition in case ϕ = R1 v R2 ∈ T .
Theorem 1. Under restriction (inter2), checking KB satisfiability is NP-
complete in DL-LiteHN HN
bool , PTime-complete in DL-Litehorn and NLogSpace-
HN HN
complete in both DL-Litekrom and DL-Litecore .
We now consider the case where the restriction (inter1) is imposed on the
interaction between sub-roles and number restrictions. In presence of an ABox,
(inter2) restricts the number of R-successors in the ABox, which appears to be
a strong constraint on the instances of the ABox. On the other hand, the less
restrictive condition (inter1), which does not impose any bound on R-successors
in the ABox, does not come for free, as shown by the following theorem:
Theorem 2. Under restriction (inter1), checking KB satisfiability is NP-hard
even in DL-LiteHN
core .
Proof. We show that graph 3-colorability can be reduced to KB satisfiability.
Let G = (V, E) be a graph with vertices V and edges E and {r, g, b} be three
colors. Consider the following KB K = (T , A) with role names vi and w and
object names o, r, g, b and the xi , for each vertex vi ∈ V :
T ={≥ (|V | + 4) w v ⊥} ∪ {vi v w, B1 v ∃vi , B2 u ∃vi− v ⊥ | vi ∈ V } ∪
{∃vi− u ∃vj− v ⊥ | (vi , vj ) ∈ E},
A ={B1 (o), w(o, r), w(o, g), w(o, b)} ∪ {w(o, xi ), B2 (xi ) | vi ∈ V }.
It can be shown that K is satisfiable iff G is 3-colorable.
4 Reasoning with Attributes
In this section we study the effect of extending DL-Lite with attributes. In par-
ticular, we show that for the Bool, Horn and core cases the addition of attributes
does not change the complexity of KB satisfiability.
Theorem 3. KB satisfiability is NP-complete in DL-LiteN A
bool , PTime-complete
NA NA
in DL-Litehorn and NLogSpace-complete in DL-Litecore .
Under restriction (inter2), checking KB satisfiability is NP-complete in
DL-LiteHN A HN A
bool , PTime-complete in DL-Litehorn and NLogSpace-complete in
HN A
DL-Litecore .
Proof. (Sketch) We encode a DL-LiteHN α
A
KB K = (T , A) in a QL1 sentence
‡a
K in a way similar to the translation used in Lemma 1. Denote by val (A) the
set of all value names that occur in A. Similarly to roles, we define the sets QU
T
of natural numbers for all occurrences of ≥ q U (including sub-attributes). We
need a unary predicate Eq U (x), for each attribute name U and q ∈ QUT , denoting
the set of objects with at least q values of attribute U . We also need, for each
attribute name U and each datatype T , a unary predicates U T (x), denoting all
objects that may have attribute U values only of datatype T . Following this
intuition, we extend ·∗ by the following two statements:
(≥ q U )∗ = Eq U (x) and (∀U.T )∗ = U T (x).
The QL1 sentence encoding the KB K is defined as follows:
^ 2
K‡a = K‡e ∧ ∀x T U (x) ∧ 1 2
∧ A ‡a ∧ A ‡a ,
δU (x) ∧ αU (x) ∧ αU (x)
U ∈att(K)
where K‡e is as before, T U (x), δU (x) and A‡a are similar to T R (x), δR (x) and
A‡e , but rephrased for attributes and their inclusions. The new types of ABox
assertions require the following formula:
2 ^ ^ ^
A‡a =
U T (ai ) → T vj ∧ T vj ,
Uk (ai ,vj )∈A datatype T T (vj )∈A
where T vj is a propositional variable for each datatype T and each vj ∈ val (A).
1 2
The two additional formulas, αU (x) and αU (x), capturing datatype inclusions
and disjointness constraints are:
^
1
U T (x) → U T 0 (x) ,
αU (x) =
T vT 0 ∈T
^ ^
2
U T (x) ∧ U T 0 (x) ∧ E1 U (x) → ⊥ ∧ T v ∧ T 0v → ⊥ .
αU (x) =
T uT 0 v⊥∈T v∈val(A)
2
We would like to note here that the formula αU (x) for disjoint datatypes demon-
strates a subtle interaction between attribute range constraints ∀U.T and mini-
mal cardinality constraints ∃U .
We show that K is satisfiable iff the QL1 -sentence K‡a is satisfiable. For (⇐),
let M |= K‡a . We construct a model I = (∆IO ∪ ∆IV , ·I ) of K similarly to the way
we proved Lemma 1 but this time datatypes will have to be taken into account:
let ∆IO be defined inductively as before and ∆IO = val (A) ∪ V . The set V will
be constructed starting from val (A) in order to ‘cure’ the attribute successors
as follows. For each datatype T and each attribute U , let
T 0 = {v ∈ val (A) | M |= T v} and U 0 = {(a, v) | U (a, v) ∈ A}.
For every attribute U ∈ att(K), we can define the required U -rank r(U, d) of
d ∈ D and the actual U -rank r0 (R, w) of w ∈ ∆IO as before, treating U as a role
name (the only difference is that there will be only one step, and so, the actual
rank is needed only for step 0). We can also consider the equivalence relation
induced by the sub-attribute relation in T , then we can choose representatives
and a linear order on them respecting the sub-attribute relation of T . We can
start from the smaller attributes and ‘cure’ their defects. Let w ∈ ∆IO and
q = r(U, cp(w)) − r0 (U, w) > 0. Take q fresh elements v1 , . . . , vq , add those
fresh values to V , add pairs (w, v1 ), . . . , (w, vq ) to U 0 and add v1 , . . . , vq to T 0
for each datatype T with M |= U T [cp(w)]. Let U I and T I be the resulting
relations. Now, it can be shown that if M |= K‡a then I |= ϕ for every ϕ ∈ K.
We only note here that fresh values vj cannot be added to two disjoint datatypes
T and T 0 because of formula αU 2
(x).
Now, given a KB with a Bool or Horn TBox, K‡a is a universal one-variable
formula or a universal one-variable Horn formula, respectively, which immedi-
ately gives the NP and PTime upper complexity bounds for the Bool and Horn
fragments. The NLogSpace upper bound for KBs with core TBoxes is not so
2
straightforward because αU (x) is not a binary clause. In this case we note that
K is still a universal one-variable Horn formula and therefore, K‡a is satisfiable
‡a
iff it is true in the ‘minimal’ model. The minimal model can be constructed in the
bottom-to-top fashion by using only positive clauses of K‡a (i.e., clauses of the
form ∀x (B1 (x) ∧ · · · ∧ Bk (x) → H(x))) and then checking whether the negative
clauses of K‡a (i.e., clauses of he form ∀x (B1 (x) ∧ · · · ∧ Bk (x) → ⊥)) hold in the
constructed model. By inspection of the structure of K‡a , one can see that all
its positive clauses are in fact binary, and therefore, whether an atom is true in
its minimal model or not can be checked in NLogSpace.
It is of interest to note that the complexity of KB satisfiability increases in
the case of Krom TBoxes:
Theorem 4. KB satisfiability is NP-complete in DL-LiteN A
krom , and so, in
HN A
DL-Litekrom even under (inter) and (inter2).
2
Proof. (Sketch) The proof exploits the ternary disjointness formula αU (x) in
K‡a . In fact, if T u T 0 v ⊥ ∈ T then the following concept inclusion, although
not in the syntax of DL-LiteN A 2
krom , is a logical consequence of T (cf. αU (x)):
∀U.T u ∀U.T 0 u ∃U v ⊥.
Vm
Using such ternary intersections one can encode 3SAT. Let ϕ = i=1 Ci be a
3CNF, where the Ci are ternary clauses over variables p1 , . . . , pn . Now, suppose
pji1 ∨ ¬pji2 ∨ pji3 is the ith clause of ϕ. It is equivalent to ¬pji1 ∧ pji2 ∧ ¬pji3 → ⊥
and so, can be encoded as follows:
Ti1 u Ti2 v ⊥, ¬Aji1 v ∀Ui .Ti1 , Aji2 v ∀Ui .Ti2 , ¬Aji3 v ∃Ui ,
where the A1 , . . . , An are concept names for the variables p1 , . . . , pn , and Ui is
an attribute and Ti1 and Ti2 are datatypes for the ith clause (note that Krom
concept inclusions of the form ¬B v B 0 are required, which is not allowed in
the core TBoxes). Let T consist of all such inclusions for clauses in ϕ. It can be
seen that ϕ is satisfiable iff T is satisfiable.
5 Conclusions
We studied two different extensions of the DL-Lite logics. First, local attributes
allow to use the same attribute associated to different concepts with different
datatype range restrictions. We showed that the extension with attributes is
harmless with the only notable exception of the Krom fragment, where the com-
plexity rises from NLogSpace to NP.
Second, we consider weak syntactic restrictions on interaction between cardi-
nality constraints and role inclusions and study their impact on the complexity
of satisfiability. For example, under (inter) [3], roles with sub-roles cannot have
maximum cardinality constraints. We present two alternative restrictions, which
coincide without ABoxes, and show that the complexity of TBox satisfiability
under them coincides with the complexity of TBox satisfiability without role in-
clusions. However, if we want to preserve complexity of KB reasoning, condition
(inter2) imposes a bound on the number R-successors in the ABox. Indeed,
under the weaker condition (inter1) complexity of KB satisfiability rises to at
least NP (even for the core fragment).
As a future work, we intend to fill the gaps in Table 1 and, in particular, to
see whether the NP-hardness results have a matching upper bound. We are also
working on query answering in the languages with attributes.
References
1. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. DL-Lite in the
light of first-order logic. In Proc. of the 22nd Nat. Conf. on Artificial Intelligence
(AAAI 2007), pages 361–366, 2007.
2. A. Artale, D. Calvanese, and A. Ibáñez-Garcı́a. Full satisfiability of UML class
diagrams. In Proc. of the 29th International Conference on Conceptual Modeling
(ER-10), 2010.
3. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The DL-Lite family
and relations. J. of Artificial Intelligence Research, 36:1–69, 2009.
4. A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. Complexity of
reasoning over temporal data models. In Proc. of the 29th International Conference
on Conceptual Modeling (ER-10), 2010.
5. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. DL-Lite:
Tractable description logics for ontologies. In Proc. of the 20th Nat. Conf. on
Artificial Intelligence (AAAI 2005), pages 602–607, 2005.
6. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Data com-
plexity of query answering in description logics. In Proc. of the 10th Int. Conf.
on the Principles of Knowledge Representation and Reasoning (KR 2006), pages
260–270, 2006.
7. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Inconsis-
tency tolerance in P2P data integration: An epistemic logic approach. Information
Systems, 33(4):360–384, 2008.
8. A. Poggi, D. Lembo, D. Calvanese, G. De Giacomo, M. Lenzerini, and R. Rosati.
Linking Data to Ontologies. J. on Data Semantics, X:133–173, 2008.