Recent papers address the issue of updating the instance level of knowledge bases expressed in Description Logic following a modelbased approach. One of the outcomes of these papers is that the result of updating a knowledge base K is generally not expressible in the Description Logic used to express K. In this paper we introduce a formula-based approach to this problem, by revisiting some research work on formulabased updates developed in the '80s, in particular the WIDTIO (When In Doubt, Throw It Out) approach. We show that our operator enjoys desirable properties, including that both insertions and deletions according to such operator can be expressed in the DL used for the original KB. Also, we present polynomial time algorithms for the evolution of the instance level knowledge bases expressed in DL-LiteA;id, which the most expressive Description Logics of the DL-Lite family.
Description Logics (DLs) are logics for expressing knowledge bases (KBs) constituted by two components, namely, the TBox, asserting general properties of concepts and roles (binary relations), and the ABox, which is a set of assertions about individuals that are instances of concepts and roles. It is widely accepted that such logics are well-suited for expressing ontologies, with the TBox capturing the intensional knowledge about the domain of interest, and the ABox expressing the knowledge about the instance level of the predicates de ned in the TBox. Following this idea, several Knowledge Representation Systems, called DL systems, have been recently built, providing methods and tools for managing ontologies expressed in DLs 1. Notice that numerous DLs have been studied in the last decades, with the goal of analyzing the impact of the expressive power of the DL language to the complexity of reasoning. Consequently, each DL system is tailored towards managing KB expressed in a speci c DL.
By referring to the so-called functional view of knowledge representation [
There are two types of evolution operators, corresponding to inserting, and deleting chunks of knowledge, respectively. In the case of insertion, the aim is to incorporate new knowledge into the KB, and the corresponding operator should be de ned in such a way to compute a consistent KB that supports the new knowledge. In the case of deletion, the aim is to come up with a consistent KB where the retracted knowledge is not valid. In both cases, the crucial aspect to take into account is that evolving a consistent knowledge base should not introduce inconsistencies.
While ASK operations have been investigated in detail by the DL community,
existing DL reasoners do not provide explicit services for KB evolution.
Nevertheless, many recent papers demonstrate that the interest towards a well-de ned
approach to KB evolution is growing signi cantly [
In this paper, we study the problem of DL KB evolution, by focusing our attention to scenarios characterized by the following elements:
(1) We consider the case where the evolution a ects only the instance level
of the KB, i.e., the ABox. In other words, we enforce the condition that the KB
resulting from the application of the evolution operators has the same TBox as
the original KB (similarly to [
(2) We aim at a situation where the KB resulting from the evolution can be expressed in the same DL as the original KB. This is coherent with our goal of providing the foundations for equipping DL systems with evolution operators: indeed, if a DL system S is able to manage KBs expressed in a DL L, the result of evolving such KBs should be expressible in L.
(3) The KBs resulting from the application of an evolution operator on two logically equivalent KBs should be mutually equivalent. In other words, we want the result to be independent of the syntactic form of the original KB.
Assumption (1), although limiting the generality of our approach, captures several interesting scenarios, including ontology-based data management, where the DL KB is used as a logic-based interface to existing data sources.
As for item (2), we note that virtually all model-based approaches su er
from the expressibility problem. This has been reported in many recent papers,
including [
Finally, to deal with item (3), we sanction that the notion of distance between KBs refers to the closure of the ABox of a KB, rather than to the ABox itself. The closure of an ABox A with respect to an TBox T is de ned as the set of all ABox assertions that logically follows from T and A. By basing the de nition of distance on the closure of ABoxes, we achieve the goal of making the result of our operators independent of the form of the original KB.
After a brief introduction to DLs (Section 2), we provide the de nition of
our evolution operators in Section 3. The remaining sections are devoted to
illustrating algorithms for deletion (Section 4), and insertion (Section 5) for
KBs expressed in the DL DL-LiteA;id, which is the most expressive logic in the
DL-Lite family [
Let S be a signature of symbols for individual (object and value) constants, and atomic elements, i.e., concepts, value-domains, attributes, and roles. If L is a DL, then an L-KB K over S is a pair hT ; Ai, where T , called TBox, is a nite set of intensional assertions over S expressed in L, and A, called ABox, is a nite set of instance assertions, i.e, assertions on individuals, over S expressed in L. Di erent DLs allow for di erent kinds of concept, attribute, and role expressions, and di erent kinds of TBox and ABox assertions over such expressions. In this paper we assume that ABox assertions are always atomic, i.e., they correspond to ground atoms, and therefore we omit to refer to L when we talk about ABox assertions.
The semantics of a DL KB is given in terms of interpretations. An
interpretation is a model of a KB K = hT ; Ai if it satis es all assertions in T [ A, where
the notion of satisfaction depends on the constructs allowed by the speci c DL
in which K is expressed. We denote the set of models of K with Mod (K).
2 Not to be confused with the set of DLs studied in [
Let T be a TBox in L, and let A be an ABox. We say that A is T -consistent if hT ; Ai is satis able, i.e. if M od(hT ; Ai) 6= ;, T -inconsistent otherwise. The T -closure of A with respect to T , denoted clT (A), is the set of all atomic ABox assertion that are formed with individuals in A, and are logically implied by hT ; Ai. Note that if hT ; Ai is an L-KB, then hT ; clT (A)i is an L-KB as well, and is logically equivalent to hT ; Ai, i.e., Mod (hT ; Ai) = Mod (hT ; clT (A)i). A is said to be T -closed if clT (A) = A. Finally, for an ABox assertion 1, we denote by SubsumeehT ;Ai( 1) the set of atoms 2 2 clT (A) such that hT ; Ai j= 2 1.
The DL-Lite family [
We now present the DL DL-LiteA;id, which is the most expressive logic in the family. Expressions in DL-LiteA;id are formed according to the following syntax: B Q T ! A j 9Q j (U ) ! P j P ! >D j T1 j j Tn
E V ! (U ) ! U j :U
C R ! B j :B ! Q j :Q where A, P , and U are symbols in S denoting respectively an atomic concept name, an atomic role name and an attribute name, T1; : : : ; Tn are all the valuedomains allowed in the logic (those corresponding to the data types adopted by Resource Description Framework (RDF)4), >D denotes the union of all domain values, P denotes the inverse of P , 9Q denotes the objects related to by the role Q, : denotes negation, (U ) denotes the domain of U , i.e., the set of objects that U relates to values, and (U ) denotes the range of U , i.e., the set of values related to objects by U .
A DL-LiteA;id TBox T contains intensional assertions of three types, namely
inclusion assertions, functionality assertions, and identi cation assertions [
Q v R (role inclusion) (id B 1; :::; n) (identi cation)
(funct U ) (attribute functionality ) In the identi cation assertions, denotes a path, which is an expression built according to the following syntax rule: ! S j B? j 1 2 where S denotes an atomic role, the inverse of an atomic role, or an atomic attribute, 1 2 denotes the composition of the paths 1 and 2, and B?, called test relation, represents the identity relation on instances of the concept B. In our logic, identi cation assertions are local, i.e., at least one i 2 f 1; :::; ng has length 1, i.e., it is an atomic role, the inverse of an atomic role, or an atomic attribute. In what follows, we only refer to IDs which are local. 3 http://www.w3.org/TR/2008/WD-owl2-profiles-20081008/ 4 http://www.w3.org/RDF/
The set of positive (resp., negative) inclusions in T will be denoted by T + (resp., T ), and the set of identi cation assertions in T will be denoted by Tid.
A concept inclusion assertion expresses that a (basic) concept B is subsumed by a (general) concept C. Analogously for the other types of inclusion assertions. Inclusion assertions that do not contain (resp. contain) the symbols ':' in the right-hand side are called positive inclusions (resp. negative inclusions ). Attribute functionality assertions are used to impose that attributes are actually functions from objects to domain values. An ID (id B 1; :::; n) asserts that for any two di erent instances a,b of B, there is at least one i such that a and b differ in the set of their i- llers. Note that IDs can be used to assert functionality of roles. Speci cally, the assertion (id 9Q Q ) imposes that Q is functional.
Finally, a TBox DL-LiteA;id T satis es the following condition: every role or attribute that occurs (in either direct or inverse direction) in a path of an ID 2 Tid or in a functional assertion, is not specialized in T 0, i.e., it does not appear in the right-hand side of assertions of the form Q v Q0 or U v U 0.
A DL-LiteA;id ABox A is a nite set of assertions of the form A(a), P (a; b), and U (a; v), where A, P , and U are as above, a and b are object constants in S, and v is a value constant in S.
Example 1. We consider a portion of the Formula One domain. We know that o cial drivers (OD) and test drivers (T D) are both team members (T M ), and o cial drivers are not test drivers. Every team member is a member of (mf ) a exactly one team (F T ), and every team has at most one o cial driver. Finally, no race director (RD) is a member of a team. We also know that s is the o cial driver of team t1, that b is a test driver, and that p is a team member. The corresponding DL-LiteA;id-KB K is: T : OD v T M T D v T M OD v :T D RD v :T M T M v 9mf
T M v :F T 9mf v T M 9mf v F T (id OD mf ) (id F T mf ) A: OD(s) mf (s; t1) T D(b) T M (p)
We conclude this section with a brief discussione on the complexity of reasoning about a DL-LiteA;id-KB hT ; Ai. Satis ability can be checked in polynomial time with respect to jT n Tidj and jAj, and in NP with respect to jTidj. Moreover, if hT ; Ai is satis able, then answering a query q posed to hT ; Ai can be done in polynomial time with respect to jT j and jAj, and in NP with respect to jqj. Finally, clT (A) can be computed in quadratic time with respect to jT j and jAj. 3
In this section we rst present our semantics for the evolution of DL knowledge bases at the instance level, and then we provide a comparison between our operator and other work in the literature.
In the rest of this section, L is a DL, and K = hT ; Ai is a satis able L-KB. In other words, we do not consider the evolution of unsatis able KBs. In addition, F is a nite set of atomic ABox assertions in L.
The following de nition speci es when a set of ABox assertions \realizes" the insertion or deletion of a set of ABox assertions with respect to K. De nition 1. Let A0 be an ABox. Then, A0 accomplishes the insertion of F into hT ; Ai if A0 is T -consistent, and hT ; A0i j= F (i.e., F clT (A0)). Similarly, A0 accomplishes the deletion of F from hT ; Ai if A0 is T -consistent, and hT ; A0i 6j= F (i.e., F 6 clT (A0)).
Obviously, we are interested in KBs which accomplish the evolution of a KB with a minimal change. In order to formalize the notion of minimal change, we rst need to provide some de nitions.
Let A1 and A2 be two ABoxes. Then, we say that A1 has fewer deletions than A2 with respect to hT ; Ai if clT (A) n clT (A1) clT (A) n clT (A2). Similarly, we say that A1 and A2 have the same deletions with respect to hT ; Ai if clT (A) n clT (A1) = clT (A) n clT (A2). Finally, we say that A1 has fewer insertions than A2 with respect to hT ; Ai if clT (A1) n clT (A) clT (A2) n clT (A). De nition 2. Let A1 and A2 be two ABoxes. Then, A1 has fewer changes than A2 with respect to hT ; Ai if A1 has fewer deletions than A2 with respect to hT ; Ai, or A1 and A2 have the same deletions with respect to hT ; Ai, and A! has fewer insertions than A2 with respect to hT ; Ai.
Now that we have de ned the relation of fewer changes between two KBs w.r.t. another one, we can de ne the notion of a KB which accomplishes the insertion (resp. deletion) of a set of facts into (resp. from) another KB minimally. De nition 3. Let A0 be an ABox. Then A0 accomplishes the insertion (deletion) of F into (from) hT ; Ai minimally if A0 accomplishes the insertion (deletion) of F into (from) hT ; Ai, and there is no A00 that accomplishes the insertion (deletion) of F into (from) hT ; Ai, and has fewer changes than A0 with respect to hT ; Ai.
With these notions in place, we can now de ne our evolution operator. De nition 4. Let U = fA1; : : : ; Ang be the set of all ABoxes accomplishing the insertion (deletion) of F into (from) hT ; Ai minimally, and let A0 be an ABox. Then, hT ; A0i is the result of changing hT ; Ai with the insertion (deletion) of F if (1) U is empty, and hT ; clT (A0)i = hT ; clT (A)i, or (2) U is nonempty, and hT ; clT (A0)i = hT ; T1 i n clT (Ai)i.
It is immediate to verify that, up to logical equivalence, the result of changing hT ; Ai with the insertion or the deletion of F is unique. In the rest of this paper, the result of changing K = hT ; Ai with the insertion (resp. deletion) of F according to our semantics will be denoted by K T\ F (resp. K T\ F ). Notice that, by de nition of our operator, in the case where F is T -inconsistent, the result of changing hT ; Ai with both the insertion and the deletion of F is logically equivalent to hT ; Ai itself.
Example 2. Consider the DL-LiteA;id KB K of the Example 1, and suppose that p becomes now a race director, and b becomes the new o cial driver of the team t1. To re ect this new information, we change K with the insertion of F1 = fRD(p); OD(b); mf (b; t1)g. Since the TBox implies that a race director cannot be a team member, RD(p) contradicts T M (p). Also, since every team has at most one o cial driver, OD(b) and mf (b; t1) contradict mf (s; t). According to De nition 3, the KBs accomplishing the insertion of F1 into K minimally are: K1 = hT ; fRD(p),OD(b),mf (b; t1),T M (s),mf (s; t1)gi
K2 = hT ; fRD(p),OD(b),mf (b; t1),T M (s),OD(s)gi Thus, K
T\ F1 is:
K3 = hT ; fRD(p),OD(b),mf (b; t1),T M (s)gi.
Now, suppose that we do not know anymore whether b is a member of t1, and, even more, whether b is a team member at all. Then, we change K3 with the deletion of F2 = fT M (b); mf (b; t1)g, thus obtaining
K3 T\ F2 = hT ; fRD(p),T M (s),OD(b)gi.
The following theorem is an adaptation to our setting of two results reported
in [
Theorem 1. Let A0 be an ABox. Then 1. A0 accomplishes the deletion of F from hT ; Ai minimally if and only if clT (A0) is a maximal T -closed subset of clT (A) such that F 6 clT (A0). 2. A0 accomplishes the insertion of F from hT ; Ai minimally if and only if clT (A0) = A00 [ clT (F ), where A00 is a maximal T -closed subset of clT (A) such that A00 [ F is T -consistent.
We end this section with a brief discussion on related work. We mentioned
in the introduction several model-based approaches to DL KB evolution, and
noticed that they all su er from the expressibility problem. This problem is also
shared by [
Related to our proposal are several formula-based approaches presented in
the literature. Perhaps, the closest approach to the one proposed in this paper
is that reported in [
Finally, we point out that, to our knowledge, the evolution operator presented in this work is the rst tractable evolution operator based on the WIDTIO principle. 4
We study deletion under the assumption that the DL language L is DL-LiteA;id. Thus, in this section, we implicitly refer to a DL-LiteA;id-KB K = hT ; Ai, and we address the problem of changing K with the deletion of a nite set F of ABox assertions. We assume that both hT ; Ai and hT ; F i are satis able.
We rst consider the case where the set F is constituted by just one assertion f . By exploiting Theorem 1, it is easy to conclude that there is exactly one KB accomplishing the deletion of ff g from a given KB.
Theorem 2. Let f be an ABox assertion. Up to logical equivalence, there is exactly one KB of the form hT ; A0i that accomplishes the deletion of ff g from hT ; Ai minimally, and such KB can be computed in polynomial time with respect to jT j and jAj.
Let us now consider the case of arbitrary F , i.e., the case where F = ff1; : : : ; fmg, for m 0. Suppose that, for every 1 i m, Ai accomplishes the deletion of ffig from hT ; Ai minimally. One might wonder whether the set 1 = fhT ; Aj i j Aj accomplishes the deletion of F minimally from hT ; Aig coincides (modulo logical equivalence) with 2 = fhT ; A1i; : : : hT ; Amig. The next theorem tells us that one direction is indeed valid: for each KB K1 2 1 there exists a KB K2 2 2 such that Mod (K1) = Mod (K2).
Theorem 3. If hT ; A0i accomplishes the deletion of ff1; : : : ; fmg from hT ; Ai minimally, then there exists i 2 f1::mg such that hT ; A0i accomplishes the deletion of ffig from hT ; Ai minimally.
However, the following example shows that the other direction does not hold: there may exist a K2 2 2 that is not logically equivalent to any K1 2 1. Example 3. Let T = fB v C; C v D; E v Dg, A = fB(a); E(a)g, and F = fC(a); D(a)g. It is easy to see that the deletion of D(a) from hT ; Ai is accomplished minimally by hT ; ;i, while the deletion of C(a) from hT ; Ai is accomplished minimally by hT ; fE(a)gi. Therefore, in this case, we have 2 = fhT ; ;i; hT ; fE(a)gig. Also, one can verify that hT ; fE(a)gi is the only (up to logical equivalence) KB accomplishing the deletion of F minimally, i.e., 1 = fhT ; fE(a)gig. Thus, there is a KB in 2, namely hT ; ;i, that is not logically equivalent to any KB in 1.
The next theorem characterizes when a given hT ; Aii 2 2 accomplishes the deletion of F minimally.
Theorem 4. Let F = ff1; : : : ; fmg, and, for every 1 i m, let hT ; Aii accomplish the deletion of ffig from hT ; Ai minimally. Then, hT ; Aj i, where j 2 f1::mg, accomplishes the deletion of F from hT ; Ai minimally if and only if there is no h 2 f1::mg such that h 6= j, and hT ; ffhgi j= fj .
By exploiting Theorems 2, 3, and 4, we can directly prove that K T\ F can be computed by the algorithm ComputeDeletion below. It is easy to see that the time complexity of the algorithm is O(jT j2 jF j2 + jAj2).
end Input: a satis able DL-LiteA;id KB K = hT ; Ai, a nite set of ABox assertions
F such that hT ; F i is satis able Output: a DL-LiteA;id KB begin
F 0 F ; foreach fi 2 F 0 and fj 2 F such that i 6= j do
if hT ; ffjgi j= fi then F 0 F 0 n ffig; return hT ; clT (A) n f 2 SubsumeeK(f ) j f 2 F 0gi;
Theorem 5. ComputeDeletion(hT ; Ai; F ) terminates, and computes hT ; Ai F in polynomial time with respect to jT j, jAj and jF j.
T \ 5
In this section, we refer to a DL-LiteA;id-KB K = hT ; Ai, and address the problem of changing K with the insertion of a nite set F of ABox assertions. As in the previous section, we assume that both hT ; Ai and hT ; F i are satis able.
Theorem 1 tells us that, in principle, we can compute the KB resulting from
the insertion of F into hT ; Ai by building all maximal subsets of A which are
T -consistent with F , and then computing their intersection. The main problem
to be faced with this method is that, depending on the DL used, there can
be an exponential number of maximal subsets A0 of clT (A) such that A0 [
ff g is T -consistent5.In particular, in DL-LiteA;id, building all maximal subsets
of A which are T -consistent with F , and then computing their intersection is
computationally costly. Fortunately, we show in the following that K T\ F can
be computed without computing all maximal consistent subsets of A with F .
5 Note that this cannot happen in those DLs of the DL-Lite family which do not admit
the use of identi cation assertions (such as the DL studied in [
To describe our method, we need some preliminary notions. A set V of ABox assertions is called a T -violation set for t 2 T nT + if hT +[ftg; V i is unsatis able, while for every proper subset V 0 of V , hT + [ ftg; V 0i is satis able. Any set V of ABox assertions that is a T -violation set for a t 2 T n T + is simply called a T -violation set.
We know from Theorem 1 that the ABox A0 accomplishes the insertion of F from hT ; Ai minimally if and only if clT (A0) = A00 [ clT (F ), where A00 is a maximal T -closed subset of clT (A) such that A00 [ F is T -consistent. Since we must compute the intersection of all such ABoxes A0, it is su cient to compute those assertions in clT (A) that are not in the intersection, and remove them from clT (A) [ clT (F ). All the assertions in clT (F ) are obviously in the intersection of the ABoxes A0. As for the ABox assertions in clT (A) n clT (F ), it is easy to see that one such assertion is not in the intersection of the ABoxes A0 if and only if there exists a maximal subset of clT (A) such that [ F is T -consistent, and does not contain .
Taking into account the above observation, the next theorem is the key to our solution.
Theorem 6. Let be an assertion in clT (A) n clT (F ). There exists a maximal subset of clT (A) such that [ F is T -consistent, and does not contain if and only if there is a T -violation set V in clT (A) [ clT (F ) such that 2 V , and F [ (V n f g) is T -consistent.
Theorem 6 suggests immediately the algorithm ComputeInsertion below for computing K T\ F .
end Input: a satis able DL-LiteA;id KB K = hT ; Ai, a nite set of ABox assertions
F such that hT ; F i is satis able Output: a DL-LiteA;id KB. begin
F 0 = ;; foreach 2 clT (A) n clT (F ) do if 9 a T -violation set V in clT (A) [ clT (F ) s.t. 2 V and
hT ; F [ (V n f g)i is satis able then F 0 F 0 [ f g; return hT ; F [ clT (A) n F 0i;
Algorithm ComputeInsertion requires to compute all T -violation sets in clT (A) [ clT (F ). It can be shown that this can be done by computing the results of suitable conjunctive queries posed to clT (A) [ clT (F ). Such queries are built out of the negative inclusion assertions and the identi cation assertions Tid in T , and essentially look for tuples that satisfy the negation of such assertions. From this observation, one can derive the following theorem.
Theorem 7. ComputeInsertion(hT ; Ai; F ) terminates, and computes hT ; Ai T\ F in polynomial time with respect to jT n Tidj, jAj, and jF j, and in NP with respect to jTidj.
We plan to continue our work along several directions. First, we aim at extending
our approach to the problem of evolution of the whole KB, as opposed to the
ABox only. Also, we will add the notion of protected part to our approach, to
model situations where one wants to prevent changes on speci c parts of the
KB when applying insertions or deletions. Finally, we aim at studying the case
where the KB contains other kinds of constraints, so as to capture the scenario
where updates are expressed on a conceptual model used as a global schema in
a data integration system [