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. Di erently from arbitrary (nonsingleton) nominals, which make query answering intractable in data complexity, we show that both knowledge base satis ability and conjunctive query answering stay rst-order rewritable when DL-LiteA is extended with singleton nominals. Our technique is based on a practically 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.
The DL-Lite family [
The DL-Lite family has been investigated thoroughly in recent years, and
several extensions with respect to the original set of constructs studied in [
Nominals, i.e., concepts interpreted as a singleton, are a signi cant construct
in DLs, investigated both for expressive DLs [
In this paper, we ll this gap, and present DL-LiteoA, which extends DL-LiteA with singleton nominals. We concentrate on the two most signi cant reasoning problems investigated in the context of DL-Lite, namely knowledge base satis ablity, and conjunctive query answering. We show that under this extension both inference tasks stay rst-order rewritable. Our technique is based on a practically 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-LiteoA in Section 3. We discuss, in Section 4, the problem of query answering for satis able knowledge bases, and then show, in Section 5, how to rely on it to address knowledge base satis ability. We draw some conclusions in Section 6. Proofs of most theorems can be found in the appendix. 2
The Description Logic DL-Lite o
A
We introduce the technical preliminaries, and the lightweight DL DL-LiteA
[
In DL-LiteA1, 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 j 9R
R !
P j P
A DL-LiteA TBox is a nite set of assertions of the following form:
B1 v B2
B1 v :B2
R1 v R2
R1 v :R2
(funct R)
(concept inclusion assertion)
(concept disjointness assertion )
(role inclusion assertion )
(role disjointness assertion )
(functionality assertion)
In order to guarantee the good computational properties of DL-LiteA, 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 [
An ABox A is a nite 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 [
The formal semantics in DL-LiteA is given in the standard way, by relying
on rst-order interpretations I = h I ; I i. We refer to [
A conjunctive query (CQ) q over a KB K is a rst-order formula of the form: q(x) = 9y: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 variables. A union of conjunctive queries (UCQ) is a disjunction q(x) = Wi=1;:::;n 9yi:conj i(x; yi) of CQs of the same arity. We sometimes use the Datalog notation for (U)CQs:
Given an interpretation I, we denote by qI 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 2 qI for every model I of K. If K is unsatis able, 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 satis ability 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 xed). 3
Adding Nominals to DL-Lite A We present now the DL DL-LiteoA, which extends DL-LiteA with nominals. Speci cally, in DL-LiteoA, we allow for using as basic concepts also nominals, i.e., concepts of the form f g
d , which are interpreted as the singleton denoted by the individual d. Hence, basic concepts are built according to the following syntax:
B
A j 9R j fdg ! Apart from that, DL-LiteoA is de ned exactly as DL-LiteA.
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.
Nominals in DL-LiteoA 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 di erent roles in expressiveness and inference. Indeed, a concept inclusion assertion fdg v A with a nominal fdg in the left-hand side, corresponds to an ABox assertion A(d). Similarly, a concept disjointness assertion A v :fdg (or its equivalent form fdg 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 fdg v fd0g, where d 6= d0, is always satis ed due to the una, and hence can be safely eliminated from the TBox.
Formally, we call a DL-LiteoA TBox normalized, if all its nominals appear only in concept inclusion assertions of the form:
B v fdg (1) A DL-LiteoA KB K = hT ; Ai is normalized if T is so.
We can transform each DL-LiteoA KB K = hT ; Ai into an equivalent normalized KB Kn = hTn; Ani as follows: 1. Initialize Tn to T and An to A. 2. For each assertion 2 Tn of the form fdg v :fd0g, where d 6= d0, remove from Tn. 3. For each assertion 2 Tn of the form B v :fdg, where B is not a nominal, replace in Tn with fdg v :B. 4. For each nominal fdg appearing in the left-hand side of a concept inclusion or disjointness assertion fdg v C in Tn, introduce a fresh atomic concept Ad. 5. For each concept inclusion or disjointness assertion 2 Tn of the form fdg 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 (unsatis able) inclusion assertion of the form fdg v fd0g, 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 [
Lemma 1. Let K be a DL-Liteo KB and let Kn be the normalized DL-Liteo
A A KB constructed as described above. Then Kn is satis able i K is sati able, 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-LiteoA 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-LiteoA 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; 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 speci c treatment in the query answering 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 domain or range is restricted to a nominal. For such a role P for which To contains 9P v fdg, for a model I of T we have that P I fdI g I , making the interpretation of the role similar to that of a concept. If a concept is restricted to a nominal via B v fdg, then every other concept that is restricted to the nominal indirectly, e.g., via B0 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 nominal. 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 nominals 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 de ne the notion of singleton closure of a TBox. De nition 1. Let K = hT ; Ai be a normalized DL-Liteo KB. Then the singleA 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 fdg is in SC(T ) and B2 v B1 is in Tp, then B2 v fdg is in SC(T ). 2. If 9P v fdg is in SC(T ) and (funct P ) is in T , then 9P v f xg is in
SC(T ), such that x is a new underscore element. 3. If 9P v fdg and (funct P ) is in T , then 9P v f xg is in SC(T ), such that x is a new underscore element.
Lemma 2. For every ABox A. The KB K = hT ; Ai is satis able i hSC(T ); Ai is satis able.
In the following, we make use of these notions to devise query answering and reasoning techniques for DL-LiteoA. 4
Our aim is to extend the query rewriting algorithm of [
The critical di erence in DL-LiteoA with respect to the chase introduced in
[
The chase rules are listed in Table 1. is the rst (in lexicographic order)
membership assertion in chasei(K) such that there exists a PI (i.e., an inclusion
in Tp [ To) that is applicable to it, and is the rst such PI. The notion of
applicability of a PI extends in a straightforward way the one in [
Input: union of conjunctive queries Q, DL-LiteoA TBox T Output: union of conjunctive queries Qr Qr := Q; ST = SC(T ); repeat (1)
Q0r := Qr; for each q 2 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 [ fremdup(q[g=gr(g; I)])g; (b) for each g1, g2 in q if g1 and g2 unify then Qr := Qr [ fremdup( (reduce(q; g1; g2)))g; until Q0r = Qr; return Qr.
The canonical interpretation can(K) = h can(K); can(K)i is de ned 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) = fa j A(a) 2 chase(K)g for each atomic concept A, and P can(K) = f(a1; a2) j P (a1; a2) 2 chase(K)g for each atomic role P . The construction of the canonical interpretation guarantees the satis ability of the positive inclusion assertions in the TBox, and if hSC(T ); Ai is satis able, then it also guarantees the satis ability of the nominal inclusion assertions.
Lemma 3. For every i satis es SC(T )
0, if chasei(K) satis es SC(T ) then chasei+1(K) Lemma 4. Let K = hT ; Ai be a DL-Liteo KB. Then, can(K) is a model of K A i K is satis able.
Now we can provide an adapted version of the PerfectRef algorithm presented
in [
Brie y, 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 roles in the queries using the inclusions in To, and uni es any resulting uni able atoms.
We recall here the basic features that our variant of PerfectRef has in common
with the original version as presented in [
Our addition to PerfectRef is Step (O) which is used to handle assertions involving 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., 9R v fdg, then for every model I we will have that RI fdI g 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 9R (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 fdg in the TBox T , then reducesingleton will reduce q to q0(x; d) R1(x; d); R2(x; ) (i.e., y is being bound to d in the answers of q). tu
It is possible that one role is indirectly restricted to a singleton nominal, e.g., the assertions A v B and B v fdg induce the restriction A v fdg. PerfectRef handles the e ect 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 [
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 satis able 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 [
Taking into consideration that can(K) is in nite in general, we cannot
compute and evaluate queries over it. However, as for DL-LiteA, we can show that
instead 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 de nition of database interpretation given in [
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-Liteo A ABox A such that hT ; Ai is satis able, we have that ans (Q; hT ; Ai) = Qrdb(T ; A). Corollary 1. Query answering in DL-Liteo is in AC0 with respect to the data A complexity 5
We now consider KB satis ablity in DL-LiteoA, and provide a technique to solve
it via query evaluation, hence showing its FO-rewritablity. The rst 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-LiteA knowledge base with only
positive inclusion assertions which is satis able according to lemma 7 in [
However, in the general case, we cannot construct the canonical interpretation unless the nominal inclusion assertions are satis ed. According to theorem 3 it su ces to show that the db(T ; A) satis es the nominal inclusion assertions in the singleton closure in order to show that can(K) satis es the singleton closure (and hence the nominal inclusion assertions in the TBox).
The ABox A satis es SCo(T ) when it satis es all the assignments in SCo(T ).
An inclusion assertion A v fxg is satis ed when no individual, di erent than x,
is asserted as a member to the concept A in A, whereas the assertion: A v f xg
is satis ed when no two di erent 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 i the
assertion is satis ed. In the following, we make use of CQs and UCQs enriched
with inequalities, and express them in the Datalog notation as in [
A the form B v f g
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
9x : B(x); x 6= d Whereas, assertions of the form: B v f g are associated with the following query: qO
9x9y : B(x); B(y)x 6= y
The following Lemma states that satis ability for a DL-LiteoA 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 = WO2SC(T ) qO. Then, K is satis able i A 6j= QO.
Having checked the satis abilty 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 restrictions, 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 de nition of the singleton closure. Finally, we have to check whether the functionality restrictions are full lled. This we do by de ning the query associated to a functionality restriction.
De nition 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 WO2SC(T ) qO and QF A 6j= QF .
= =(TpW[ TOq[. TTf ;hAen), bKe ias sDaLti-sLiatbeloAe i
F2Tf F
KB, and QO =
A 6j= QO and
Notably, since answering of QF and QO over the ABox A involves only evaluating QF and QO over db(T ; A), the above lemma also entails that satis ablity of DL-Liteo knowledge bases without NIs is FO-rewritable. Now, we can continue
A
the tradition of [
De nition 4. Given a DL-Liteo negative inclusion assertion N of the form
A B1 v :B2 in Tn, the query associated to N is a boolean conjunctive query qN of the form: qN
Input: DL-LiteoA K = hT ; Ai Output: true if it is unsatis able, false otherwise
Normalize knowledge base K = Normalize(K) Build singleton closure SC(T ) = SingletonClosure(T )
Check Singleton Closure and functionality restrictions qO := ?; foreach
2 SCo(T ) [ SCF (T ) qSC(T ) = qSC(T ) _ q ; if qdb(T ; A) 6= ; return true;
SC(T ) qTn := ?; foreach N 2 Tn
qTn = qTn [ fqTn g qTn = PerfectRef(qTn ; Tp [ TO) return qdb(T ; A)
Tn Theorem 3. Let hT ; Ai be a satis able DL-Liteo KB, Tn a set of NIs, Qn = SN2Tn qN the UCQ associated to Tn. Then, K =A hT [ Tn; Ai is satis able i hT ; Ai 6j= Qn.
Now, given Lemma 6 and Theorem 3, we can establish the satis ability of a DL-LiteoA. This allows us to say that checking the satis ability of DL-LiteoA KB is rst-order rewritable, and we can now write an algorithm to check the satis abilty of KBs (see Figure 2). Brie y, the algorithm rst normalizes the KB, then it checks whether the singleton closure is satis ed. Afterwards, it checks if the funcionality restrictions are satis ed, and nally considers the satis ablity 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 satis ablity in DL-Liteo is in AC0 with respect to data comA plexity. 6
This paper shows that the extending DL-LiteA 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 [
A.1
Proof. ( Let hSC(T ); Ai be satis able and M be a model of it. Then, M is obviously a model of K = hT ; Ai, since T SC(T ) by de nition.
) Let M be a model of K, by looking at de nition 1, we see three parts of SC(T ). 1. For part one, M j= K, then B2M B1M and B1M fxM g imply that B2M fxM g which means that M satis es B2 v fxg. 2. For part two, if M j= 9P v fdg then fx 2 M : 9y : (x; y) 2 P M g fdg, i.e., 8(x; y) 2 P M : x = d and if M j= (funct P ) then 8x; y; z 2 M : (x; y) 2 P M ; (x; z) 2 P M ! y = z but 8(x; y) 2 P M : x = dM then 8(x; y) 2 P M : 9w : x = d ^ y = w , then 9P v f xg . 3. For part three, the proof is parallel to part three.
B B.1
Proof. Let us assume the opposite: chasei(K) satis es SC(T ) and chasei+1(K) = chasei(K) [ f newg does not satisfy SC(T ). Then there is an assertion B v fdg in SC(T ) which has been broken by new. However this is not possible because if B v fdg in SC(T ) then B v fdg in SC(T )i which will enforce the execution of one of the roles: cr2o, cr2u, cr4o, or cr4u which guarantee the satis ability of SC(T ), which is a contradiction.
B.2
Proof. We rst prove that given a satis able DL-LiteoA 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 2
then (o) 2 AM and 2. For each atomic role P in K and each pair of objects o; o0 2 (o; o0) 2 P can(K), then ( (o); (o0)) 2 P M can(K), if o 2 Acan(K), can(K), if
Again, the proof can be done the same way it is done in [
Base Step: For each constant d occurring in A, we de ne (dcan(K)) = dM, note that chase0(K) = A and that (dcan(K)) = d. It is the case that for every concept A: o 2 Acan0(K) if A(o) 2 A and respectively for every role P : (o1; o2) 2 P can0(K) if P (o1; o2) 2 A. Taking into consideration that M is a model, we can say that: (o) 2 AM and ( (o1); (o2)) 2 P M.
Inductive Step: chasei+1(K) is obtained from chasei(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 9R, where A is an atomic concept T , and R is a basic role in T , is applied in chasei(K) to a certain assertion of the form A(o), and there is not an assertion of the form P (o; ) in chasei(K), then: { if there is no singleton restriction on the role P , i.e., chasei+1(K) = chasei(K) [ fP (o; e)g such that e is the rst lexicographically not used constant. By the induction hypothesis above, there exists om 2 M such that (o) = om and because M is a model of K then there should be a o0 such that (om; o0) 2 P M, hence we set (e) = o0 { If there is a singleton restriction on the role P of the form 9P 2 fdg, then chasei+1(K) = chasei(K) [ fP (o; d)g. By the induction hypothesis above, there exists om 2 M such that (o) = om and because M is a model of K then (om; (d)) 2 P M should be satis ed by M. { If there is a singleton restriction on the role P of the form 9P 2 f g, then chasei+1(K) = chasei(K)[fP (o; e)g, such that e is the rst lexicographically not used constant. By the induction hypothesis above, there exists om 2 M such that (o) = om and because M is a model of K then there should be a well de ned constant o0 such that (om; o0) 2 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 satis able by de nition. ( If K is satis able then there is an interpretation M = ( M; :M) which is a model of K per de nition. can(K) satis es A because A = chase0(K) chase(K). can(K) also satis es Tp. What is left is to prove that can(K) satis es To and Tn.
Let assume that M satis es K, but for some nominal inclusion assertions A v fdg can(K) does not satisfy K, then we have AM fdMg but Acan(K) 6 fdcan(K)g, then there exists ocan(K) 2 can(K) such that ocan(K) 2 Acan(K) and ocan(K) 2= fdcan(K)g. Hence, given the homomorphism : can(K) ! M, then (ocan(K)) 2 M such that (ocan(K)) 2 AM and (ocan(K)) 2= f (dcan(K))g, 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. 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 2 ans(Q; K) i t 2 Qcan(K).
\)" if t 2 ans(Q; K) then 8M such that M is a model of K: t 2 QM. Taking into consideration that can(K) is a model of K, then t 2 Qcan(K). \(" if t 2 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 2 QM for every model M. By de nition, it follows that t 2 ans(Q; K).
B.4
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. De nition 5. Given: { a DL-Liteo knowledge base K = hT ; Ai { a CQ q(x)A 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 su ciently enough to make 9y:conj(x; y) valuate true in the canonical interpretation can(K), making t = tcan(K) a member of qcan(K). In other words, t 2 qcan(K) i there exists a witness G of t w.r.t. q such that G chase(K). The cardinality of a witness G, denoted by jGj, is the number of membership assertions in G.
However, the nite witness corresponds to a subset of the possibly in nite chase(K). Nevertheless, G is nite, which means that there are a certain j such that G chasej (K). This motivates us to de ne the notion of pre-witness, which projects on de ning the atoms in chasei(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 f2; : : : ; ng. 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 chasek(K). For each i 2 f0; : : : ; kg, we denote with Gi the pre-witness of t w.r.t. q in chasei(K), de ned as follows:
Gi = [ 02Gk f 2 chasei(K) j
is an ancestor of 0 in chasek(K) and there exists no successor of in chasei(K) which is an ancestor of 0 in chasek(K) g: Now we can get to formalize and prove the theorem.
Since hT ; Ai is satis able, and the nite size of the reformulation of the query, i.e., Qr = Wq^2Qr q^, we need only to prove that Sq^2Qr q^db(T ; A) = qcan(K). Let t 2 qic+an1(K), then there exists a witness G there are two possibilities: \(" We have to show that q^db(T ; A) qcan(K) for each q^ 2 Qr. Hence, let us consider two CQs qi and qi+1, such that qi+1 is obtained from qi by applying some step of the algorithm PerfectRef, and show that qic+an1(K) qican(K). can(K) of t w.r.t. qi+1. Then { 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).
Therefore, tcan(K) 2 qican(K). { 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) 2 qcan(K).
i
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^ 2 Qr it is the case that q^can(K) qcan(K) by repeating the application of the property above. Hence, it follows that q^db(T ; A) q^can(K) qcan(K), i.e., q^db(T ; A) qcan(K).
\)" We have to show that qcan(K) Qrdb(T ; A), i.e., we have to show that for each tuple t 2 qcan(K), there exists q^ 2 Qr such that t 2 q^db(T ; A). First, since t 2 qcan(K), it follows that there exists a CQ q in Q and a nite number k such that there is a witness Gk of t w.r.t. q contained in chasek(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 nd a query q^ in Qr such that the pre-witness Gk i of t w.r.t. q in chasek i(K) is also a witness of t w.r.t. q^.
To this aim, we prove that there exists q^ 2 Qr such that: { Gk i (the per-witness of t w.r.t. q) is a witness of t w.r.t. q^ and { jq^j = jGk ij, where jq^j indicates the number of atoms in the CQ q^. Then we can apply this claim for i = k, taking into consideration that chase0(K) = A.
Base step: (i=0) There exists q^ 2 Qr such that Gk is a witness of t w.r.t. q^ and jq^j = jGkj. This is an immediate consequence of the fact that q 2 Qr and that Qr is closed with respect to step (b) of the algorithm PerfectRef. Indeed, if jGkj < jqj then there exist two atoms g1, g2 in q and a membership 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 2 Qr (with q1 = reduce(q; g1; g2)) such that Gk is a witness of t w.r.t. q1 and jq1j = jqj 1. This step is exactly proved as in DL-LiteA, taking into consideration that our added function reducesingleton does not in uence the statement. . Now, if jGkj < jq1j, we can iterate the above argument, thus we conclude that there exists q^ 2 Qr such that Gk is a witness of t w.r.t. q^ and jq^j = jGkj. Inductive step: suppose that there exists q^ 2 witness of t w.r.t. q^ and jq^j = jGk i+1j.
Qr such that Gk i+1 is a Let us assume that chasek i+1(K) is obtained by applying cr2, cr2o, or cr2u to chasek 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 9P 3, where A is an atomic concept and P is an atomic role, is applied in chasek 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) 2 chasek i(K). Therefore, if P is not a restricted role, then we apply rule cr2, i.e., chasek i+1(K) = chasek i(K) [ fP (a; a00)g, 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 jq^j = jGk i+1j, 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 2 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 9P v fdg, 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 9P (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 jq1j = jGk ij, and in this case the claim is immediate; or jq1j = jGk ij + 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 2 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 9P , which is analogous. jq2j = jGk i+1j, which proves the claim. Note that the restricted roles are treated exactly like 9P , because the reducesingleton function will reduce them to such. C C.1
Let K = (Tp [ To [ Tf ; A) be a DL-LiteoA KB, and QO = WO2SC(T ) qO and QF = WF2Tf qF . Then, K is satis able i A 6j= QO and A 6j= QF . Proof. ")" if K is satis able, then per de nition it su ces all the assertions in Tp [ To [ Tf . Hence, taking into consideration that the queries qF ,QO are de ned to be true only when an an assertion is not satsi ed, we can say that A 6j= QO and A 6j= QF . "(" if A 6j= QO and A 6j= QF then the satisfaction of the nominal inclusion assertions, it follows from A 6j= QO that A = chase0(K) satis es SC(T )o, which makes them satis able 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 satis ed. This means that there exist x; y; z 2 can(K) such (x; y) and (x; z) are in Rcan(K), and y 6= z. Well, this can not occur in chase0(K) = A because of the non-satisfaction of the queries. Then there would exist an i such that chasei(K) satis es the functionality assertion, whereas chasei+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 generality we will only prove the case for the rst 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 element, but this is guaranteed by the de nition of the singleton closure. which is satis ed as above for the nominal inclusion assertions { For if cr2u is parallel to cr2o C.2
Proof. \(" We show that if hT [ Tn; Ai is unsatis able then hT ; Ai j= Qn. Consider the FOL formula being the conjenction of all assertions in K, in terms of rst-order logic, i.e.
= ^ ^ ^ 2Tn ^ ^ : from which we can observe that there should be a NI N 2 Tn such that hT ; Ai j= N , and therefore hT ; Ai 6j= Qn.
\)" We prove that if hT ; Ai j= Qn then K = hT [ Tn; Ai is unsatis able. If hT ; Ai j= Qn, them there is some NI N , such that If hT ; Ai j= qN , which implies that every model satisfying hT ; Ai satis es also qN . Taking into consideration the assumed satis ablity of the rst, we can deduce the satis ability of the latter. Meaning that there are some objects in the domain which contradict the NI N , i.e., hT ; Ai 6j= N , or hT ; Ai j= :N . By deduction, we have that hT [ fN g; Ai is unsatis able, making any KB containing it, including hT [ Tn; Ai not satis able.
^ ^
: