We address the revision problem for knowledge bases (KBs) in Description Logics (DLs). This problem has received much attention in the ontology management and DL communities, but the existing proposals are restricted in several 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 characterization 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.
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 applied 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 (terminological box) and an ABox (set of assertions).
DL-Lite [
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
postulates for propositional logic to DLs but no specific revision operators were provided,
e.g. [
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 [
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 [
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
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
R B C
P j P > j ? j A j n R
B j :C j C1 u C2 where n 1, A 2 SC and P 2 SR. B is called a basic concept and C is called a general concept. We write 9R as a shorthand for 1 R, and let R+ = P , where P 2 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 membership 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 = f(aI ; bI ) j (bI ; aI ) 2 P I g ( n R)I = faI j jfbI j (aI ; bI ) 2 RI gj
(:C)I = I n CI (C1 u C2)I = C1I \ C2I ng
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 2 CI ; I is a model of an assertion R(a; b)) if (aI ; bI ) 2 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 j= , 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
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 features 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 [
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 2 iff :L 62 ; – for any m; n 2 SN with m < n, n R 2 implies m R 2 ; – for any m; n 2 SN with m < n, :( m R) 2 implies :( n R) 2 .
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 Stypes, in light of the fact that C can be transformed into an equivalent disjunction of S-types. For example, concept A u (B t 9 P ) can be transformed into (A u B u 9 P ) t (A u :B u 9 P ) t (A u B u :9 P ).
Informally speaking, types correspond to propositional models whereas Ts(C) correspond 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 propositional models. For example, let SC = fA; Bg, SR = fP g, and SN = f1; 3g. Then = f A; 9P; 3P; 9P g is a type instead of = f >; A; :B; 9P; 3P; 9P ; :( 3P ) g.
We say a type satisfies a concept C if 2 Ts(C), and satisfies concept inclusion C1 v C2 if 2 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 2 SO, B 2 Lit +, P 2 SR, satisfying the following conditions
S 1. for each a 2 SO, if B1(a); : : : ; Bk(a) are all the concept assertions about a in H, then the set fB1; : : : ; Bkg forms an S-type. 2. for each P 2 SR, if P (a; bi) (1 i n) are all the assertions in H of such form, then for any m 2 SN with m n, ( m P )(a) is in H; 3. for each P 2 SR, if P (bi; a) (1 i n) are all the assertions in H of such form, then for any m 2 SN with m n, ( m P )(a) is in H.
Informally, B(a) 62 H with B 2 Lit S+ means that :B(a) holds in H, and P (a; b) 62 H with P 2 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 condition 2 in Definition 1 requires that n P 2 H implies m P 2 H for all m 2 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 = fB1; : : : ; Bkg 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 Herbrand set H satisfies a membership assertion C(a) if (a) is in H and 2 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 = hf 9P v ? g; f 9P (a) gi be a DL-Litebool KB. Obviously, K is inconsistent and thus has no model. However, let S = fP; a; 1g and = f9P g, then h ; f (a)gi 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
between 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
characterization for a DL-Litebool KB. Using sets of types as semantic characterizations of DL-Lite
TBoxes is also suggested in [
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 2 SR, 9P 2 S iff 9P 2 S ; 2. for each a 2 SO and (a) in H, s. t. is an S-type,
Informally, the first condition in Definition 2 says that 9P is a satisfiable concept in F if and only if 9P 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 2 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 = f A v 9P; B v 9P; 9P v
B; A u B v ?; 2 P v ? g and A = f A(a); P (a; b) g. It is shown in [
An infinite model I of K is defined as follows: I = fda; db; d1; d2; d3 : : :g, aI = da and bI = db; the concept A is interpreted as a singleton fdag and B as fdb; d1; d2; d3 : : :g; and role P is interpreted as f(da; db); (db; d1); (d1; d2); : : : ; (di; di+1); : : :g.
Take S = Sig(K) = fA; B; P; 1; 2; a; bg. The (finite) model feature of K that corresponds to I is F = h ; Hi where the Herbrand set H = f 1(a); 2(b); P (a; b) g and = f 1; 2g with 1 = fA; 9P g and 2 = fB; 9P; 9P g.
Given an inclusion or assertion over S = Sig(K), we define K j=f if for each F 2 K, F satisfies . Given two KBs K1 and K2, let S = Sig(K1 [ K2), define K1 j=f K2 if K1 K2 ; and K1 f K2 if K1 = K2 .
The following two results show that model features do capture the semantic properties 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 j= (C1 v C2) iff K j=f (C1 v C2); 3. for any membership assertion C(a) (resp., R(a; b)) over S, K j= C(a) iff K j=f
C(a) (resp., K j= R(a; b) iff K j=f R(a; b)); Proposition 2. Let K1; K2 be two DL-Litebool KBs and S = Sig(K1 [ K2). Then 1. K1 j= K2 iff K1 j=f K2; 2. K1 K2 iff K1 f K2.
In summary, the advantages of model features over standard models can be described 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
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 extend the definition of symmetric difference 4 so that it can be used for model features.
Recall that S14S2 = (S1 S2)[(S2 S1) for any two sets S1 and S2. Given two Sfeatures F1 = h 1; H1i and F2 = h 2; H2i, the distance between F1 and F2, denoted F14F2, is a pair h 14 2; H14H2 i. Note that H14H2 may not be a Herbrand set anymore. For example, let S = fP; a; b1; b2; b3; 1; 2; 3g, H1 = f9P (a); P (a; b1)g and H2 = f9P (a); ( 2 P )(a); P (a; b2); P (a; b3)g. Then we get H14H2 = f( 2 P )(a); P (a; b1); P (a; b2); P (a; b3)g, which is not a Herbrand set because it does not contain 9P (a) and ( 3 P )(a).
To compare two distances, we could define F14F2 d F34F4 if 14 2 d 34 4 and H14H2 d H34H4, where Fi = h i; Hii for i = 1; 2; 3; 4; and F14F2 d F34F4 if F14F2 d F34F4 and F34F4 6 d F14F2. However, we will show in an example later that such a measure is too weak for KB revision and cannot preserve enough information. Instead, we set a preference on Herbrand sets over type sets: F14F2 d F34F4 iff 1. H14H2 H34H4, or 2. H14H2 = H34H4 and Now we are ready to define our revision operator in terms of model features.
K K0
K00 .
Definition 3. Let K; K0 be two DL-Litebool KBs and S = Sig(K [ K0). The (featurebased) revision of K by K0 is defined as the DL-Litebool KB K K0 such that if K = ;, then K K0 = K0 ; otherwise
K0 ; K) K K0 , and
K K0 is minimal in the sense that, for any DL-Litebool KB K00 satisfying the above condition 1,
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.
K = h f PhD v Student ; Student v :9teaches g; f PhD (Tom) g 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 f PhD v 9teaches g; ; i.
Then F 0 = h f 1g; f 1(Tom)g i, where 1 = fStudent g is a model feature of K0. Take F = h f 1; 2g; f 2(Tom)g i where 2 = fPhD ; Student g. 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 f PhD v Student ; PhD v 9teaches; Student u 9teaches v PhD g; f Student (Tom) g 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 :9teaches with Student u 9teaches v PhD . Also, PhD (Tom) is weaken to be Student (Tom), because :9teaches(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 [
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 classical AGM postulate. We remark that the condition in (R5) cannot be removed. That is, (K K0) [ K00 j= 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 f A v B; B v C g; f A(a) g i, K0 = h f B v A; A v :C g; f (A t C)(a) g i, and K00 = h ;; f :B(a) g i. Then K K0 = h f A v B; B v A; A v :C g; f (AtC)(a) g i, and after combined with K00, (AtC)(a) in the ABox is replaced with C(a). However, K (K0 [K00) = h f B v C; B v A; A v :C g; f (At C)(a) g i. That is, (K K0) [ K00 6j= K (K0 [ K00) and K (K0 [ K00) 6j= (K K0) [ K00.
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 introduce 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; H1i and F2 = h 2; H2i, 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: – f 1; 2g(a), for each a 2 SO, 1(a) 2 H1 and 2(a) 2 H2; and – P (a; b), for a; b 2 SO, P (a; b) 2 H1 and P (a; b) 2 H2.
In a multiple Herbrand set, f 1; 2g 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 and H2.
Given a DL-Litebool KB K, we use L K = h K; MKi 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 f 1; : : : ; ng(a) in a multiple Herbrand set M, we also represent it as (a) with = f 1; : : : ; ng.
Example 5. Recall the KB K in Example 2. K consists of nine types: f ;; 1; 2; fA; 9P; 2 P g; fB; 9P g; fB; 9P; 2 P; (9P )g; f9P; ( 2 P )g g, where a type containing a basic concept in brackets, e.g., (9P ), represents two types, one containing 9P and the other not. The multiple Herbrand set MK consists of f 1; fA; 9P; 2 P g g(a), f 2; fB; 9P; 2 P; 9P g g(b), and P (a; b).
To compute the model features of a KB K, a naive method is to check for each Sfeature F whether F satisfies K. However, we can show that L K can be computed directly from K through syntactic transformations, and K can be easily obtained from L K.
Now we show how to compute L 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.
Theorem 2. Given a consistent DL-Litebool KB K, Algorithm 1 always returns L
The following result shows that all the model features of K can be easily obtained from L K.
Proposition 3. Given a DL-Litebool KB K, if L K = h K; MKi, then for any feature F = h ; Hi, F is a model feature of K iff the following conditions are satisfied: 1. add >(a) into A, and compute a = TC(a)2A Ts(C) \ ; 2. for each P 2 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 2 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.
3. P (a; b) 2 H, for each P (a; b) 2 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 that
of features, there always exists a DL-Litebool KB K such 1. L 2.
K = L ;
K; and for any DL-Litebool KB K0 with K0 ,
K
K0 .
AlsoT,hteo acboomvepuptreoLpositiKonKs0 u,gwgeesctasnthaavto,iKd coKm0puctainngbealclotnhsetrfuecatteudrefsroinm LK KK0, bKu0t. obtain it directly from ( K0 ; K). Indeed, we have L K K0 = L ( 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 returns 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).
Method: Step 1. Use Algorithm 1 to compute L K and L K0 .
Step 2. Compute K and K0 through Proposition 3.
Step 3. Obtain ( K0 ; K) and compute L K K0 = L ( K0 ; K). Suppose L h ; Mi.
Step 4. Construct from h ; Mi the DL-Litebool KB hT ; Ai with
T = f l B u l :B v ? j B 2 Lit S+; is an S-type s.t. 62
B2 B62 g; and K K0 =
Approaches on adapting classical model-based revision to DLs have proposed in [
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 propositional logic. We have also developed algorithms for computing KB revisions in DLLitebool , 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 approach 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 conjunctions of literal concepts. Another problem is to look at applications of our revision operator in nonmonotonic reasoning problems in DLs.