=Paper=
{{Paper
|id=None
|storemode=property
|title=Extending DL-Lite_A with (Singleton) Nominals
|pdfUrl=https://ceur-ws.org/Vol-1014/paper_46.pdf
|volume=Vol-1014
|dblpUrl=https://dblp.org/rec/conf/dlog/HaddadC13
}}
==Extending DL-Lite_A with (Singleton) Nominals==
https://ceur-ws.org/Vol-1014/paper_46.pdf
Extending DL-Lite A with (Singleton) Nominals
Maxim G. Haddad and Diego Calvanese
KRDB Research Centre for Knowledge and Data
Free University of Bozen-Bolzano
Piazza Domenicani 3, Bolzano, Italy
lastname @inf.unibz.it
Abstract. In this paper we study the extension of description logics
of the DL-Lite family with singleton nominals, which correspond in
OWL 2 to the ObjectHasValue construct. Differently from arbitrary (non-
singleton) nominals, which make query answering intractable in data
complexity, we show that both knowledge base satisfiability and con-
junctive query answering stay first-order rewritable when DL-LiteA is
extended with singleton nominals. Our technique is based on a practi-
cally implementable algorithm based on rewriting rules, in the style of
those implemented in current state-of-the-art OBDA systems based on
DL-Lite, such as Quest. This allows us to follow the tradition of the
DL-Lite family for employing relational database technology for query
answering with optimal data complexity.
1 Introduction
The DL-Lite family [7] is a family of descriptions logics (DLs) which is designed
for optimal data complexity of reasoning and query answering, while maintaining
enough expressive power to capture basic ontology and conceptual data modeling
languages [6]. It is at the basis of the OWL 2 QL profile of the Web Ontology
Language (OWL) [11].
The DL-Lite family has been investigated thoroughly in recent years, and
several extensions with respect to the original set of constructs studied in [7]
have been proposed [1,5,14,8]. In particular, DL-Lite A [12,6] is a significant
representative of the DL-Lite family, featuring the the possibility of expressing
both functionality of roles and role inclusion assertions.
Nominals, i.e., concepts interpreted as a singleton, are a significant construct
in DLs, investigated both for expressive DLs [16], including OWL 2 [4], and
for lightweight ones [2]. It is known that the addition to DL-Lite of arbitrary
nominals, i.e., concepts interpreted as a given (in general non-singleton) set of
individuals causes data complexity of query answering to become intractable
[15]. However, the impact of singleton nominals only, i.e., concepts interpreted
as a single individual, has not been investigated so far for the DLs of the DL-
Lite family. Such construct corresponds to the ObjectHasValue construct in the
context of OWL 2.
In this paper, we fill this gap, and present DL-Lite oA , which extends DL-Lite A
with singleton nominals. We concentrate on the two most significant reasoning
2 Maxim G. Haddad and Diego Calvanese
problems investigated in the context of DL-Lite, namely knowledge base sat-
isfiablity, and conjunctive query answering. We show that under this extension
both inference tasks stay first-order rewritable. Our technique is based on a prac-
tically implementable algorithm based on rewriting rules, in the style of those
implemented in current state-of-the-art OBDA systems based on DL-Lite, such
as QuOnto and Quest. This allows us to follow the tradition of the DL-Lite
family for employing relational database technology for query answering with
optimal data complexity.
After some preliminaries in Section 2, we introduce DL-Lite oA in Section 3.
We discuss, in Section 4, the problem of query answering for satisfiable knowledge
bases, and then show, in Section 5, how to rely on it to address knowledge base
satisfiability. We draw some conclusions in Section 6. Proofs of most theorems
can be found in the appendix.
2 The Description Logic DL-Lite oA
We introduce the technical preliminaries, and the lightweight DL DL-Lite A
[12,6], on which we base our results.
In DL-Lite A 1 , starting from atomic concepts and atomic roles, respectively
denoted by A and P (possibly with subscripts), we can build basic concepts B
and basic roles R according to the following syntax:
B −→ A | ∃R R −→ P | P −
A DL-Lite A TBox is a finite set of assertions of the following form:
B1 v B2 (concept inclusion assertion)
B1 v ¬B2 (concept disjointness assertion)
R1 v R2 (role inclusion assertion)
R1 v ¬R2 (role disjointness assertion)
(funct R) (functionality assertion)
In order to guarantee the good computational properties of DL-Lite A , in the
TBox we must avoid the interaction between functionality assertions and role
inclusion assertions that would be caused by allowing a functional role to be
specialized [12]. Formally, if the TBox contains (funct P ) or (funct P − ), then it
cannot contain an assertion of the form P 0 v P or P 0 v P − , for some role P 0 .
An ABox A is a finite set of membership assertions of the form A(d), ¬A(d),
P (d, d0 ), or ¬P (d, d0 ), where d, d0 denote individuals. In the following, We use
R− to denote P − if R = P , and P if R = P − . Similarly, we use R(x, y) to denote
P (x, y) if R = P , and P (y, x) if R = P − . A TBox T and an ABox A constitute
a knowledge base (KB) K = hT , Ai.
1
We do not distinguish here between data values and objects, and hence do not
introduce datatypes and attributes as done in [12], since they do not affect reasoning
as far as the results in this paper are concerned.
Extending DL-Lite A with (Singleton) Nominals 3
The formal semantics in DL-Lite A is given in the standard way, by relying
on first-order interpretations I = h∆I , ·I i. We refer to [3] for more details, and
just observe that DL-Lite A adopts the unique name assumption (una), i.e., syn-
tactically different individuals are interpreted as different domain elements. We
make use of the standard notions of satisfaction and model. In this paper, we will
focus on two reasoning problems, namely, query answering and KB satisfiability,
defined in the standard way [7]. The KB satisfiability problem is to check, given
a KB K, whether K admits at least one model. To define query answering, we
present some definitions.
A conjunctive query (CQ) q over a KB K is a first-order formula of the
form: q(x) = ∃y.conj (x, y), such that conj (x, y) is a conjunction of atoms of
the form A(t) and P (t, t0 ), where A and P are respectively an atomic concept
and an atomic role of K, and t, t0 are terms, i.e., constants in K or variables
in x and y. The free variables x of q(x) are also called distinguished variables,
and their number is called the arity of q. A boolean query is a query without
distinguished
W variables. A union of conjunctive queries (UCQ) is a disjunction
q(x) = i=1,...,n ∃yi .conj i (x, yi ) of CQs of the same arity. We sometimes use
the Datalog notation for (U)CQs:
q(x) ← ∃y1 .conj 1 (x, y1 )
···
q(x) ← ∃yn .conj n (x, yn )
Given an interpretation I, we denote by q I the set of tuples of elements of
I
∆ obtained by evaluating q in I. The certain answers of q over a KB K is the
set ans(q, K) of tuples a of constants appearing in K, such that aI ∈ q I for
every model I of K. If K is unsatisfiable, then ans(q, K) is trivially the set of all
possible tuples of constants in K whose arity is the same as that of the query.
We denote such a set by AllTup(q, K). The problem of query answering is the
computation of the set of certain answers for given (U)CQ q and KB K.
Both for KB satisfiability and for query answering, we are interested in the
data complexity, which is the complexity of the problem measured in the size of
the ABox only (i.e., assuming the TBox and the query to be fixed).
3 Adding Nominals to DL-Lite A
We present now the DL DL-Lite oA , which extends DL-Lite A with nominals.
Specifically, in DL-Lite oA , we allow for using as basic concepts also nominals,
i.e., concepts of the form {d}, which are interpreted as the singleton denoted
by the individual d. Hence, basic concepts are built according to the following
syntax:
B −→ A | ∃R | {d}
Apart from that, DL-Lite oA is defined exactly as DL-Lite A .
We observe that, due to the lack of disjunction in the DLs of the DL-Lite
family, we restrict the attention to so-called singleton nominals, which cannot
be composed using disjunction into multiple element nominals.
4 Maxim G. Haddad and Diego Calvanese
Nominals in DL-Lite oA may appear in the left-hand and in the right-hand side
of concept inclusion and disjointness assertions, and the two kinds of occurrences
play quite different roles in expressiveness and inference. Indeed, a concept in-
clusion assertion {d} v A with a nominal {d} in the left-hand side, corresponds
to an ABox assertion A(d). Similarly, a concept disjointness assertion A v ¬{d}
(or its equivalent form {d} v ¬A) corresponds to an ABox assertion ¬A(d).
Hence, we can eliminate these two kinds of assertions by moving them to the
ABox. Observe also that an assertion of the form {d} v {d0 }, where d 6= d0 , is
always satisfied due to the una, and hence can be safely eliminated from the
TBox.
Formally, we call a DL-Lite oA TBox normalized, if all its nominals appear
only in concept inclusion assertions of the form:
B v {d} (1)
A DL-Lite oA KB K = hT , Ai is normalized if T is so.
We can transform each DL-Lite oA KB K = hT , Ai into an equivalent normal-
ized KB Kn = hTn , An i as follows:
1. Initialize Tn to T and An to A.
2. For each assertion α ∈ Tn of the form {d} v ¬{d0 }, where d 6= d0 , remove α
from Tn .
3. For each assertion α ∈ Tn of the form B v ¬{d}, where B is not a nominal,
replace in Tn α with {d} v ¬B.
4. For each nominal {d} appearing in the left-hand side of a concept inclusion
or disjointness assertion {d} v C in Tn , introduce a fresh atomic concept
Ad .
5. For each concept inclusion or disjointness assertion α ∈ Tn of the form
{d} v C, replace α in Tn with Ad v C and add Ad (d) to An .
Notice that Steps 4 and 5 above deal correctly also with the case of an
(unsatisfiable) inclusion assertion of the form {d} v {d0 }, which for d 6= d0
generate the assertions Ad (d) and Ad v d0 .
It is easy to see that the above construction of Kn from K can be done in
logarithmic space in the size of K. The following result is an easy consequence
of the fact that each of the above transformations preserves the semantics of the
KB, and hence Kn is a model-conservative extension of K [10].
Lemma 1. Let K be a DL-LiteoA KB and let Kn be the normalized DL-LiteoA
KB constructed as described above. Then Kn is satisfiable iff K is satifiable, and
for each UCQ Q over K, we have that ans(Q, K) = ansQ, Kn .
By Lemma 1, we can from now on assume without loss of generality to deal
only with DL-Lite oA KBs that are normalized. For a normalized KB, all nominals
appear in the right-hand side of concept inclusion assertions that have the form
as in Equation (1). In what follows, given a normalized DL-Lite oA TBox T ,
we consider it partitioned into four parts denoted as follows: Tn contains the
concept and role disjointness assertions; Tf contains the functionality assertions;
Extending DL-Lite A with (Singleton) Nominals 5
To contains the concept inclusion assertions involving nominals; Tp contains the
remaining concept inclusions, and the role inclusions. We call Tp ∪ To the set of
positive inclusions (PIs).
The concept inclusions in To require a specific treatment in the query answer-
ing approach based on rewriting, since they restrict the concept on the left-hand
side of the concept inclusion to be interpreted as a singleton. This leads us to
introduce the notion of domain and range restricted roles, i.e., roles whose do-
main or range is restricted to a nominal. For such a role P for which To contains
∃P v {d}, for a model I of T we have that P I ⊆ {dI } × ∆I , making the inter-
pretation of the role similar to that of a concept. If a concept is restricted to a
nominal via B v {d}, then every other concept that is restricted to the nominal
indirectly, e.g., via B 0 v B, should be restricted to the same nominal. Similarly,
if a functional role is domain or range restricted, then the other component
should have maximally one element, i.e., it is restricted to an unnamed nomi-
nal. To represent this fact we make use of underscore elements with subscripts
0 , 1 , . . .. Hence, each of the occurances of these underscore elements denotes
an unnamed individual, possibly coinciding with individuals representing nomi-
nals or with other unnamed individuals (i.e, for unnamed individuals the unique
name assumption does not apply). We will use the underscore symbol without
a subscript to denote an arbitrary unnamed element.
This motivates us to define the notion of singleton closure of a TBox.
Definition 1. Let K = hT , Ai be a normalized DL-LiteoA KB. Then the single-
ton closure SC(T ) of T , is obtained by including T in SC(T ), and closing it
according to the following rules:
1. If B1 v {d} is in SC(T ) and B2 v B1 is in Tp , then B2 v {d} is in SC(T ).
2. If ∃P v {d} is in SC(T ) and (funct P ) is in T , then ∃P − v { x } is in
SC(T ), such that x is a new underscore element.
3. If ∃P − v {d} and (funct P − ) is in T , then ∃P v { x } is in SC(T ), such
that x is a new underscore element.
Lemma 2. For every ABox A. The KB K = hT , Ai is satisfiable iff hSC(T ), Ai
is satisfiable.
In the following, we make use of these notions to devise query answering and
reasoning techniques for DL-Lite oA .
4 First-order Rewritablity of Query Answering
Our aim is to extend the query rewriting algorithm of [7,6] to handle also nom-
inals. For this, we exploit the fact that DL-Lite oA , similarly to other DLs of the
DL-Lite family, enjoys a canonical model property. Specifically, we show how
to adapt the notion of restricted chase, adopted in [9] for the case of inclusion
dependencies in databases, and extended to DL-Lite in [7,8], to show the exis-
tence of a(n in general infinite) canonical model for any given DL-Lite oA KB. We
6 Maxim G. Haddad and Diego Calvanese
can construct the chase of a KB starting from the ABox, and applying positive
inclusion assertions to the set of membership assertions obtained so far.
The critical difference in DL-Lite oA with respect to the chase introduced in
[7] is that we have to take care of restricted roles (cf. Section 3), and hence
make use of the singleton closure. As above, we use the underscore symbols
to denote unnamed individuals. Throughout the construction of the canonical
interpretation, some unnamed individuals will be named, and this will change
the singleton closure. However, the cardinality of the singleton closure does not
change. For the application of the chase rules it is assumed that we have a
total (lexicographic) ordering on the assertions and on the constants (includ-
ing the ones not occurring in S our KB). The chase of K is the set of member-
ship assertions chase(K) = j∈N chase i (K), starting from chase 0 (K) = A, and
SC 0 is obtained from SC(T ) by replacing the unnamed individuals in SC(T ),
which occur in the ABox with their names. For example, if ∃R v { x } and
R(a, b) is in the ABox, then ∃R v {a} will replace ∃R v { x } in SC 0 . Then,
chase i+1 (K) is obtained from chase i (K) by adding the membership assertion
βnew , i.e., chase i+1 (K) = chase i (K) ∪ {βnew }, where βnew is the membership
assertion obtained from chase i (K) by applying one of the chase rules. Similarly,
SC i+1 = SC i [σ], the result of applying σ on SC i , where σ is the substitution
resulting from the application of one of the chase rules. The substitution σ is
the empty substitution by default, unless a concept restricted to an unnamed
individual in the singleton closure has been mapped to a named individual. In
that case, we will substitute the underscore with the named individual.
Table 1. Chase Rules for DL-Lite oA
rule α β ∈
/ chase i (K) ∈ SC i ∈/ SC i βnew σ
cr1 A1 v A2 A1 (a) A2 (a) A2 (a) []
cr2 A v ∃R A(a) R(a, x ) R− v { x } R(a, anew ) []
cr2o A v ∃R A(a) R(a, x ) R− v {d} R(a, d) []
cr2u A v ∃R A(a) R(a, x ) R− v { x } R(a, anew ) [R− v { x }/R− v {anew }]
cr3 ∃R v A ∃R(a) A(a) A(a) []
cr4 ∃R1 v ∃R2 ∃R1 (a) R2 (a, x ) R2− v { x } R2 (a, anew ) []
cr4o ∃R1 v ∃R2 ∃R1 (a) R2 (a, x ) R2− v {d} R2 (a, d) []
cr4u ∃R1 v ∃R2 ∃R1 (a) R2 (a, x ) R2− v { x } R2 (a, anew ) [R2− v { x }/R2− v {anew }]
cr5 R1 v R2 R1 (a, b) R2 (a, b) R2 (a, b) []
The chase rules are listed in Table 1. β is the first (in lexicographic order)
membership assertion in chase i (K) such that there exists a PI (i.e., an inclusion
in Tp ∪ To ) that is applicable to it, and α is the first such PI. The notion of
applicability of a PI extends in a straightforward way the one in [7] (see below).
The three subsequent columns in the table express the conditions under which
the chase rule is applied in chase i (K), in terms of the atom that should be
missing from chase i (K), and possibly the inclusion that should be present or
absent from SC i .
Extending DL-Lite A with (Singleton) Nominals 7
Algorithm PerfectRef(q, T )
Input: union of conjunctive queries Q, DL-Lite oA TBox T
Output: union of conjunctive queries Qr
Qr := Q;
ST = SC(T );
repeat (1)
Q0r := Qr ;
for each q ∈ Q0r
(O) q = reducesingleton(q, SC(T ));
(a) for each g in q
for each PI I in ST
if I is applicable to g
then Qr := Qr ∪ {remdup(q[g/gr(g, I)])};
(b) for each g1 , g2 in q
if g1 and g2 unify
then Qr := Qr ∪ {remdup(τ (reduce(q, g1 , g2 )))};
until Q0r = Qr ;
return Qr .
Fig. 1. The algorithm PerfectRef
The canonical interpretation can(K) = h∆can(K) , ·can(K) i is defined from
chase(K) as follows: ∆can(K) is the set of constants occurring in chase(K),
acan(K) = a for each constant a occurring in chase(K), Acan(K) = {a | A(a) ∈
chase(K)} for each atomic concept A, and P can(K) = {(a1 , a2 ) | P (a1 , a2 ) ∈
chase(K)} for each atomic role P . The construction of the canonical interpreta-
tion guarantees the satisfiability of the positive inclusion assertions in the TBox,
and if hSC(T ), Ai is satisfiable, then it also guarantees the satisfiability of the
nominal inclusion assertions.
Lemma 3. For every i ≥ 0, if chase i (K) satisfies SC(T ) then chase i+1 (K)
satisfies SC(T )
Lemma 4. Let K = hT , Ai be a DL-LiteoA KB. Then, can(K) is a model of K
iff K is satisfiable.
Now we can provide an adapted version of the PerfectRef algorithm presented
in [7,6], which takes into account the presence of nominals in DL-Lite oA . It takes
a DL-Lite oA TBox T and a UCQ Q and returns a UCQ Qr , which we will
show to be the FO-rewriting of Q w.r.t. T . In the following, after discussing
some preliminary notions, we explain the algorithm PerfectRef, and show its
termination and correctness.
Briefly, the algorithm PerfectRef, shown in Figure 1, iterates over the CQs
in Q and takes into consideration those assertions in T that are relevant for the
computation of the answers of Q in order to produce Qr . Note that only the
assertions in Tp and To play a role in the computation of Qr . Roughly speaking,
the algorithm checks the atoms, sees whether we can rewrite them into other
atoms in each query in Q using the PIs as rewriting rules, reduces the restricted
8 Maxim G. Haddad and Diego Calvanese
roles in the queries using the inclusions in To , and unifies any resulting unifiable
atoms.
We recall here the basic features that our variant of PerfectRef has in common
with the original version as presented in [7]2 . We say that a PI I is applicable
to an atom g if g is unifiable with the right-hand side of the assertion. The
result of the application of a PI gr(g, I)on an atom is the atom unifiable with
the left-hand side of the assertion. For example, the PI A v ∃P is applicable
to the atoms P (x, ) and P ( , ), with the atoms resulting from this application
being A(x) and A( ), respectively. We use q[g/g 0 ] to denote the CQ obtained by
replacing every occurrence of the atom g in the query q by the atom g 0 . The
function remdup removes from the body of a CQ atoms occurring more than
once. We define the most general unifier (mgu) of two unifiable atoms g1 , g2
occurring in a CQ q as in [7]. The function reduce computes the mgu of its two
arguments g1 , g2 , and applies it to the CQ q. Finally, the function τ takes as
input a CQ q and replaces every variable occurring only once with the symbol .
Our addition to PerfectRef is Step (O) which is used to handle assertions in-
volving nominals. This step involves the reduction of restricted roles to concepts.
This turns out to be necessary, since if R is a restricted role, i.e., ∃R v {d}, then
for every model I we will have that RI ⊆ {dI } × ∆I , which makes R “behave
like a concept” w.r.t. rewriting steps. Hence, we can replace an atom R(x, y)
occurring in a CQ q by ∃R− (y), and replace any further occurrence of x in q
with d. This is accomplished by the function reducesingleton, which makes use
of the singleton closure SC(T ).
Example 1. For example, if we have q(x, y) ← R1 (x, y), R2 (x, y), and we have
R2− v {d} in the TBox T , then reducesingleton will reduce q to q 0 (x, d) ←
R1 (x, d), R2 (x, ) (i.e., y is being bound to d in the answers of q). t
u
It is possible that one role is indirectly restricted to a singleton nominal, e.g.,
the assertions A v B and B v {d} induce the restriction A v {d}. PerfectRef
handles the effect of this interaction of positive inclusion assertions with nominal
inclusion assertions by making use of SC(T ), instead of T .
Taking into consideration that the presence of nominals does not lead to an
increase of the number of atoms in the rewritten queries, the termination of
PerfectRef can be proved similarly to Lemma 34 in [7].
Lemma 5. Let T be a DL-LiteoA TBox, and Q be a union of conjunctive queries
over T . Then, the algorithm PerfectRef(Q, T ) terminates.
To compute the answers of Q, given the KB K = hT , Ai, we need to evaluate
the set of conjunctive queries Qr produced by the algorithm PerfectRef on the
ABox A, which can be done in AC0 in data complexity.
Now we can start observing that query answering over satisfiable knowledge
bases can in principle be done by evaluating the query over the model can(K).
2
Extensions of PerfectRef to deal with additional constructs have also been presented
in [5,13,8].
Extending DL-Lite A with (Singleton) Nominals 9
Theorem 1. Let K be a satisfiable DL-LiteoA KB, and let Q be a union of con-
junctive queries over K. Then, ans(Q, K) = Qcan(K)
The proof is done analogously to the proof of Theorem 29 in [7], which states
an analogous result for DL-Lite R and DL-Lite F .
Taking into consideration that can(K) is infinite in general, we cannot com-
pute and evaluate queries over it. However, as for DL-Lite A , we can show that in-
stead of computing Qcan(K) we can evaluate the UCQ Qr computed by PerfectRef
directly over the ABox, considered as a database. For this purpose, we extend
the definition of database interpretation given in [7] so as to handle the presence
of nominals. The database interpretation db(T , A) = h∆db(T , A) , ·db(T , A) i of a
KB hT , Ai is the interpretation whose domain ∆db(T , A) is the non-empty set
consisting of all constants appearing in A and in nominals in T , and such that
adb(T , A) = a for each constant a, and Adb(T , A) = {a | A(a) ∈ A} for each
atomic concept A, and P db(T , A) = {(a1 , a2 ) | P (a1 , a2 ) ∈ A} for each atomic
role P .
Theorem 2. Let T be a DL-LiteoA TBox, Q a UCQ over T , and Qr =
PerfectRef(Q, T ) the UCQ returned by PerfectRef. Then, for every DL-LiteoA
db(T , A)
ABox A such that hT , Ai is satisfiable, we have that ans(Q, hT , Ai) = Qr .
Corollary 1. Query answering in DL-LiteoA is in AC0 with respect to the data
complexity
5 FO-Rewritability of KB Satisfiability
We now consider KB satisfiablity in DL-Lite oA , and provide a technique to solve
it via query evaluation, hence showing its FO-rewritablity. The first case to be
considered is a special case where the TBox has only positive inclusion assertions,
in this case the knowledge base is just a DL-Lite A knowledge base with only
positive inclusion assertions which is satisfiable according to lemma 7 in [7].
However, in the general case, we cannot construct the canonical interpreta-
tion unless the nominal inclusion assertions are satisfied. According to theorem 3
it suffices to show that the db(T , A) satisfies the nominal inclusion assertions in
the singleton closure in order to show that can(K) satisfies the singleton closure
(and hence the nominal inclusion assertions in the TBox).
The ABox A satisfies SCo (T ) when it satisfies all the assignments in SCo (T ).
An inclusion assertion A v {x} is satisfied when no individual, different than x,
is asserted as a member to the concept A in A, whereas the assertion: A v { x }
is satisfied when no two different individuals are asserted to the concept A in A.
In order to formulate the latter statement, we need to introduce the notion of a
(boolean) query associated to a nominal inclusion assertion (which was originally
applied only to negative inclusion assertions). This query evaluates false iff the
assertion is satisfied. In the following, we make use of CQs and UCQs enriched
with inequalities, and express them in the Datalog notation as in [8].
10 Maxim G. Haddad and Diego Calvanese
Definition 2. Given a DL-LiteoA nominals inclusion assertion O in SCo (T ),
the form B v {d}, such that B is a basic concept and d is an individual, the
query associated to O is a boolean conjunctive query qO of the form:
qO ← ∃x : B(x), x 6= d
Whereas, assertions of the form: B v { } are associated with the following query:
qO ← ∃x∃y : B(x), B(y)x 6= y
The following Lemma states that satisfiability for a DL-Lite oA knowledge base
K = hT , Ai, where T contains positive inclusions and nominal inclusions, can
be reduced to answering a UCQ with inequalities over A.
Lemma 6. Let K = (Tp ∪ TO , A) be a DL-LiteoA KB, and QO = O∈SC(T ) qO .
W
Then, K is satisfiable iff A 6|= QO .
Having checked the satisfiabilty of the singleton closure, we can build the
canonical interpretation satisfying a TBox containing only positive and nominal
inclusion assertions. Now we have to consider negative inclusion assertions and
functionality assertions. Functionality restrictions interact with the nominal re-
strictions, in the sense that if a role is restricted and functional then not only
the restricted component but also the other component has to be taken into the
singleton closure. We have already handled this situation in our definition of the
singleton closure. Finally, we have to check whether the functionality restric-
tions are fullfilled. This we do by defining the query associated to a functionality
restriction.
Definition 3. Given a DL-LiteoA functionality restriction F of the form
(funct R) in Tf , the query associated to F is a boolean conjunctive query qF
of the form:
qF ← R(x, y), R(x, z), y 6= z
Lemma 7. Let K = (TpW∪ TO ∪ Tf , A) be a DL-LiteoA KB, and QO =
W
O∈SC(T ) qO and QF = F ∈Tf qF . Then, K is satisfiable iff A 6|= QO and
A 6|= QF .
Notably, since answering of QF and QO over the ABox A involves only evalu-
ating QF and QO over db(T , A), the above lemma also entails that satisfiablity of
DL-Lite oA knowledge bases without NIs is FO-rewritable. Now, we can continue
the tradition of [8] in using the algorithm PerfectRef, presented in Section 4, to
check the satisfiablity of the negative inclusion assertions. Note that PerfectRef
only requires the inclusions in Tp and To .
Definition 4. Given a DL-LiteoA negative inclusion assertion N of the form
B1 v ¬B2 in Tn , the query associated to N is a boolean conjunctive query qN of
the form:
qN ← B1 (x), B2 (x)
Extending DL-Lite A with (Singleton) Nominals 11
Algorithm Consistent(K)
Input: DL-Lite oA K = hT , Ai
Output: true if it is unsatisfiable, false otherwise
• Normalize knowledge base
K = Normalize(K)
• Build singleton closure
SC(T ) = SingletonClosure(T )
• Check Singleton Closure and functionality restrictions
qO := ⊥;
foreach α ∈ SCo (T ) ∪ SC F (T )
qSC(T ) = qSC(T ) ∨ qα ;
db(T , A)
if qSC(T ) 6= ∅ return true;
qTn := ⊥;
foreach N ∈ Tn
qTn = qTn ∪ {qTn }
qTn = PerfectRef(qTn , Tp ∪ TO )
db(T , A)
return qTn
Fig. 2. The algorithm Consistent
Theorem 3. Let hT , Ai be a satisfiable DL-LiteoA KB, Tn a set of NIs, Qn =
S
N ∈Tn qN the UCQ associated to Tn . Then, K = hT ∪ Tn , Ai is satisfiable iff
hT , Ai 6|= Qn .
Now, given Lemma 6 and Theorem 3, we can establish the satisfiability of a
DL-Lite oA . This allows us to say that checking the satisfiability of DL-Lite oA KB
is first-order rewritable, and we can now write an algorithm to check the satisfi-
abilty of KBs (see Figure 2). Briefly, the algorithm first normalizes the KB, then
it checks whether the singleton closure is satisfied. Afterwards, it checks if the
funcionality restrictions are satisfied, and finally considers the satisfiablity of the
negative inclusion assertions. We will make use of the algorithms Normalize and
SingletonClosure, where SingletonClosure is an algorithm for calculating SC(T ) .
The next Theorem follows directly from the FO-rewritablity.
Theorem 4. KB satisfiablity in DL-LiteoA is in AC0 with respect to data com-
plexity.
6 Conclusion
This paper shows that the extending DL-Lite A with singleton nominals does
not have an impact on the data complexity of reasoning. The structure of the
paper follows similar ideas to those in [7,8], but is based first define a singleton
closure, and build a canonical interpretation based on this closure. Furthermore,
we define a modified version of the algorithm PerfectRef to handle the nomianl
constructions, which shows the FO-rewritability of query answering for satisfi-
able knowledge bases, and finally make use of this algorithms to check for the
12 Maxim G. Haddad and Diego Calvanese
satisfiability of DL-Lite oA knowledge bases using first-order query evaluation.
Thus, showing the FO-rewritablity of the satisfiablity problem.
Extending DL-Lite A with (Singleton) Nominals 13
References
1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family
and relations. J. of Artificial Intelligence Research 36, 1–69 (2009)
2. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proc. of the 19th
Int. Joint Conf. on Artificial Intelligence (IJCAI 2005). pp. 364–369 (2005)
3. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.):
The Description Logic Handbook: Theory, Implementation and Applications. Cam-
bridge University Press (2003)
4. Bao, J., et al.: OWL 2 Web Ontology Language document overview (second edi-
tion). W3C Recommendation, World Wide Web Consortium (Dec 2012), available
at http://www.w3.org/TR/owl2-overview/
5. Botoeva, E., Artale, A., Calvanese, D.: Query rewriting in DL-Lite HN horn . In: Proc. of
the 23rd Int. Workshop on Description Logic (DL 2010). CEUR Electronic Work-
shop Proceedings, http://ceur-ws.org/, vol. 573, pp. 267–278 (2010)
6. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Poggi, A., Rodrı́guez-
Muro, M., Rosati, R.: Ontologies and databases: The DL-Lite approach. In: Tes-
saris, S., Franconi, E. (eds.) Semantic Technologies for Informations Systems –
5th Int. Reasoning Web Summer School (RW 2009), Lecture Notes in Computer
Science, vol. 5689, pp. 255–356. Springer (2009)
7. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable
reasoning and efficient query answering in description logics: The DL-Lite family.
J. of Automated Reasoning 39(3), 385–429 (2007)
8. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Data com-
plexity of query answering in description logics. Artificial Intelligence 195, 335–360
(2013)
9. Johnson, D.S., Klug, A.C.: Testing containment of conjunctive queries under func-
tional and inclusion dependencies. J. of Computer and System Sciences 28(1),
167–189 (1984)
10. Lutz, C., Walther, D., Wolter, F.: Conservative extensions in expressive description
logics. In: Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007).
pp. 453–458 (2007)
11. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C.: OWL 2 Web
Ontology Language profiles (second edition). W3C Recommendation, World Wide
Web Consortium (Dec 2012), available at http://www.w3.org/TR/owl2-profiles/
12. Poggi, A., Lembo, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.:
Linking data to ontologies. J. on Data Semantics X, 133–173 (2008)
13. Savković, O.: Managing Datatypes in Ontology-Based Data Access. Master’s thesis,
Free University of Bozen-Bolzano, Technische Universität Wien (2011)
14. Savkovic, O., Calvanese, D.: Introducing datatypes in DL-Lite. In: Proceedings of
the Twentieth European Conference on Artificial Intelligence (ECAI 2012) (2012)
15. Seylan, I., Franconi, E., de Bruijn, J.: Effective query rewriting with ontologies
over DBoxes. In: Proc. of the 21st Int. Joint Conf. on Artificial Intelligence (IJ-
CAI 2009). pp. 923–925 (2009)
16. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals
in expressive description logics. J. of Artificial Intelligence Research 12, 199–217
(2000)
14 Maxim G. Haddad and Diego Calvanese
A Proofs for Section 3
A.1 Proof of Lemma 2
Proof. ⇐ Let hSC(T ), Ai be satisfiable and M be a model of it. Then, M is
obviously a model of K = hT , Ai, since T ⊆ SC(T ) by definition.
⇒ Let M be a model of K, by looking at definition 1, we see three parts
of SC(T ). 1. For part one, M |= K, then B2M ⊆ B1M and B1M {xM } imply that
B2M ⊆ {xM } which means that M satisfies B2 v {x}.
2. For part two, if M |= ∃P v {d} then {x ∈ ∆M : ∃y : (x, y) ∈ P M } ⊆ {d},
i.e., ∀(x, y) ∈ P M : x = d and if M |= (funct P ) then ∀x, y, z ∈ ∆M : (x, y) ∈
P M , (x, z) ∈ P M → y = z but ∀(x, y) ∈ P M : x = dM then ∀(x, y) ∈ P M : ∃w :
x = d ∧ y = w , then ∃P − v { x } . 3. For part three, the proof is parallel to part
three.
B Proofs for Section 4
B.1 Proof of Lemma 3
Proof. Let us assume the opposite: chase i (K) satisfies SC(T ) and chase i+1 (K) =
chase i (K) ∪ {βnew } does not satisfy SC(T ). Then there is an assertion B v {d}
in SC(T ) which has been broken by βnew . However this is not possible because
if B v {d} in SC(T ) then B v {d} in SC(T )i which will enforce the execution
of one of the roles: cr2o, cr2u, cr4o, or cr4u which guarantee the satisfiability
of SC(T ), which is a contradiction.
B.2 Proof of Lemma 4
Proof. We first prove that given a satisfiable DL-Lite oA KB K = hT , Ai, and let
M = (∆M , .M ) be a model of K. Then, a model homomorphism ψ from ∆can(K)
to ∆M such that:
1. For each atomic concept A in K and each object o ∈ ∆can(K) , if o ∈ Acan(K) ,
then ψ(o) ∈ AM and
2. For each atomic role P in K and each pair of objects o, o0 ∈ ∆can(K) , if
(o, o0 ) ∈ P can(K) , then (ψ(o), ψ(o0 )) ∈ P M
Again, the proof can be done the same way it is done in [6], among
other papers, by induction on the construction of chase(K). Now, we get at
the statement that whenever K is satisfiable, can(K) is a model of K and
vice-versa. The proof follows our definition of the chase with some changes in
the inductive step, where we have to take into consideration the singleton closure.
We define the function ψ from ∆can(K) to ∆M by a chase based induc-
tion, and show that the properties above hold.
Base Step: For each constant d occurring in A, we define ψ(dcan(K) ) = dM ,
note that chase 0 (K) = A and that ψ(dcan(K) ) = d. It is the case that for every
Extending DL-Lite A with (Singleton) Nominals 15
concept A: o ∈ Acan 0 (K) if A(o) ∈ A and respectively for every role P : (o1 , o2 ) ∈
P can 0 (K) if P (o1 , o2 ) ∈ A. Taking into consideration that M is a model, we can
say that: ψ(o) ∈ AM and (ψ(o1 ), ψ(o2 )) ∈ P M .
Inductive Step: chase i+1 (K) is obtained from chase i (K) by applying a certain
chase rule. We will prove the case for the rules cr2, cr2o, and cr2u, where the
other rules can be done analogously. Let us consider the rules cr2, cr2o, cr2u
this means that the PI of the form A v ∃R, where A is an atomic concept T ,
and R is a basic role in T , is applied in chase i (K) to a certain assertion of the
form A(o), and there is not an assertion of the form P (o, ) in chase i (K), then:
– if there is no singleton restriction on the role P , i.e., chase i+1 (K) =
chase i (K) ∪ {P (o, e)} such that e is the first lexicographically not used con-
stant. By the induction hypothesis above, there exists om ∈ ∆M such that
ψ(o) = om and because M is a model of K then there should be a o0 such
that (om , o0 ) ∈ P M , hence we set ψ(e) = o0
– If there is a singleton restriction on the role P of the form ∃P − ∈ {d}, then
chase i+1 (K) = chase i (K) ∪ {P (o, d)}. By the induction hypothesis above,
there exists om ∈ ∆M such that ψ(o) = om and because M is a model of K
then (om , ψ(d)) ∈ P M should be satisfied by M.
– If there is a singleton restriction on the role P of the form ∃P − ∈ { }, then
chase i+1 (K) = chase i (K)∪{P (o, e)}, such that e is the first lexicographically
not used constant. By the induction hypothesis above, there exists om ∈ ∆M
such that ψ(o) = om and because M is a model of K then there should be
a well defined constant o0 such that (om , o0 ) ∈ P M , hence we set ψ(e) = o0 .
Now we can prove the main theorem.
⇒ If can(K) is a model of K, then K is satisfiable by definition.
⇐ If K is satisfiable then there is an interpretation M = (∆M , .M ) which
is a model of K per definition. can(K) satisfies A because A = chase 0 (K) ⊆
chase(K). can(K) also satisfies Tp . What is left is to prove that can(K) satisfies
To and Tn .
Let assume that M satisfies K, but for some nominal inclusion assertions
A v {d} can(K) does not satisfy K, then we have AM ⊆ {dM } but Acan(K) 6⊆
{dcan(K) }, then there exists ocan(K) ∈ ∆can(K) such that ocan(K) ∈ Acan(K) and
ocan(K) ∈/ {dcan(K) }. Hence, given the homomorphism ψ : ∆can(K) → ∆M , then
ψ(o can(K)
) ∈ ∆M such that ψ(ocan(K) ) ∈ AM and ψ(ocan(K) ) ∈ / {ψ(dcan(K) )},
which contradicts the fact that M is a model. The proof for negative inclusion
assertions can be done in an analogous way.
B.3 Proof of Theorem 1
Proof. Note that for each constant d occurring in K, we have dcan(K) = d. Hence,
for every tuple t composed of constants in K, we have t = tcan(K) . We can hence
rephrase the claim as t ∈ ans(Q, K) iff t ∈ Qcan(K) .
“⇒” if t ∈ ans(Q, K) then ∀M such that M is a model of K: t ∈ QM .
Taking into consideration that can(K) is a model of K, then t ∈ Qcan(K) .
16 Maxim G. Haddad and Diego Calvanese
“⇐” if t ∈ Qcan(K) then there is an assignment µ : V → ∆can(K) which maps
every distinguished variable in the query to an object in the domain of can(K),
such that all atoms in the query are evaluated as true. Given the fact that there
is a truth-preserving homomorphism ψ : ∆can(K) → ∆M for every model of
K, then the composition function ψ ◦ µ : V → ∆M maps every distinguished
variable in the query to an object in ∆M , taking into consideration that ψ is
truth-preserving, t ∈ QM for every model M. By definition, it follows that
t ∈ ans(Q, K).
B.4 Proof of Theorem 2
Proof. In order to start with the proof, we have to introduce the preliminary
notion of witness of a tuple of constants with respect to a certain CQ q.
Definition 5. Given:
– a DL-LiteoA knowledge base K = hT , Ai
– a CQ q(x) ← conj(x, y) over K
– a tuple t of constants occurring in K
then a set of membership assertions G is a witness of t w.r.t. q if there exists a
substitution σ from the variables y in conj(t, y) to constants in G such that the
set of atoms in σ(conj(t, y)) is equal to G.
It is intuitive that each such witness corresponds to a subset of chase(K),
which is sufficiently enough to make ∃y.conj(x, y) valuate true in the canonical
interpretation can(K), making t = tcan(K) a member of q can(K) . In other words,
t ∈ q can(K) iff there exists a witness G of t w.r.t. q such that G ⊆ chase(K).
The cardinality of a witness G, denoted by |G|, is the number of membership
assertions in G.
However, the finite witness corresponds to a subset of the possibly infinite
chase(K). Nevertheless, G is finite, which means that there are a certain j such
that G ⊆ chase j (K). This motivates us to define the notion of pre-witness, which
projects on defining the atoms in chase i (K), such that i < j which resulted in
G (or Gj ), by repeated applications of chase rules. In order to do so, we have to
introduce the notions of ancestor (and its dual successor ).
In the following, we say that a membership assertion β is an ancestor of
a membership assertion β 0 in a set of membership assertions S, if there exist
β1 , . . . , βn in S, such that β1 = β, βn = β 0 , and each βi can be generated by
applying a chase rule to βi−1 , for i ∈ {2, . . . , n}. We also say that β 0 is a successor
of β.
Given a witness of Gk of a tuple t w.r.t. a CQ q, such that k is the highest
k such that Gk ⊆ chase k (K). For each i ∈ {0, . . . , k}, we denote with Gi the
pre-witness of t w.r.t. q in chase i (K), defined as follows:
[
Gi = { β ∈ chase i (K) | β is an ancestor of β 0 in chase k (K) and
0
β ∈Gk there exists no successor of β in chase i (K)
which is an ancestor of β 0 in chase k (K) }.
Extending DL-Lite A with (Singleton) Nominals 17
Now we can get to formalize and prove the theorem.
Since hT , Ai W
is satisfiable, and the finite size of Sthe reformulation of the
query, i.e., Qr = q̂∈Qr q̂, we need only to prove that q̂∈Qr q̂ db(T , A) = q can(K) .
“⇐” We have to show that q̂ db(T , A) ⊆ q can(K) for each q̂ ∈ Qr . Hence,
let us consider two CQs qi and qi+1 , such that qi+1 is obtained from qi by
can(K) can(K)
applying some step of the algorithm PerfectRef, and show that qi+1 ⊆ qi .
can(K)
Let t ∈ qi+1 , then there exists a witness G ⊆ can(K) of t w.r.t. qi+1 . Then
there are two possibilities:
– step (a) of PerfectRef is applied then qi+1 is resulting from applying some
PI I, say I = A1 v A, then:
qi+1 = qi [A(x)/A1 (x)]
(note that the same methodology can be generalized to all of the other types
of assertions). Then, there exists a membership assertion in G for which I is
applicable, implying that there exists a witness for t w.r.t. qi in chase(K).
can(K)
Therefore, tcan(K) ∈ qi .
– step (b) of PerfectRef is applied, then:
qi+1 = τ (reduce(reducesingleton(qi ), g1 , g2 ))
where g1 and g2 are two atoms belonging to qi such that g1 and g2 unify. It
is easy to see that G stays a witness of t w.r.t. qi , and therefore tcan(K) ∈
can(K)
qi .
Since each query q̂ of Qr is either q or a query resulting from q by applying
PerfectRef n-times, where n ≥ 1, we can see that for each q̂ ∈ Qr it is the
case that q̂ can(K) ⊆ q can(K) by repeating the application of the property above.
Hence, it follows that q̂ db(T , A) ⊆ q̂ can(K) ⊆ q can(K) , i.e., q̂ db(T , A) ⊆ q can(K) .
db(T , A)
“⇒” We have to show that q can(K) ⊆ Qr , i.e., we have to show that
for each tuple t ∈ q can(K)
, there exists q̂ ∈ Qr such that t ∈ q̂ db(T , A) . First,
since t ∈ q can(K) , it follows that there exists a CQ q in Q and a finite number k
such that there is a witness Gk of t w.r.t. q contained in chase k (K). Moreover,
without loss of generality, we can assume that every rule cr1, cr2, cr2o, cr2u,
cr3, cr4, cr4o, cr4u, and cr5 used in the construction of chase(K) is necessary
in order to generate such a witness Gk . Now we prove by induction on i that,
starting from Gk , we can “go back” through the rule applications and find a
query q̂ in Qr such that the pre-witness Gk−i of t w.r.t. q in chase k−i (K) is also
a witness of t w.r.t. q̂.
To this aim, we prove that there exists q̂ ∈ Qr such that:
– Gk−i (the per-witness of t w.r.t. q) is a witness of t w.r.t. q̂ and
– |q̂| = |Gk−i |, where |q̂| indicates the number of atoms in the CQ q̂.
18 Maxim G. Haddad and Diego Calvanese
Then we can apply this claim for i = k, taking into consideration that
chase 0 (K) = A.
Base step: (i=0) There exists q̂ ∈ Qr such that Gk is a witness of t
w.r.t. q̂ and |q̂| = |Gk |. This is an immediate consequence of the fact that
q ∈ Qr and that Qr is closed with respect to step (b) of the algorithm PerfectRef.
Indeed, if |Gk | < |q| then there exist two atoms g1 , g2 in q and a mem-
bership assertion β in Gk such that β and g1 unify and β and g2 unify, which
implies that g1 and g2 unify.
Therefore, by step (b) of the algorithm, it follows that there exists a query
q1 ∈ Qr (with q1 = reduce(q, g1 , g2 )) such that Gk is a witness of t w.r.t. q1
and |q1 | = |q| − 1. This step is exactly proved as in DL-Lite A , taking into
consideration that our added function reducesingleton does not influence the
statement. . Now, if |Gk | < |q1 |, we can iterate the above argument, thus we con-
clude that there exists q̂ ∈ Qr such that Gk is a witness of t w.r.t. q̂ and |q̂| = |Gk |.
Inductive step: suppose that there exists q̂ ∈ Qr such that Gk−i+1 is a
witness of t w.r.t. q̂ and |q̂| = |Gk−i+1 |.
Let us assume that chase k−i+1 (K) is obtained by applying cr2, cr2o, or
cr2u to chase k−i (K) (the proof is analogous for rules cr1, cr3, cr4, cr4o,
cr4u, and cr5). This means that a PI of the form A v ∃P 3 , where A is
an atomic concept and P is an atomic role, is applied in chase k−i (K) to a
membership assertion of the form A(a), such that there are no named individual
a0 in t such that P (a, a0 ) ∈ chase k−i (K). Therefore, if P is not a restricted
role, then we apply rule cr2, i.e., chase k−i+1 (K) = chase k−i (K) ∪ {P (a, a00 )},
where a00 is a new symbol. Since a00 is not a named individual symbol, i.e., a
constant not occurring elsewhere in Gk−i+1 , and since |q̂| = |Gk−i+1 |, it follows
that the atom P (x, ) occurs in q̂. Therefore, by step (a) of the algorithm, it
follows that there exists a query q1 ∈ Qr (with q1 = q̂[P (x, )/A(x)]) such that
Gk−i is a witness of t w.r.t. q1 . If P is a restricted role, say ∃P v {d}, then we
apply cr2o, but in this case the function reducesingleton will reduce the atom
P (a, x), if x is a variable to the form ∃P (a) and replacing all the occurences
of the variable x to d, thus maintaining the answers connecting with d. The
discussion is similar for the chase rule cr2u.
Now, there are two possible cases: either |q1 | = |Gk−i |, and in this case the
claim is immediate; or |q1 | = |Gk−i | + 1. This last case arises if and only if the
membership assertion A(a) to which the rule cr2 is applied is both in Gk−i and
inGk−i+1 . This implies that there exist two atoms g1 and g2 in q1 such that
A(a) and g1 unify and A(a) and g2 unify, hence g1 and g2 unify. Therefore, by
step (b) of the algorithm (applied to q1 ), it follows that there exists q2 ∈ Qr
(with q2 = reduce(q1 , g1 , g2 )) such that Gk−i is a witness of t w.r.t. q2 and
3
The other execution of rule cr2 is for the case where the PI is A v ∃P − , which is
analogous.
Extending DL-Lite A with (Singleton) Nominals 19
|q2 | = |Gk−i+1 |, which proves the claim. Note that the restricted roles are treated
exactly like ∃P , because the reducesingleton function will reduce them to such.
t
u
C Proofs for Section 5
C.1 Proof of Lemma 7
Let K = (Tp ∪ To ∪ Tf , A) be a DL-Lite oA KB, and QO = O∈SC(T ) qO and
W
W
QF = F ∈Tf qF . Then, K is satisfiable iff A 6|= QO and A 6|= QF .
Proof. ”⇒” if K is satisfiable, then per definition it suffices all the assertions
in Tp ∪ To ∪ Tf . Hence, taking into consideration that the queries qF ,QO are
defined to be true only when an an assertion is not satsified, we can say that
A 6|= QO and A 6|= QF .
”⇐” if A 6|= QO and A 6|= QF then the satisfaction of the nominal inclusion
assertions, it follows from A 6|= QO that A = chase 0 (K) satisfies SC(T )o , which
makes them satisfiable by a direct application of Lemma 2.
For the functionality assertions, let us assume that a certain assertion in Tf ,
say (funct R) is not satisfied. This means that there exist x, y, z ∈ ∆can(K)
such (x, y) and (x, z) are in Rcan(K) , and y 6= z. Well, this can not occur
in chase 0 (K) = A because of the non-satisfaction of the queries. Then there
would exist an i such that chase i (K) satisfies the functionality assertion, whereas
chase i+1 (K) does not. The only chase rules which can break the functionality
assertions are cr2,cr2o,cr2u and cr4,cr4o,cr4u. Without restriction of gener-
ality we will only prove the case for the first three (the proof for the next three
is parallel)
– If it is cr2 is applied, then only new individuals are introduced, which makes
the violation of the functionality not possible.
– For if cr2o is applied, then the only case where the functionality assertion
can be broken, if the non-restricted component contains more than one ele-
ment, but this is guaranteed by the definition of the singleton closure. which
is satisfied as above for the nominal inclusion assertions
– For if cr2u is parallel to cr2o
C.2 Proof of Theorem 3
Proof. “⇐” We show that if hT ∪ Tn , Ai is unsatisfiable then hT , Ai |= Qn .
Consider the FOL formula φ being the conjenction of all assertions in K, in
terms of first-order logic, i.e.
^ ^ ^
φ= α∧ ∧ γ.
α∈T β∈Tn γ∈A
20 Maxim G. Haddad and Diego Calvanese
Intuitively, if K is unsatisfiable then φ is unsatisfiable, hence, we can deduce
that: ^ ^ _
∧ γ |= ¬β
α∈T γ∈A β∈Tn
from which we can observe that there should be a NI N ∈ Tn such that hT , Ai |=
N , and therefore hT , Ai 6|= Qn .
“⇒” We prove that if hT , Ai |= Qn then K = hT ∪ Tn , Ai is unsatisfiable. If
hT , Ai |= Qn , them there is some NI N , such that If hT , Ai |= qN , which implies
that every model satisfying hT , Ai satisfies also qN . Taking into consideration
the assumed satisfiablity of the first, we can deduce the satisfiability of the latter.
Meaning that there are some objects in the domain which contradict the NI N ,
i.e., hT , Ai 6|= N , or hT , Ai |= ¬N . By deduction, we have that hT ∪ {N }, Ai is
unsatisfiable, making any KB containing it, including hT ∪ Tn , Ai not satisfiable.