=Paper=
{{Paper
|id=Vol-477/paper-29
|storemode=property
|title=Revision of DL-Lite Knowledge Bases
|pdfUrl=https://ceur-ws.org/Vol-477/paper_27.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/WangWT09
}}
==Revision of DL-Lite Knowledge Bases==
https://ceur-ws.org/Vol-477/paper_27.pdf
Revision of DL-Lite Knowledge Bases
Zhe Wang, Kewen Wang, and Rodney Topor
Griffith University, Australia
Abstract. We address the revision problem for knowledge bases (KBs) in De-
scription Logics (DLs). This problem has received much attention in the ontology
management and DL communities, but the existing proposals are restricted in sev-
eral ways. In this paper we develop a formal framework for revision of DL-Lite
KBs, using techniques that are analogous to those for model-based revision in
propositional logic. However, unlike propositional logic, a DL-Lite KB can have
infinitely many models, which makes it hard to define and compute revision in
terms of models. For this reason, we first develop an alternative semantic charac-
terization for DL-Lite by introducing the concept of a feature and then define a
specific revision operator for DL-Lite KBs based on features (instead of models).
In contrast to previous approaches, we tackle the problem of revision between
KBs, and the result of revision is always an unique DL-Lite KB. We also present
an algorithm for computing KB revisions in DL-Lite.
1 Introduction
An ontology is a formal description of a common vocabulary for a domain of interest
and the relationships between terms built from the vocabulary. Ontologies have been ap-
plied in a wide range of practical domains such as medical informatics, bio-informatics
and, more recently, the Semantic Web. Description Logics (DLs) have been used as
underlying formalisms of most ontology languages recently. A DL-based ontology is
usually expressed as a DL-knowledge base (KB), which consists of a TBox (termino-
logical box) and an ABox (set of assertions).
DL-Lite [1, 3] is specifically designed as a family of lightweight DLs with rela-
tively restricted expressive power but efficient ontological reasoning algorithms. In par-
ticular, logics in the DL-Lite family have polynomial time computational complexity
with respect to standard reasoning tasks, and LogSpace data complexity with respect
to complex query answering. With reasonable expressive power and efficient reason-
ing support, especially on answering complex queries over large amounts of data, the
DL-Lite family has proved to be an appealing formalism for ontology development.
A challenge in ontology maintenance is that ontologies are not static but may evolve
over time. Because of limitations in the initial design, changes in users’ requirements,
need to reflect changes in the real world, and so on, there is a need to revise ontologies
in accordance with the new knowledge. Recently, intensive interest has been shown on
revision/update in DLs. Earlier approaches concentrated on adapting revision postu-
lates for propositional logic to DLs but no specific revision operators were provided,
e.g. [4, 5]. Recently, there have been several attempts to define specific revision/update
operators for DLs including [7, 9, 11–16]. In particular, an update operator for DL-Lite
ABoxes is defined in [7]. In fact, most specific revision/update operators for DLs can
deal only with ABoxes, like [7, 9, 11], or only with TBoxes, like [13, 14]. As shown in
[8, 14, 16], the kernel revision operator for propositional logic can be adapted to most
DLs in a straightforward way, but the result of revision is not an unique KB in most
cases and thus arbitrary choices by the user are required.
It is worth mentioning that update is traditionally distinguished from revision in
that update addresses changes of the actual state of the world (e.g., that resulting from
an action) whereas revision addresses the incorporation of new knowledge about the
world. In this paper, we focus on the revision problem.
In propositional logic, the area of belief revision [6] is well developed, with nu-
merous proposals and techniques for knowledge base revision. Among them, Satoh’s
revision operator ϕ ∗s µ [17] is well known. In his approach, the set of models of a re-
vised knowledge base K 0 are those models of K 0 that are ‘closest’ to those of the initial
knowledge base K, where the distance between two models is based on their symmetric
difference.
However, such model-based approaches cannot be applied directly to KB revision
in DLs. The difficulties in defining and computing model-based revision of KBs in DLs
are that: (1) unlike a propositional theory, a KB in a DL may have infinitely many
models; (2) a model of a KB can be infinite; and (3) given a collection M of models,
there may not exist an unique KB K such that M is exactly the set of all models of K.
In this paper, we aim to define a rational revision operator for DL-Litebool ontologies
in a way analogous to the model-based approaches in propositional logic. In order to
achieve this goal, we first define the concept of features for DL-Litebool , which precisely
capture most important semantic properties of DL-Litebool KBs, and are always finite.
We adapt the techniques of model-based revision in propositional logic to the revision of
DL-Litebool KBs, and define a specific revision operator based on the distance between
features. We also show that the revision operator possesses desirable properties, and can
be computed through syntactic methods.
Although our approach is based on DL-Litebool [1], we remark that the belief revi-
sion method we propose also applies to other logics in DL-Lite. In contrast to previous
approaches, we address the problem of defining and computing revision of a DL-Lite
KB by another KB. Also, the result of our revision is always an unique KB in DL-Lite.
Due to space limitation, proofs are omitted in this paper but a longer version of
this paper with complete proofs can be found at http://www.cit.gu.edu.au/
˜kewen/revision_long.pdf.
2 DL-Lite Family
A signature is a finite set S = SC ∪ SR ∪ SO ∪ SN where SC is the set of atomic
concepts, SR is the set of atomic roles, SO is the set of individual names (or, objects)
and SN is the set of natural numbers in S. We assume 1 is always in SN . > and ⊥ will
not be considered as atomic concepts or atomic roles. Formally, given a signature S, a
DL-Litebool language L has the following syntax:
R ←− P | P −
B ←− > | ⊥ | A | ≥ n R
C ←− B | ¬C | C1 u C2
where n ≥ 1, A ∈ SC and P ∈ SR . B is called a basic concept and C is called
a general concept. We write ∃R as a shorthand for ≥ 1 R, and let R+ = P , where
P ∈ SR , whenever R = P or R = P − .
A literal is a basic concept or its negation. The set of all literals on S is denoted as
Lit S , and the set of all basic concepts is denoted as Lit +
S.
A DL-Litebool TBox T is a finite set of concept inclusions of the form C1 v C2 ,
where C1 and C2 are general concepts. A DL-Litebool ABox A is a finite set of mem-
bership assertions of the form C(a), R(a, b), where a, b are individual names. We call
C(a) a concept assertion and R(a, b) a role assertion. A DL-Litebool knowledge base
(KB) is a pair K = hT , Ai.
The semantics of a DL-Lite KB is given by interpretations. An interpretation I is a
pair (∆I , ·I ), where ∆I is a non-empty set called the domain and ·I is an interpretation
function which associates each atomic concept A with a subset AI of ∆I , each atomic
role P with a binary relation P I ⊆ ∆I × ∆I , and each individual name a with an
element aI of ∆I such that aI 6= bI for each pair of individual names a, b (unique
name assumption).
The interpretation function ·I can be extended to general concept descriptions:
(P − )I = {(aI , bI ) | (bI , aI ) ∈ P I }
(≥ n R)I = {aI | |{bI | (aI , bI ) ∈ RI }| ≥ n}
(¬C)I = ∆I \ C I
(C1 u C2 )I = C1I ∩ C2I
An interpretation I is a model of inclusion C1 v C2 if C1I ⊆ C2I ; I is a model of
an assertion C(a) if aI ∈ C I ; I is a model of an assertion R(a, b)) if (aI , bI ) ∈ RI ).
I is a model of a TBox T (or ABox A) if I is a model of each inclusion in T (resp.,
each assertion in A). Two inclusions (or resp., assertions, TBoxes, ABoxes) are said to
be equivalent if they have exactly the same models.
I is a model of a KB hT , Ai, if I is a model of both T and A. A KB K is consistent
if it has at least one model. Two KBs K1 , K2 that have the same models are said to be
equivalent, denoted K1 ≡ K2 . A KB K logically implies an inclusion or assertion α,
denoted K |= α, if all models of K are also models of α. We will use Mod(K) to denote
the set of models of a KB K. Sig(K) is the signature of K.
As in propositional logic, a DL-Litebool concept C can always be transformed into
an equivalent disjunction of conjunctions of literal concepts (DNF).
3 Features in DL-Litebool
In this section, we introduce the concept of features in DL-Litebool , which provides an
alternative semantic characterization for DL-Litebool . An advantage of semantic fea-
tures over models is that the number of all features for a DL-Litebool knowledge base
is finite and each feature is finite as we will see later. These finiteness properties make
it possible to recast key approaches to revision for classical propositional logic into
DL-Litebool .
Features for DL-Litebool are based on the notion of types defined in [10].
In the following sections, we assume S is a fixed signature. Recall that a S-literal
(or, literal) is a basic concept on S or its negation. Lit S is the set of all S-literals.
A S-type is a subset τ of Lit S containing > and satisfying the following conditions:
– for every S-literal L, L ∈ τ iff ¬L 6∈ τ ;
– for any m, n ∈ SN with m < n, ≥ n R ∈ τ implies ≥ m R ∈ τ ;
– for any m, n ∈ SN with m < n, ¬(≥ m R) ∈ τ implies ¬(≥ n R) ∈ τ .
A type τ can be equivalently represented by the conjunction of all literals in τ , which
we also call a type when the context is clear and no confusion is caused. An important
observation is that every general concept C over S corresponds to a set Ts(C) of S-
types, in light of the fact that C can be transformed into an equivalent disjunction of
S-types. For example, concept A u (B t ∃ P ) can be transformed into (A u B u ∃ P ) t
(A u ¬B u ∃ P ) t (A u B u ¬∃ P ).
Informally speaking, types correspond to propositional models whereas Ts(C) cor-
respond to the set of models of formula C. For simplicity, we assume that a type τ
consists of only its basic concepts, following similar common practices for proposi-
tional models. For example, let SC = {A, B}, SR = {P }, and SN = {1, 3}. Then τ =
{ A, ∃P, ≥ 3P, ∃P − } is a type instead of τ = { >, A, ¬B, ∃P, ≥ 3P, ∃P − , ¬(≥
3P − ) }.
We say a type τ satisfies a concept C if τ ∈ Ts(C), and τ satisfies concept inclusion
C1 v C2 if τ ∈ Ts(¬C1 t C2 ). In this way, we define that τ satisfies a TBox T if it
satisfies each inclusion in T .
However, in order to capture the membership relations in a KB, we need to extend
the notion of types and thus define Herbrand sets in DL-Lite.
Definition 1. A S-Herbrand set H is a finite set of assertions of the form B(a) or
P (a, b), where a, b ∈ SO , B ∈ Lit +
S , P ∈ SR , satisfying the following conditions
1. for each a ∈ SO , if B1 (a), . . . , Bk (a) are all the concept assertions about a in H,
then the set {B1 , . . . , Bk } forms an S-type.
2. for each P ∈ SR , if P (a, bi ) (1 ≤ i ≤ n) are all the assertions in H of such form,
then for any m ∈ SN with m ≤ n, (≥ m P )(a) is in H;
3. for each P ∈ SR , if P (bi , a) (1 ≤ i ≤ n) are all the assertions in H of such form,
then for any m ∈ SN with m ≤ n, (≥ m P − )(a) is in H.
Informally, B(a) 6∈ H with B ∈ Lit + S means that ¬B(a) holds in H, and P (a, b) 6∈
H with P ∈ SR means that a, b are not related by P in H. Thus, Herbrand sets are
different from ABoxes by adopting a close world assumption. It is not hard to see that,
conditions 2 and 3 in Definition 1 preserve consistency of a Herbrand set. And condi-
tion 2 in Definition 1 requires that ≥ n P ∈ H implies ≥ m P ∈ H for all m ∈ SN
with m < n. These conditions are introduced mainly for simplifying the definition of
our revision operator in the following section.
For simplicity, we denote the group of all the concept assertions B1 (a), . . . , Bk (a)
about a in H as τ (a), where τ = {B1 , . . . , Bk } is a type. We say τ (a) is in H if Bi (a)
is in H for all 1 ≤ i ≤ k.
Herbrand sets can be used to capture membership relations in a KB. We say a Her-
brand set H satisfies a membership assertion C(a) if τ (a) is in H and τ ∈ Ts(C); and
H satisfies assertion P (a, b) (resp., P − (b, a)) if P (a, b) (resp., P − (b, a)) is in H. H
satisfies an ABox A if H satisfies all the assertions in A.
To provide an alternative characterization for reasoning in a KB, we could use pairs
hτ, Hi, where τ is a type and H is a Herbrand set, to replace standard interpretations,
such that hτ, Hi satisfies KB hT , Ai if τ satisfies T and H satisfies A. To this end, we
want it to guarantee that K is consistent iff there exists some pair hτ, Hi satisfying K.
However, the following example shows that this approach does not work.
Example 1. Let K = h{ ∃P − v ⊥ }, { ∃P (a) }i be a DL-Litebool KB. Obviously, K is
inconsistent and thus has no model. However, let S = {P, a, 1} and τ = {∃P }, then
hτ, {τ (a)}i satisfies K.
The problem with using pairs hτ, Hi as alternative semantic characterization for
DL-Lite is that a single type τ is not sufficient to capture the semantic connection be-
tween the TBox and the ABox of a KB. Our investigation shows that it is plausible to
use a pair of a set of types and a Herbrand set, as an alternative semantic characteriza-
tion for a DL-Litebool KB. Using sets of types as semantic characterizations of DL-Lite
TBoxes is also suggested in [10].
Thus, we introduce the definition of features as follows.
Definition 2. Given a signature S, a feature on S, or simply S-feature, is defined as
a pair F = hΞ, Hi, where Ξ is a non-empty set of S-types and H a S-Herbrand set,
such that the following conditions are satisfied:
1. for each P ∈ SR , ∃P ∈ Ξ iff ∃P − ∈ Ξ;
S S
2. for each a ∈ SO and τ (a) in H, s. t. τ is an S-type, τ ∈ Ξ.
Informally, the first condition in Definition 2 says that ∃P is a satisfiable concept in
F if and only if ∃P − is also a satisfiable concept. And the second condition requires
that the interpretation of the ABox must be in accordance to the TBox.
We use a feature F = hΞ, Hi as an alternative for an interpretation in DL-Litebool :
– F satisfies an inclusion C1 v C2 over S, if Ξ ⊆ Ts(¬C1 t C2 ).
– F satisfies an assertion C(a) over S, if τ (a) is in H and τ ∈ Ts(C).
– F satisfies assertion P (a, b) (resp., P − (b, a)) over S, if P (a, b) is in H.
We say F is a model feature of DL-Litebool KB K if F satisfies each inclusion and each
assertion in K. ΩK denotes the set of all model features of K.
From the definition of features, a model feature is finite and the number of model
features of a KB is also finite.
Example 2. Consider the KB K = hT , Ai, where T = { A v ∃P, B v ∃P, ∃P − v
B, A u B v ⊥, ≥ 2 P − v ⊥ } and A = { A(a), P (a, b) }. It is shown in [2] that K is
a KB having no finite model.
An infinite model I of K is defined as follows: ∆I = {da , db , d1 , d2 , d3 . . .},
a = da and bI = db ; the concept A is interpreted as a singleton {da } and B as
I
{db , d1 , d2 , d3 . . .}; and role P is interpreted as {(da , db ), (db , d1 ), (d1 , d2 ), . . . , (di , di+1 ), . . .}.
Take S = Sig(K) = {A, B, P, 1, 2, a, b}. The (finite) model feature of K that cor-
responds to I is F = hΞ, Hi where the Herbrand set H = { τ1 (a), τ2 (b), P (a, b) }
and Ξ = {τ1 , τ2 } with τ1 = {A, ∃P } and τ2 = {B, ∃P, ∃P − }.
Given an inclusion or assertion α over S = Sig(K), we define K |=f α if for each
F ∈ ΩK , F satisfies α. Given two KBs K1 and K2 , let S = Sig(K1 ∪ K2 ), define
K1 |=f K2 if ΩK1 ⊆ ΩK2 ; and K1 ≡f K2 if ΩK1 = ΩK2 .
The following two results show that model features do capture the semantic proper-
ties of DL-Litebool KBs.
Proposition 1. Let K be a DL-Litebool KB and S = Sig(K). Then
1. K is consistent iff K has a model feature;
2. for any concept inclusion C1 v C2 over S, K |= (C1 v C2 ) iff K |=f (C1 v C2 );
3. for any membership assertion C(a) (resp., R(a, b)) over S, K |= C(a) iff K |=f
C(a) (resp., K |= R(a, b) iff K |=f R(a, b));
Proposition 2. Let K1 , K2 be two DL-Litebool KBs and S = Sig(K1 ∪ K2 ). Then
1. K1 |= K2 iff K1 |=f K2 ;
2. K1 ≡ K2 iff K1 ≡f K2 .
In summary, the advantages of model features over standard models can be de-
scribed as follows. First, each model feature of a KB is finite in structure. Second, there
are a finite number of model features for each KB. Third, each non-empty set of model
features determines a unique KB up to KB equivalence. In particular, given a non-empty
set Ω of S-features, we can always construct an unique DL-Litebool KB K over S such
that Ω ⊆ ΩK and ΩK is minimal among all supersets ΩK0 of Ω. In Section 5, we will
introduce a method for constructing such a DL-Litebool KB from a set of features.
4 Feature-based Revision
In this section, we introduce a specific revision operator for DL-Lite KBs based on
model features rather than models.
Before introducing the definition of our feature-based revision operator, we first ex-
tend the definition of symmetric difference 4 so that it can be used for model features.
Recall that S1 4S2 = (S1 −S2 )∪(S2 −S1 ) for any two sets S1 and S2 . Given two S-
features F1 = hΞ1 , H1 i and F2 = hΞ2 , H2 i, the distance between F1 and F2 , denoted
F1 4F2 , is a pair h Ξ1 4Ξ2 , H1 4H2 i. Note that H1 4H2 may not be a Herbrand set
anymore. For example, let S = {P, a, b1 , b2 , b3 , 1, 2, 3}, H1 = {∃P (a), P (a, b1 )}
and H2 = {∃P (a), (≥ 2 P )(a), P (a, b2 ), P (a, b3 )}. Then we get H1 4H2 = {(≥
2 P )(a), P (a, b1 ), P (a, b2 ), P (a, b3 )}, which is not a Herbrand set because it does
not contain ∃P (a) and (≥ 3 P )(a).
To compare two distances, we could define F1 4F2 ⊆d F3 4F4 if Ξ1 4Ξ2 ⊆d
Ξ3 4Ξ4 and H1 4H2 ⊆d H3 4H4 , where Fi = hΞi , Hi i for i = 1, 2, 3, 4; and
F1 4F2 ⊂d F3 4F4 if F1 4F2 ⊆d F3 4F4 and F3 4F4 6⊆d F1 4F2 . However, we
will show in an example later that such a measure is too weak for KB revision and can-
not preserve enough information. Instead, we set a preference on Herbrand sets over
type sets: F1 4F2 ⊂d F3 4F4 iff
1. H1 4H2 ⊂ H3 4H4 , or
2. H1 4H2 = H3 4H4 and Ξ1 4Ξ2 ⊂ Ξ3 4Ξ4 .
Note that here we set a preference on Herbrand set over type set, such that asser-
tions in the original ABox are prior to be preserved than inclusions in the TBox. The
rationale behind this preference is that assertions represent more specific information
than inclusions and thus from the view point of knowledge representation, should have
higher priority.
According to our new semantic characterization for DL-Litebool KBs, the semantics
of each KB K is determined by the set ΩK of all model features of K.
Given two KBs K and K0 , to define our revision operator K ◦ K0 , we need to specify
the subset of ΩK0 that is closest to ΩK .
Let Ω1 and Ω2 be two sets of features. Then we define
σ(Ω1 , Ω2 ) = { F1 ∈ Ω1 | there exists F2 ∈ Ω2 s.t.
(F10 4F20 ) 6⊂d (F1 4F2 ) for all F10 ∈ Ω1 and F20 ∈ Ω2 }
Now we are ready to define our revision operator in terms of model features.
Definition 3. Let K, K0 be two DL-Litebool KBs and S = Sig(K ∪ K0 ). The (feature-
based) revision of K by K0 is defined as the DL-Litebool KB K ◦ K0 such that if ΩK = ∅,
then ΩK◦K0 = ΩK0 ; otherwise
1. σ(ΩK0 , ΩK ) ⊆ ΩK◦K0 , and
2. ΩK◦K0 is minimal in the sense that, for any DL-Litebool KB K00 satisfying the above
condition 1, ΩK◦K0 ⊆ ΩK00 .
Note that the definition is slightly different from Satoh’s as σ(ΩK0 , ΩK ) may not
correspond exactly to a DL-Litebool KB. By requiring ΩK◦K0 to be the minimal superset
of σ(ΩK0 , ΩK ), we define K ◦ K0 in a conservative manner. Another option is to define
ΩK◦K0 to be a maximal subset of σ(ΩK0 , ΩK ). However, as ΩK◦K0 can be very small
if defined this way, there is a risk that unexpected logical consequences are introduced.
Thus, it is more plausible to use supersets instead of subsets.
For any two DL-Litebool KBs K1 , K2 that are both revisions of K by K0 , we have
ΩK1 = ΩK2 . By Proposition 2, this definition uniquely defines the result of K ◦ K0 up
to equivalence. We will show in Section 5 that K ◦ K0 always exists.
Example 3. Consider a DL-Litebool KB
K = h { PhD v Student, Student v ¬∃teaches }, { PhD(Tom) } i.
The TBox of K specifies that PhD students are students, and students are not allowed
to teach any courses, while the ABox states that Tom is a PhD student. Suppose PhD
students are actually allowed to teach, and we want to revise K with K0 = h { PhD v
∃teaches }, ∅ i.
Then F 0 = h {τ1 }, {τ1 (Tom)} i, where τ1 = {Student} is a model feature of K0 .
Take F = h {τ1 , τ2 }, {τ2 (Tom)} i where τ2 = {PhD, Student}. It can be verified that
F is a model feature of K and it is closest to F 0 .
The distance between F and F 0 is a minimal one among those between model
features of K and K0 . Thus, F 0 is a model feature of K ◦ K0 .
In fact, we can show that K◦K0 is h { PhD v Student, PhD v ∃teaches, Studentu
∃teaches v PhD }, { Student(Tom) } i.
In Example 3, the new inclusion added causes concept PhD to be unsatisfiable,
i. e., PhD must be interpreted as an empty set, and thus contradicts PhD(Tom). The
contradiction is resolved through revision by replacing Student v ¬∃teaches with
Student u ∃teaches v PhD. Also, PhD(Tom) is weaken to be Student(Tom), be-
cause ¬∃teaches(Tom) is also (implicitly) expressed in K. However, if we treat type
sets and Herbrand sets equally in measuring distances, as we can show, Student(Tom)
will be lost from the result of revision.
The standard AGM postulates (R1) – (R6) for propositional belief revision have
been adapted to DLs in [15]. However, the authors present the postulates in terms of
models of KBs. In the following, we reformulate them using KB combinations and
entailments, in a manner analogous to classical AGM postulates.
(R1) K ◦ K0 |= K0 ;
(R2) if K ∪ K0 is consistent, then K ◦ K0 ≡ K ∪ K0 ;
(R3) if K0 is consistent, then K ◦ K0 is consistent;
(R4) if K1 ≡ K2 and K10 ≡ K20 , then K1 ◦ K10 ≡ K2 ◦ K20 ;
(R5) if ΩK◦K0 = σ(ΩK0 , ΩK ), then (K ◦ K0 ) ∪ K00 |= K ◦ (K0 ∪ K00 );
(R6) if (K ◦ K0 ) ∪ K00 is consistent, then K ◦ (K0 ∪ K00 ) |= (K ◦ K0 ) ∪ K00 .
The following theorem states the first five postulates are satisfied by our revision
operator.
Theorem 1. The revision operator defined in Definition 3 satisfies postulates (R1) –
(R5).
Note that (R5) is conditional, and in this sense varies from its corresponding classi-
cal AGM postulate. We remark that the condition in (R5) cannot be removed. That is,
(K ◦K0 )∪K00 |= K ◦(K0 ∪K00 ) is not always satisfied. Also, (R6) is not always satisfied
by our revision operator, as with Satoh’s revision operator in propositional logic. This
can be seen from the following example.
Example 4. Let K = h { A v B, B v C }, { A(a) } i, K0 = h { B v A, A v
¬C }, { (A t C)(a) } i, and K00 = h ∅, { ¬B(a) } i. Then K ◦ K0 = h { A v B, B v
A, A v ¬C }, { (AtC)(a) } i, and after combined with K00 , (AtC)(a) in the ABox is
replaced with C(a). However, K◦(K0 ∪K00 ) = h { B v C, B v A, A v ¬C }, { (At
C)(a) } i. That is, (K ◦ K0 ) ∪ K00 6|= K ◦ (K0 ∪ K00 ) and K ◦ (K0 ∪ K00 ) 6|= (K ◦ K0 ) ∪ K00 .
5 Algorithm for Computing Revision
In this section, we investigate the problem of computing revision and as a result, present
an algorithm that can compute the result of revision syntactically.
The revision operator is based on model features of KBs. In what follows, we in-
troduce a method for computing all the model features of a DL-Litebool KB K, by first
computing the assembling of all the model features, which can be obtained directly
from K through syntactic transformations.
Given two features F1 = hΞ1 , H1 i and F2 = hΞ2 , H2 i, we define the assembling
of F1 and F2 as F1 ⊕ F2 = h Ξ1 ∪ Ξ2 , H1 ⊕ H2 i, where H1 ⊕ H2 is called a multiple
Herbrand set, consisting of:
– {τ1 , τ2 }(a), for each a ∈ SO , τ1 (a) ∈ H1 and τ2 (a) ∈ H2 ; and
– P (a, b), for a, b ∈ SO , P (a, b) ∈ H1 and P (a, b) ∈ H2 .
In a multiple Herbrand set, {τ1 , τ2 } can be viewed as a disjunction of types τ1 and
τ2 . Since role disjunction is not allowed in DL-Litebool , we only need to consider those
role assertions appearing in both H1 andL H2 .
Given a DL-Litebool KB K, we use ΩK = hΞK , MK i to denote the assembling
of all the model features of K, where ΞK is a type set and MK a multiple Herbrand set.
For simplicity, given {τ1 , . . . , τn }(a) in a multiple Herbrand set M, we also represent
it as Ξ(a) with Ξ = {τ1 , . . . , τn }.
Example 5. Recall the KB K in Example 2. ΞK consists of nine types: { ∅, τ1 , τ2 , {A, ∃P, ≥
2 P }, {B, ∃P }, {B, ∃P, ≥ 2 P, (∃P − )}, {∃P, (≥ 2 P )} }, where a type containing a
basic concept in brackets, e.g., (∃P − ), represents two types, one containing ∃P − and
the other not. The multiple Herbrand set MK consists of { τ1 , {A, ∃P, ≥ 2 P } }(a),
{ τ2 , {B, ∃P, ≥ 2 P, ∃P − } }(b), and P (a, b).
To compute the model features of a KB K, a naive methodLis to check for each S-
feature F whether F satisfies K. However, we can show that ΩK can be computed
directly
L from K through syntactic transformations, and ΩK can be easily obtained from
ΩK . L
Now we show how to compute ΩK for a DL-Litebool KB K through syntactic
method (ref. Figure 1).
Note that 2 and 3 of Step 3 ensure that M is a multiple Herbrand set, and thus,
together with Step 2, ensure hΞ, Mi is an assembling of features.
L
Theorem 2. Given a consistent DL-Litebool KB K, Algorithm 1 always returns ΩK .
L following result shows that all the model features of K can be easily obtained
The
from ΩK .
L
Proposition 3. Given a DL-Litebool KB K, if ΩK = hΞK , MK i, then for any feature
F = hΞ, Hi, F is a model feature of K iff the following conditions are satisfied:
1. Ξ ⊆ ΞK ;
2. τa ∈ Ξa , for each a ∈ SO , τa (a) ∈ H and Ξa (a) ∈ MK ; and
Algorithm 1 (Compute the assembling of all the model features of a DL-Litebool KB)
Input: AL DL-Litebool KB K = hT , Ai and a signature S.
Output: ΩK .
Method: T
Step 1. Compute S-type set Ξ = (C1 vC2 )∈T Ts(¬C1 t C2 ).
Step 2. Eliminate from Ξ all the types τ such that ∃R ∈ τ for some R but ∃R− 6∈ Ξ.
S
Step 3. Initially, take M = { P (a, b) | P (a, b) or P − (b, a) ∈ A }. Then, for each a ∈ SO ,
perform the following procedure:
T
1. add >(a) into A, and compute Ξa = C(a)∈A Ts(C) ∩ Ξ;
2. for each P ∈ SR , if n is the number of P -successors of a in M and m the largest number
in SN with m ≤ n, then eliminate from Ξa all the types not containing ≥ m P ;
3. for each P ∈ SR , if n is the number of P -predecessors of a in M and m the largest number
in SN with m ≤ n, then eliminate from Ξa all the types not containing ≥ m P − ;
4. add Ξa (a) into M.
L
Step 4. Return hΞ, Mi as ΩK .
Fig. 1. Compute assembling of model features.
3. P (a, b) ∈ H, for each P (a, b) ∈ MK .
From Proposition 3, ΩK is the set consisting of all the features satisfying 1 – 3 of
Proposition 3.
Given ΩK and ΩK0 , we can select those features in ΩK0 that are closet to ΩK , i. e.,
σ(ΩK0 , ΩK ), through the definition. To provide a complete algorithm for our revision
operator, we only need a method to construct K ◦ K0 from σ(ΩK0 , ΩK ).
Each KB uniquely determines an assembling of features, that is, the assembling of
all its model features. The converse is also true, as shown in the following proposition.
Proposition 4. Given a set Ω of features, there always exists a DL-Litebool KB K such
that
L L
1. ΩK = Ω;
2. Ω ⊆ ΩK ; and for any DL-Litebool KB K0 with Ω ⊆ ΩK0 , ΩK ⊆ ΩK0 .
suggests that, K ◦ K0 can be constructed from
L
The above proposition
L ΩK◦K0 .
Also, to compute ΩK◦K0 , we can avoid computing L all the features
L in ΩK◦K 0 , but
obtain it directly from σ(ΩK0 , ΩK ). Indeed, we have ΩK◦K0 = σ(ΩK0 , ΩK ).
Finally, we present an algorithm for DL-Litebool KB revision in Figure 2, which
follows from the definition.
Theorem 3. Given two consistent DL-Litebool KBs K and K0 , Algorithm 2 always re-
turns K ◦ K0 .
The problem of computing the revision is decidable although it may be exponential
in the worst case.
Algorithm 2 (Compute the result of revising a DL-Litebool KB)
Input: Two DL-Litebool KBs K and K0 , S = Sig(K ∪ K0 ).
Output: K ◦ K0 .
Method: L L
Step 1. Use Algorithm 1 to compute ΩK and ΩK0 .
Step 2. Compute ΩK and ΩK0 through Proposition
L 3. L L
Step 3. Obtain σ(ΩK0 , ΩK ) and compute ΩK◦K0 = σ(ΩK0 , ΩK ). Suppose ΩK◦K0 =
hΞ, Mi.
Step 4. Construct from hΞ, Mi the DL-Litebool KB hT , Ai with
l l
T ={ Bu ¬B v ⊥ | B ∈ Lit + S ; τ is an S-type s.t. τ 6∈ Ξ },
B∈τ B6∈τ
and
G l l
A = {( ( Bu ¬B))(a) | a ∈ SO , Ξa (a) ∈ M } ∪ { P (a, b) ∈ M }.
τ ∈Ξa (a) B∈τ B6∈τ
Step 5. Return hT , Ai as K ◦ K0 .
Fig. 2. Compute revision.
6 Conclusion
Approaches on adapting classical model-based revision to DLs have proposed in [13,
15]. In [15], the author discuss a special case in KB revision, that is, when inconsistency
is caused by ABox assertions. The distances between two models are defined through
the number of individuals whose membership differ in the two models. A TBox revi-
sion operator that can handle incoherence is introduced in [13], in which the distance
between two models are defined through the number of atomic concepts they disagree.
In both of these two approaches, the results of revision are not single KBs, but dis-
junctive KBs. Also, when applying to Example 3 (with only the TBox revised in the
second approach), neither of these two approaches has Student(Tom) as a logical con-
sequence of the revision. Same problem also occurs in those kernel revision operators
with disjunctive KBs as the results of revision.
We have developed a formal framework for revising general KBs (with no specific
restriction) in DL-Litebool , based on the notion of features. We have defined a specific
revision operator, which is a natural adaptation of revision approaches from proposi-
tional logic. We have also developed algorithms for computing KB revisions in DL-
Litebool , and the result of our revision is always an unique DL-Litebool KB. We note
that other propositional revision operators, e. g., Dalal’s revision, belief contraction and
update can also be easily adopted in our framework.
There are still several problems remaining for future work. One is to extend our ap-
proach to KB revision in other DLs. The major difficulty here is that a general concept
in most expressive DLs cannot be transformed into an equivalent disjunction of con-
junctions of literal concepts. Another problem is to look at applications of our revision
operator in nonmonotonic reasoning problems in DLs.
References
1. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. DL-Lite in the light of first-
order logic. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence
(AAAI07), pages 361–366, 2007.
2. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Data complexity of
query answering in description logics. In Proceedings of the 10th International Conference
on Principles of Knowledge Representation and Reasoning (KR-06), pages 260–270, 2006.
3. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Tractable reasoning
and efficient query answering in description logics: The DL-Lite family. J. Autom. Reason-
ing, 39(3):385–429, 2007.
4. G. Flouris, Z. Huang, J. Z. Pan, D. Plexousakis, and H. Wache. Inconsistencies, negations
and changes in ontologies. In Proceedings of the 21st National Conference on Artificial
Intelligence (AAAI-06), 2006.
5. G. Flouris, D. Plexousakis, and G. Antoniou. On applying the AGM theory to dls and OWL.
In Proceedings of the International Semantic Web Conference, pages 216–231, 2005.
6. P. Gärdenfors, editor. Belief Revision. Cambridge University Press, 1992.
7. G. De Giacomo, M. Lenzerini, A. Poggi, and R. Rosati. On the approximation of instance
level update and erasure in description logics. In Proceedings of the 22th National Confer-
ence on Artificial Intelligence (AAAI-07), pages 403–408, 2007.
8. C. Halaschek-Wiener, Y. Katz, and B. Parsia. Belief base revision for expressive description
logics. In Proceedings of Workshop on OWL Experiences and Directions, 2006.
9. C. Halaschek-Wiener, B. Parsia, E. Sirin, and A. Kalyanpur. Description logic reasoning for
dynamic ABoxes. In Proceedings of the 2006 International Workshop on Description Logics
(DL2006), 2006.
10. R. Kontchakov, F. Wolter, and M. Zakharyaschev. Can you tell the difference between
DL-Lite ontologies? In Proceedings of the 11th International Conference on Principles
of Knowledge Representation and Reasoning (KR08), pages 285–295. AAAI Press, 2008.
11. H. Liu, C. Lutz, M. Milicic, and F. Wolter. Updating description logic ABoxes. In Proceed-
ings of the 10th International Conference on Principles of Knowledge Representation and
Reasoning (KR-06), pages 46–56, 2006.
12. T. Meyer, K. Lee, and R. Booth. Knowledge integration for description logics. In Proceed-
ings of The 20th National Conference on Artificial Intelligence (AAAI05), pages 645–650,
2005.
13. G. Qi and J. Du. Model-based revision operators for terminologies in description logics. In
Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI-09),
to appear.
14. G. Qi, P. Haase, Z. Huang, Q. Ji, J. Z. Pan, and J. Völker. A kernel revision operator for
terminologies - algorithms and evaluation. In Proceedings of the 7th International Semantic
Web Conference (ISWC08), pages 419–434, 2008.
15. G. Qi, W. Liu, and D. A. Bell. Knowledge base revision in description logics. In Proceedings
of 10th European Conference on Logics in Artificial Intelligence (JELIA06), 2006.
16. M. Ribeiro and R. Wassermann. Base revision in description logics - preliminary results. In
Proceedings of International Workshop on Ontology Dynamics (IWOD07), 2007.
17. K. Satoh. Nonmonotonic reasoning by minimal belief revision. In Institute for New Gener-
ation Computer Technology (ICOT), editor, Proceedings of the International Conference on
Fifth Generation Computer Systems, pages 455–462. Springer-Verlag, 1988.