An ABox Revision Algorithm for the Description Logic EL⊥ Liang Chang1,2 , Uli Sattler1 , and Tianlong Gu2 1 School of Computer Science, The University of Manchester, Manchester, M13 9PL, UK 2 Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin, 541004, China changl.guet@gmail.com,sattler@cs.manchester.ac.uk,cctlgu@guet.edu.cn Abstract. Revision of knowledge bases (KBs) expressed in description logics (DLs) has gained a lot of attention lately. Existing revision algo- rithms can be divided into two groups: model-based approaches (MBAs) and formula-based approaches (FBAs). MBAs are fine-grained and in- dependent of the syntactical forms of KBs; however, they only work for some restricted forms of the DL-Lite family. FBAs can deal with more expressive DLs such as SHOIN , but they are syntax-dependent and not fine-grained. In this paper, we present a new method for instance- level revision of KBs. In our algorithm, a non-redundant depth-bounded model is firstly constructed for the KB to be revised; then a revision process based on justifications is carried out on this model by treating a model as a set of assertions; finally the resulting model is mapped back to a KB which will be returned by the algorithm. Our algorithm is syntax-independent and fine-grained, and works for the DL EL⊥ . 1 Introduction Description logics (DLs) are playing a central role in the Semantic Web, serving as the basis of the W3C-recommended Web ontology language OWL [11]. The main strength of DLs is that they offer considerable expressive power going far beyond propositional logic, while reasoning is still decidable. Traditionally DLs have been used for representing and reasoning about knowl- edge of static application domains [2]. Recently, however, there are some research works focused on dynamic aspects of knowledge bases (KBs) based on DL. One typical application background for these research works is ontology evolution [9], where the goal is to incorporate new information N into an original ontol- ogy K and guarantee the consistency of resulting ontology K0 . This problem is also called KB revision in artificial intelligence [1]. Another typical application background is reasoning about actions [3, 6], where the purpose is to bring the KB up to date when the world is changed by the execution of actions which are described by DL assertions. This problem is called KB update [10, 12, 15]. In this paper we investigate the revision problem. A KB K based on DL is generally composed of two parts: a TBox T for representing intensional knowledge, and an ABox A for representing extensional knowledge. Let K = hT , Ai be an original KB and N a set of new information, then there are three types of revision problems based on DLs: (1) TBox revision, where N consists of TBox assertions only and A is empty [16, 17]; (2) ABox revision, where N consists of ABox assertions only and T is assumed to be fixed [13, 14]; (3) KB revision, where N consists of both TBox assertions and ABox assertions [5, 18, 19]. In this paper we focus on the ABox revision problem. In order to capture the basic ideas and properties of revision, some postulates were proposed and well-studied in the literature [1, 12, 8]. According to these postulates, a revision operator or algorithm should hold the following properties: R1: must preserve the consistency of KBs; R2: must entail the new information and preserve the protected part; R3: should not change the original KB if there is no conflict; R4: should be independent of the syntactical forms of KBs; and R5: should guarantee a minimal change. Among these properties the last one is not precisely specified, since there are different approaches to define minimality for different applications; it is well- accepted that there is no general notion of minimality that will do the right thing under all circumstances [5]. According to the semantics adopted for defining minimality, existing revision operators and algorithms can be divided into two groups: model-based approaches (MBAs) and formula-based approaches (FBAs). In model-based approaches, the semantics of minimal change is defined by measuring the distance between the models of new information N and the models of original KB K [13]. An advantage of MBAs is that they are independent of the syntactical forms of the KB. However, although they work well for propositional logic, it is difficult to adapt them to DLs. Until now, they are only applied in the DL-Lite family for revision problems [13, 17, 18]. In formula-based approaches, the semantics of minimal change is reflected in the minimality of formulas which will be changed. One group of FBAs is based on the deductive closure of KBs; they are powerful enough to guarantee syntax- independent but only works for restricted forms of DL-Lite [5, 14]. Another group of FBAs is based on justifications; they and capable for processing DLs such as SHOIN , but are syntax-dependent and not fine-grained [16, 19]. In this paper we present a new method for ABox revision problem. Compared to MBAs and the FBAs based on deductive closures, our method is capable to support the DL EL⊥ . Compared to the FBAs based on justifications, our method is syntax-independent and fine-grained for the minimal change principle. The proofs of all of our technical results are given in the technical report [7]. 2 The Description Logic EL⊥ The DL EL⊥ extends EL with bottom concept (and consequently disjointness statements) [4]. Let NC , NR and NI be disjoint sets of concept names, role names and individual names, respectively. EL⊥ -concepts are built according to the syntax rule C ::= > | ⊥ | A | C u D | ∃r.C, where A ∈ NC , r ∈ NR , and C, D range over EL⊥ -concepts. The semantics is defined by means of an interpretation I = (∆I , ·I ), where the interpretation domain ∆I is a non-empty set composed of individuals, and ·I is a function which maps each concept name A ∈ NC to a set AI ⊆ ∆I , maps each role name r ∈ NR to a binary relation rI ⊆ ∆I × ∆I , and maps each individual name a ∈ NI to an individual aI ∈ ∆I . The function ·I is inductively extended to arbitrary concepts by setting >I := ∆I , ⊥I := ∅, (C u D)I := C I ∩ DI , and (∃r.C)I := {x ∈ ∆I | there exists y ∈ ∆I such that (x, y) ∈ rI and y ∈ C I }. A TBox T is a finite set of general concept inclusions (GCIs) of the form C v D, where C and D are concepts. An ABox A is a finite set of concept assertions of the form C(a) and role assertions of the form r(a, b), where a, b ∈ NI , r ∈ NR and C is a concept. A knowledge base (KB) is a pair K = hT , Ai. The satisfaction relation “|=” is defined inductively as follows: I |= C v D iff C I ⊆ DI ; I |= T iff I |= X for every X ∈ T ; I |= C(a) iff aI ∈ C I ; I |= r(a, b) iff (aI , bI ) ∈ rI ; and I |= A iff I |= X for every X ∈ A. I is a model of a KB K = hT , Ai if I |= T and I |= A. We use mod(K) to denote the set of models of a KB K. Two KBs K1 and K2 are equivalent (written K1 ≡ K2 ) iff mod(K1 ) = mod(K2 ). A KB K = hT , Ai is consistent (or A is consistent w.r.t. T ) if mod(K) 6= ∅. A KB K entails a GCI, assertion or ABox X (written K |= X) if I |= X for every I ∈ mod(K). It is obvious that K is inconsistent iff K |= > v ⊥ iff K |= ⊥(a) for some individual name a occurring in K. We say that K entails a clash if K is inconsistent. Let X be a concept, GCI, ABox assertion, TBox, ABox or KB, then NCX (resp., NRX and NIX ) is the set of concept names (resp., role names and individual names) occurring in X, and sig(X) = NCX ∪ NRX ∪ NIX . For any concept C, the role depth rd(C) is the maximal nesting depth of “∃” in C. Let X be anSABox or TBox, sub(X) = {C | C(a) ∈ X} if X is an ABox, and sub(X) = {C, D} if X is a TBox, then the depth of X is defined as CvD∈X depth(X) = max{rd(C) | C ∈ sub(X)}. 3 ABox Revision for EL⊥ Firstly we define the ABox revision problem in EL⊥ as follows. Definition 1. An EL⊥ KB K = hT , Ai and an ABox N is a revision setting if N is consistent w.r.t. T . A KB K0 = hT , A0 i is a solution for a revision setting K = hT , Ai and N if K is consistent and K0 |= N . 0 In a revision setting, K = hT , Ai is called original KB and N is new in- formation. The task is to incorporate new information into original KB while preserving the TBox T and guaranteeing the consistency of KB. If we only consider the requirements on solutions specified in the above def- inition, then a straightforward solution for a revision setting K = hT , Ai and N is the KB K00 = hT , N i. However, obviously it is not a “good” solution, since information contained in the ABox A is completely lost. Therefore, besides the two necessary requirements, we hope that a solution has the properties specified by R3-R5 in Section 1 of the paper. In the following subsections, we will show that existing revision approaches not work well for EL⊥ with respect to these properties, and then illustrate our method by an example. 3.1 Model-based Approaches MBAs define revision operators over the distance between interpretations [13]. Let K  N be the set of models for the solution of revision setting, then K  N is generated by choosing models of hT , N i that are minimally distant from the models of K, i.e., K  N = {J ∈ mod(hT , N i) | there exists I ∈ mod(K) such that dist(I, J ) = min{dist(I 0 , J 0 ) | I 0 ∈ mod(K), J 0 ∈ mod(hT , N i)} }. Let Σ be the set of concept names and role names occurring in K and N . There are four different approaches for measuring the distance dist(I, J ): – dists] (I, J ) = ]{X ∈ Σ | X I 6= X J }, – dists⊆ (I, J ) = {X ∈ Σ | X I 6= X J }, – dista] (I, J ) = sum ](X I X J ), X∈Σ – dista⊆ (I, J , X) = X I X J for every X ∈ Σ, where X I X J = (X I \ X J ) ∪ (X J \ X I ). Distances under dists] and dista] are natural numbers and are compared in the standard way. Distances under dists⊆ are sets and are compared by set inclusion. Distances under dista⊆ are compared as follows: dista⊆ (I1 , J1 ) ≤ dista⊆ (I2 , J2 ) iff dista⊆ (I1 , J1 , X) ⊆ dista⊆ (I2 , J2 , X) for every X ∈ Σ. It is assumed that all models have the same interpretation domain and the same interpretation on individual names. In [13], the above four different semantics are denoted as G]s , G⊆ s , G]a , and G⊆ a respectively. It was shown that, under these semantics, the ABox revision problem in DL- Lite suffers from inexpressibility (i.e., the result of revision cannot be expressed in DL-Lite) [5, 13]. The reason is that the authors hope to compute a KB K0 = hT , A0 i such that mod(K0 ) = K  N , and the minimality principle of change intrinsically introduces implicit disjunction which is not supported by DL-Lite. Since EL⊥ does not support disjunction, it is obvious that it suffers from the same problem of inexpressibility. However, in this paper, we do not require the solution to be a single KB. In the case that implicit disjunction is introduced by the revision process, we will generate more than one KBs Ki0 (1 ≤ i ≤ n) such mod(Ki0 ) = K  N . As a result, the cause for inexpressibility studied S that 1≤i≤n in [5, 13] is avoided here. There are two reasons for us to permit multi solutions. Firstly, in some ap- plications, what we care about is to check whether an assertion ϕ holds or not after the revision process. In this case, we can represent all the possible solutions as a set of KBs, and check whether ϕ holds or not in each KB. Secondly, the implicit disjunction introduced by revision process means that there are different possible results for the revision process. We can compute and represent all the possible results as a set of KBs and let the user or experts to select the best one. However, although the inexpressibility problem studied in [5, 13] can be solved by permitting multi solutions (or disjunctive KB), if we adopt MBAs, then there exists another cause of inexpressibility for ABox revision in EL⊥ . Example 1. Consider the revision setting K1 = hT , A1 i and N = {E(a)}, where T = {A v ∃R.A, A v C, E u ∃R.A v ⊥}, A1 = {A(a)}. s Firstly, we apply the semantics G⊆ and G]s . Let Σ = {A, C, E, R}. It is obvious that, for any interpretations I ∈ mod(K1 ) and J ∈ mod(hT , N i), it must be AI 6= AJ and E I 6= E J . Therefore, {A, E} is the minimal set of signatures s whose interpretations must be changed. So, under both G⊆ and G]s , we have that K1  N = {J ∈ mod(hT , N i) | there exists I ∈ mod(K1 ) such that X I = X J f or any X ∈ Σ \ {A, E}}. For every positive integer k, construct an interpretation Jk = (∆Jk , ·Jk ) as follows: ∆Jk = {x1 , ..., xk }, aJk = x1 , AJk = ∅, E Jk = {x1 }, C Jk = {x1 , ..., xk }, and RJk = {(x1 , x2 ), ..., (xk−1 , xk ), (xk , xk )}. It is obvious that Jk ∈ mod(hT , N i). Furthermore, let Ik = (∆Ik , ·Ik ) be an interpretation with ∆Ik = ∆Jk , aIk = aJk , AIk = {x1 , ..., xk }, E Ik = ∅, C Ik = C Jk , and RIk = RJk . Then it is obvious that Ik ∈ mod(K1 ) and consequently Jk ∈ K1  N . 0 0 For every positive integer k, construct another interpretation Jk0 = (∆Jk , ·Jk ) 0 0 0 0 0 as follows: ∆Jk = {x1 , ..., xk }, aJk = x1 , AJk = ∅, E Jk = {x1 }, C Jk = {x1 , ..., xk }, 0 and RJk = {(x1 , x2 ), ..., (xk−1 , xk )}. Then, although Jk0 ∈ mod(hT , N i), there 0 0 is no interpretation Ik0 ∈ mod(K1 ) with RIk = RJk . So, we have Jk0 ∈ / K1  N . s s Now, suppose solution for the revision setting under S ⊆ G and G ] is a finite number of KBs Ki0 = hT , A0i i (1 ≤ i ≤ n) such that mod(Ki0 ) = K1  N . 1≤i≤n Consider the case that k ≥ 2. From Jk ∈ K1  N , there must be some solution Ki0 = hT , A0i i (1 ≤ i ≤ n) such that Jk ∈ mod(Ki0 ). At the same time, from Jk0 / K1  N , we have Jk0 ∈ ∈ / mod(Ki0 ). Therefore, the ABox A0i must contain some concept assertion X(a) such that the role depth rd(X) equals k. Since the value of k can be infinitely big, such an ABox does not exist. In other words, solutions s under the semantics G⊆ and G]s can not be expressed. a Secondly, we apply the semantics G⊆ and G]a . It is obvious that, for any inter- pretations I ∈ mod(K1 ) and J ∈ mod(hT , N i), it must be aI ∈ AI , aJ ∈ E J , aJ ∈/ AJ , and aI ∈ / E I . Therefore, under G]a , we have min{dista] (I 0 , J 0 ) | I 0 ∈ 0 mod(K1 ), J ∈ mod(hT , N i)} = 2; under G⊆ a , we have min{dista⊆ (I 0 , J 0 , X)| I ∈ mod(K1 ), J ∈ mod(hT , N i)} = {a} for X ∈ {A, E}, and min{dista⊆ (I 0 , J 0 , 0 0 X) | I 0 ∈ mod(K1 ), J 0 ∈ mod(hT , N i)} = ∅ for X ∈ Σ \ {A, E}. So, under both a G⊆ and G]a , we have K1  N = {J ∈ mod(hT , N i) | there exists I ∈ mod(K1 ) such that AI AJ = E I E J = {aI }, and X I = X J f or any X ∈ Σ \ {A, E}}. We can construct a KB K10 = hT , {E(a), C(a), R(a, a)}i that satisfies mod(K10 ) = K1  N . Therefore, under both G⊆ a and G]a , K10 is a solution for the revision setting. However, this solution is very strange, since there seems to be no “good” reason to enforce the assertion R(a, a) to hold. t u To sum up, there are four notions of computing models in existing MBAs. For the ABox revision problem in EL⊥ , two notions suffer from inexpressibility and the other two notions are semantically questionable. 3.2 Formula-based Approaches There are two typical formula-based approaches. The first one is based on de- ductive closures [5, 14]. Given an ABox revision setting K = hT , Ai and N , it firstly calculates the deductive closure of A w.r.t. T (denoted clT (A)), and then computes a maximal subset of clT (A) that does not conflict with N and T . This method works for restricted forms of DL-Lite, where the ABox A only contains assertions of the form A(a), ∃R(a) and R(a, b), with A and R concept names or role names. With such an assumption, clT (A) is finite and can be calculated effectively. However, it does not work for EL⊥ , since in our revision setting we allow any assertion constructed on EL⊥ concepts occurring in the ABox A. The second FBA is based on justifications [19]. Given an ABox revision setting K = hT , Ai and N , it firstly constructs a KB K0 = hT , A ∪ N i and finds all the minimal subsets of K0 that entail a clash (i.e., all justifications for clashes); then it computes a minimal set R ⊆ A which contains at least one element from each justification; finally it returns K0 = hT , (A ∪ N ) \ Ri as a solution. Obviously this approach can deal with EL⊥ . However, as shown by the following examples, it is neither fine-grained nor syntax-independent. Example 2. Consider the revision setting K1 = hT , A1 i and N described in the previous example. It is obvious that hT , A1 ∪ N i |= ⊥(a) and for which there is only one justification J = {A v ∃R.A, E u ∃R.A v ⊥, A(a), E(a)}. Since T is protected and E(a) ∈ N , our only choice is to remove A(a) from A1 ∪ N and get a solution K10 = hT , {E(a)}i. This solution is not so good, since it loses many information which is entailed by K1 and not conflicted with N , such as the assertions C(a) and ∃R.C(a). t u Example 3. Consider another revision setting K2 = hT , A2 i and N , where A2 = {A(a), C(a), ∃R.C(a)}. Apply the FBA based on justifications again, we will get a solution K20 = hT , {E(a), C(a), ∃R.C(a)}i. Since the KBs K1 and K2 are logically equivalent, it is unhelpful that we get two different solutions w.r.t. the same new information N . t u To sum up, for ABox revision in EL⊥ , existing FBAs either can not be applied directly, or can be applied but is syntax-dependent and not fine-grained. 3.3 Our Approach Our method is composed of three steps. Given an ABox revision setting K = hT , Ai and N , we firstly construct a non-redundant depth-bounded model G (called k-MW in this paper) for the initial KB K, and treat G as an ABox AG which contains some auxiliary variables. Then we execute a justification-based revision process on the KB K0 = hT , AG i plus the new information N , and get a consistent KB K0 = hT , (AG \ R) ∪ N i. Finally we map AG \ R back into an ABox A0 by “rolling up” auxiliary variables, and get a solution K0 = hT , A0 ∪N i. Example 4. Consider the revision setting K1 = hT , A1 i and N described in Example 1. Firstly, since max{depth(K1 ), depth(N )} = 1, we will introduce two variables x1 , x2 , and construct a 1-MW G for the KB K1 (details will be given in Section 4.1 and 4.2). By treating G as an ABox, we get AG = {A(a), C(a), R(a, x1 ), A(x1 ), C(x1 ), R(x1 , x2 ), A(x2 ), C(x2 )}. Secondly, for the clash hT , AG ∪N i |= ⊥(a), there are two justifications: J1 = {A v ∃R.A, Eu∃R.A v ⊥, E(a), A(a)} and J2 = {Eu∃R.A v ⊥, E(a), R(a, x1 ), A(x1 )}. Since T is protected and E(a) ∈ N , we can get two possible minimal repairs for removing the clash: R1 = {A(a), A(x1 )} and R2 = {A(a), R(a, x1 )}. However, since R2 contains a role assertion R(a, x1 ) where x1 a variable, all the information related to x1 will be lost if we apply R2 as a repair. Therefore, we choose R1 as the repair and get a consistent KB K0 = hT , (AG \ R1 ) ∪ N i = hT , {C(a), R(a, x1 ), C(x1 ), R(x1 , x2 ), A(x2 ), C(x2 )} ∪ N i. Finally, by rolling up variables occurring in the ABox of K0 , we get a solution K0 = hT , {C(a), ∃R.(C u ∃R.(A u C))(a), E(a)}i. t u In our solution, information contained in K1 is inherited as more as possible. Furthermore, as we will see later, since the depth-bounded model G constructed in the first step is non-redundant, our solution is syntax-independent. 4 ABox Revision Algorithm for EL⊥ Before presenting our revision algorithm, we introduce three procedures which will be used in the revision algorithm. 4.1 Calculating Witness for Knowledge Base The first procedure will construct a possibly redundant depth-bounded model for the initial KB based on a structure named revision graph. A revision graph for EL⊥ is a directed graph G = (V, E, L), where – V is a finite set of nodes composed of individual names and variables; – E ⊆ V × V is a set of edges satisfying: • there is no edge from variables to individual names, and • for each variable y ∈ V , there is at most one node x with hx, yi ∈ E; – each node x ∈ V is labelled with a set of concepts L(x); and – each edge hx, yi ∈ E is labelled with a set of role names L(hx, yi); further- more, if y is a variable then ]L(hx, yi) = 1. For each edge hx, yi ∈ E, we call y a successor of x and x a predecessor of y. Descendant is the transitive closure of successor. For any node x ∈ V , we use level(x) to denote the level of x in the graph, and define it inductively as follows: level(x) = 0 if x is an individual name, level(x) = level(y) + 1 if x is a variable with a predecessor y, and level(x) = +∞ if x is a variable without predecessor. Procedure 1 Given a KB K = hT , Ai and a non-negative integer k, construct a revision graph G = (V, E, L) by the following steps: Step 1. Initialize the graph G as: – V = NIK , – L(a) = {C | C(a) ∈ A} for each node a ∈ V , – E = {ha, bi | there is some R with R(a, b) ∈ A}, – L(ha, bi) = {R | R(a, b) ∈ A} for each edge ha, bi ∈ E. Step 2. Expand the graph by applying the following rules, until none of these rules is applicable: GCIInd -rule: if x ∈ NIK , C v D ∈ T , D ∈ / L(x), and hT , Ai |= C(x), then set L(x) = L(x) ∪ {D}. GCIV ar -rule: if x ∈ / NIK , C v D ∈ T , D ∈ / L(x), and hT , {E(x) | E ∈ L(x)}i |= C(x), then set L(x) = L(x) ∪ {D}. u-rule: if C1 u C2 ∈ L(x), and {C1 , C2 } * L(x), then set L(x) = L(x) ∪ {C1 , C2 }. ∃-rule: if ∃R.C ∈ L(x), x has no successor z with C ∈ L(z), and level(x) ≤ k, then introduce a new variable z, set V = V ∪ {z}, E = E ∪ {hx, zi}, L(z) = {C}, and L(hx, zi) = {R}. Step 3. Return the graph G = (V, E, L). Given any KB K = hT , Ai and non-negative integer k, we call the revision graph G returned by Procedure 1 a k-role-depth-bounded witness (k-W) for K. Revision graphs can be seen S as ABoxes with variables. Given S a revision graph G = (V, E, L), we call AG = {C(x) | C ∈ L(x)} ∪ {R(x, y) | R ∈ x∈V hx,yi∈E L(hx, yi)} as the ABox representation of G, and call G as the revision-graph representation of AG . Proposition 1. Let G = (V, E, L) be a k-W for a KB K = hT , Ai, and let AG be the ABox representation of G. Then, for any ABox assertion α with sig(α) ⊆ sig(K) and depth(α) ≤ k, K |= α iff h∅, AG i |= α. 4.2 Calculating Minimal Witness for Knowledge Base A k-W of KB possibly contains some redundant information which will make two logically equivalent KBs have different witnesses. In this subsection, we introduce a procedure to remove these redundant information. A graph B = (V 0 , E 0 , L0 ) is a branch of a revision graph G if B is a tree and a subgraph of G. A branch B1 = (V1 , E1 , L1 ) is subsumed by another branch B2 = (V2 , E2 , L2 ) if B1 and B2 have the same root node, ](V1 ∩ V2 ) = 1, and there is a function f : V1 → V2 such that: f (x) = x if x is the root node, L1 (x) ⊆ L2 (f (x)) for every node x ∈ V1 , hf (x), f (y)i ∈ E2 for every edge hx, yi ∈ E1 , and L1 (hx, yi) ⊆ L2 (hf (x), f (y)i) for every edge hx, yi ∈ E1 . A branch B is redundant in G if every node in B except the root is a variable, and B is subsumed by another branch in G. Procedure 2 Given a KB K = hT , Ai and a non-negative integer k, let G = (V, E, L) be a k-W for K, construct a revision graph G 0 = (V 0 , E 0 , L0 ) by the following steps: Step 1. Initialize the graph G 0 = (V 0 , E 0 , L0 ) as – V 0 = V , E 0 = E, L0 (hx, yi) = L(hx, yi) for every hx, yi ∈ E 0 , and – L0 (x) = {C ∈ L(x) | C is a concept name} for every x ∈ V 0 . Step 2. Prune G 0 by the following rule until the rule is not applicable: R-rule: if there is a redundant branch B = (VB , EB , LB ) in G 0 , then set E 0 = E 0 \ EB and V 0 = V 0 \ (VB \ {xB }), where xB is the root of B. Step 3. Return the graph G 0 . For any KB K and non-negative integer k, we call the graph G 0 returned by Procedure 2 a k-role-depth-bounded minimal witness (k-MW) for K. Proposition 2. Let G 0 be a k-MW for a KB K = hT , Ai, and let AG 0 be the ABox representation of G 0 . Then, for any ABox assertion α with sig(α) ⊆ sig(K) and depth(α) ≤ k, K |= α iff h∅, AG 0 i |= α. The following proposition states that, for any logically equivalent KBs K and K0 , their k-MW are identical up to variable renaming in the case that k is sufficiently large. Proposition 3. Let Ki = hT , Ai i (i = 1, 2) be two consistent KBs, let k be an integer with k ≥ depth(T ), k ≥ depth(A1 ) and k ≥ depth(A2 ), and let Gi = (Vi , Ei , Li ) be a k-MW for Ki (i = 1, 2). If mod(K1 ) = mod(K2 ), then there is a bijection f : V1 → V2 such that – f (x) = x if x is an individual name, – L1 (x) = L2 (f (x)) for every node x ∈ V1 , – hx, yi ∈ E1 iff hf (x), f (y)i ∈ E2 , and – L1 (hx, yi) = L2 (hf (x), f (y)i) for every edge hx, yi ∈ E1 . 4.3 Transforming a Witness Back into a Knowledge Base In this subsection we introduce a procedure to transform a revision graph into an ABox without variables. Procedure 3 Given a TBox T and a revision graph G = (V, E, L), construct an ABox by the following steps: Step 1. Delete from V all the variables which are not descendants of any indi- vidual names in G. Step 2. Roll up the graph G by applying the following substeps repeatedly, until there is no variable contained in V : 1. Select a variable y ∈ V that has no successor. 2. Let x be the predecessor of y. d 3. If L(y) 6= ∅, then let Cy be the concept C, else let Cy be >. C∈L(y) 4. If hT , {D(x) | D ∈ L(x)}i 6|= (∃R.Cy )(x), then set L(x) = L(x) ∪ {∃R.Cy }, where R is the role name contained in L(hx, yi). 5. Set E = E \ {hx, S yi} and V = V \ {y}. S Step 3. Return A = {C(x) | C ∈ L(x)} ∪ {R(x, y) | R ∈ L(hx, yi)}. x∈V hx,yi∈E Proposition 4. For any revision graph G and TBox T , let A be the ABox returned by Procedure 3, and let AG be the ABox representation of G. Then, hT , AG i |= A. 4.4 The Revision Algorithm Given a TBox T and two ABoxes A and N , if hT , A ∪ N i |= > v ⊥, then: – a set J ⊆ A is a (A, N )-justification for clash w.r.t. T if hT , J ∪ N i |= > v ⊥ and hT , J 0 ∪ N i 6|= > v ⊥ for every J 0 ⊂ J ; – a set R ⊆ A is a (A, N )-repair for clash w.r.t. T if ](R ∩ J ) = 1 for every J which is an (A, N )-justification for clash w.r.t. T . Now we are ready to present our ABox revision algorithm. Algorithm 1 Given a revision setting K = hT , Ai and N , given a non-negative integer k, construct a finite number of KBs by the following steps: Step 1. If A ∪ N is consistent w.r.t. T , then return K0 = hT , A ∪ N i, else continue the following steps. Step 2. Construct a k-MW G for K. Step 3. Let AG be the ABox representation of G. Calculate all the (AG , N )- repairs R1 , ..., Rn for clash w.r.t. T . Step 4. For each Ri (1 ≤ i ≤ n) do the following operations: 1. Construct an ABox Ai = AG \ Ri . 2. Let Gi be the revision-graph representation of Ai . Call Procedure 3 to generate an ABox A0i by taking T and Gi as inputs. 3. Construct a KB Ki0 = hT , A0i ∪ N i. Step 5. Let S = {K10 , ..., Kn0 }. For each Ki0 = hT , A0i ∪N i ∈ S, if there is another Kj0 ∈ S such that Kj0 |= A0i ∪ N , then remove Ki0 from S. Step 6. Return all the KBs contained in S. The following theorems state that our algorithm satisfies the properties spec- ified by R1-R4 in Section 1 of the paper. Theorem 1. For any revision setting K = hT , Ai and N , let K0 = hT 0 , A0 i be any KB returned by Algorithm 1. Then, (1) K0 is consistent, (2) K0 |= N and T 0 = T , and (3) A0 = A ∪ N if A ∪ N is consistent w.r.t. T . Theorem 2. Given any two revision settings Ki = hT , Ai i and Ni (i = 1, 2), and any integer k such that k ≥ depth(X) for X ∈ {T , A1 , A2 , N1 , N2 }. If K1 ≡ K2 and hT , N1 i ≡ hT , N2 i, then for any KB K10 returned by Algorithm 1 for the revision setting K1 and N1 , there must be a KB K20 returned by the algorithm for the revision setting K2 and N2 such that K10 ≡ K20 . Theorem 2 is based on Proposition 3 where k is required to be sufficiently large. Theorem 1 has no requirement on k; the first result of it is based on Proposition 4, and the other two results are obvious from the algorithm. In our algorithm, the k-MW G for the KB K is in fact a non-redundant k-depth-bounded model for K. Therefore, our revision process works on fine- grained representation of models and guarantees the minimal change principle in a fine-grained level. So, our algorithm satisfies the property specified by R5. Theorem 3. For any revision setting K = hT , Ai and N , assume the role depth of every concept occurring in K and N is bounded by some integer k, then Al- gorithm 1 runs in time exponential with respect to the size of K and N . 5 Conclusion We studied instance level KB revision in EL⊥ . There are two main families of approaches to revision: model-based ones and formula-based ones. We illustrated that they both have disadvantages and are inappropriate for EL⊥ . We presented a new method for the revision problem. Our method is closer in spirit to the formula-based approaches, but it also inherits some ideas of model-based ones. We showed that our algorithm behaves well for EL⊥ in that it satisfies the postulates proposed in the literature for revision operators. For future work, we will extend our method to support ABox revision in EL++ . Another work is to formalize the notion of minimality of change. Finally, we will make an optimization to the algorithm and test the feasibility of it in practice. Acknowledgments. This work was partially supported by the National Nat- ural Science Foundation of China (Nos. 61363030, 61262030) and the China Scholarship Council. References 1. Alchourrón, C. E., Gärdenfors, P., Makinson, D.: On the logic of theory change: partial meet contraction and revision functions. J. Symbolic Logic, 50(2): 510-530, 1985. 2. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F.: The description logic handbook: theory, implementation and applications. Cambridge University Press, Cambridge, 2003. 3. Baader, F., Lutz, C., Miličić, M., Sattler, U., Wolter., F.: Integrating description logics and action formalisms: first results. In Proc. of AAAI’05, 572-577, 2005. 4. Baader,F., Brandt, S., Lutz, C.: Pushing the EL Envelope. In Proc. of IJCAI’05, 364-369, 2005. 5. Calvanese, D., Kharlamov, E., Nutt, W., Zheleznyakov, D.: Evolution of DL-lite knowledge bases. In Proc. of ISWC’10, 112-128, 2010. 6. Chang, L., Shi, Z.Z., Gu, T.L., Zhao, L.Z.: A family of dynamic description logics for representing and reasoning about actions. J. Automated Reasoning, 49:1-52, 2012. 7. Chang, L., Sattler, U., Gu, T.L.: Algorithm for adapting cases represented in a tractable description logic, 2014. arXiv: 1405.4180. 8. Flouris, G., Plexousakis, D., Antoniou, G.: On applying the AGM theory to DLs and OWL. In Proc. of ISWC’05, 216-231, 2005. 9. Flouris, G., Manakanatas, D., Kondylakis, H., Plexousakis, D., Antoniou, G.: Ontol- ogy change: classification and survey. Knowledge Eng. Review, 23(2):117-152, 2008. 10. Giacomo, G.D., Lenzerini, M., Poggi, A., Rosati, R.: On the update of description logic ontologies at the instance level. In Proc. of AAAI’06, 1271-1276, 2006. 11. Horrocks, I., Patel-Schneider, P.F., Harmelen, F.V.: From SHIQ and RDF to OWL: the making of a web ontology language. J. of Web Semantics, 1(1):7-26, 2003. 12. Katsuno, H., Mendelzon, A. O.: On the difference between updating a knowledge base and revising it. In Proc. of KR’91, 387-394, 1991. 13. Kharlamov, E., Zheleznyakov, D.: Capturing instance level ontology evolution for DL-Lite. In Proc. of ISWC’11, 321-337, 2011. 14. Lenzerini, M., Savo, D. F.: On the evolution of the instance level of DL-Lite knowl- edge bases. In Proc. of DL’11, 2011. 15. Liu, H., Lutz, C., Miličić, M., Wolter, F.: Updating description logic ABoxes. In Proc. of KR’06, 46-56, 2006. 16. Qi, G., Haase, P, Huang, Z., Ji Q, Pan J. Z., Völker J.: A kernel revision operator for terminologies - algorithms and evaluation. In Proc. of ISWC’08, 419-434, 2008. 17. Qi, G., Du, J.: Model-based revision operators for terminologies in description logics. In Proc. of IJCAI’09, 891-897, 2009. 18. Wang, Z., Wang, K., Topor, R.W.: A new approach to knowledge base revision in DL-Lite. In Proc. of AAAI’10, 369-374, 2010. 19. Wiener, C. H., Katz, Y., Parsia, B.: Belief base revision for expressive description logics. In Proc. of OWLED’06, 10-11, 2006.