=Paper= {{Paper |id=Vol-1193/paper_64 |storemode=property |title=An ABox Revision Algorithm for the Description Logic EL_bot |pdfUrl=https://ceur-ws.org/Vol-1193/paper_64.pdf |volume=Vol-1193 |dblpUrl=https://dblp.org/rec/conf/dlog/ChangSG14 }} ==An ABox Revision Algorithm for the Description Logic EL_bot== https://ceur-ws.org/Vol-1193/paper_64.pdf
          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.