In this paper, we propose a service for contracting axioms from ontologies based on the description logic EL. In particular, we devise algorithms that implement the contraction operation of the AGM theory on belief change. We rst generalise the AGM contraction postulates to description logics, in which a variant of the recovery postulate is de ned by using the notion of logical di erence. Plausibility of the contraction operation is demonstrated by showing that it satis es all the generalised postulates.
Introduction 1 The AGM also introduces the expansion operation but it can be considered a special case of revision. satisfy the recovery postulate of the AGM framework. As this postulate speci es the minimal change property of the contraction operation, these operators can not be justi ed against this property. In this work we address the problem by generalising the AGM contraction postulates so that their satisfaction no longer relies on the expressiveness of the underlying logic. The main idea is to re ne the recovery postulate by using the notion of logical di erence.
Intuitively, candidate outputs of a contraction operator should at least be logically weaker than the original terminology and not imply the axiom being contracted. These intuitions are captured by the so-called inclusion (K . 2) and success (K . 4) postulates in the AGM framework. Furthermore, among the candidates for retention, the most desirable ones should have the least logical di erence from the original terminology compared to the others. In Section 4, we show that for classical logic, contraction satis es the recovery postulate if and only if it has the above property. 2
Let NC and NR be disjoint sets of concept names and role names, respectively. In the description logic E L, concepts C are built according to the rule
C ::= >jAjC u Dj9R:C where A ranges over NC, R ranges over NR, and C; D range over concepts. The semantics of E L is the standard set theoretic Tarskian semantics. An interpretations is a structure I = ( I ; I ), where I is a non-empty set called the domain, and I is an interpretation function mapping concept names A to a subset AI of I and role name R to binary relations RI over I I . The function I is extended to arbitrary concepts as follows:
>I := I (C u D)I := CI \ DI (9R:C)I := fx 2
I j9y 2
I : (x; y) 2 RI ^ y 2 CI g
for short); C D is an abbreviation for C v D and D v C. An E L terminology (or TBox for short) is a nite set of GCIs. An interpretation I satis es an axiom C v D (I j= C v D) i CI DI ; I j= C D i CI = DI . I is a model of a TBox T (I j= T ) if it satis es every axiom in T . An axiom C v D is a consequence of a TBox T (T j= C v D) i every model of T satis es C v D. Given a Tarskian consequence operator Cn, and a TBox T , Cn(T ) = fC v D j T j= C v Dg.
In this paper we assume that a TBox contains only axioms of the form A C
and A v C, where A is a concept name and no concept name occurs more than
once on the left-hand side of an axiom. A concept name is primitive if it does not
occur on the left-hand side of an axiom and is pseudo-primitive if it is primitive
or occurs on the left-hand side of an axiom of the form A v C. Under these
assumptions a useful property regarding E L TBoxes (Lemma 1) is derived in [
Lemma 1 provides a description of the syntactic form of concepts C such that T j= C v A, where A is pseudo-primitive or of the form 9R:B, from which we can obtain justi cations of T entailing C v A. Suppose T j= C v A for A pseudo-primitive, according to Part 1 of the lemma, if C is of the form B u 9R:C then it must be the case T j= B v A (which implies B u 9R:C v A in T ). Similarly if T j= 9S:B u 9R:D v 9R:C then according to Part 2 of the lemma, it must be the case T j= D v C (which implies 9S:B u 9R:D v 9R:C in T ). 3
Logical Di erence Between Terminologies
The notion of logical di erence between DL terminologies was proposed by
Konev et al. [
C v D 2 Di (T; T 0 ) i 1. T j= C v D
0 = C v D 2. T 6j 3. if T j 0 0 0 0 0 = A v B and there is no A v B0 s.t. T 0 j= A v B0 and fA v B g j= A v B then fC v Dg 6j= A v B
Our de nition of logical di erence di ers from Konev's (which does not enforce condition 3) in the sense that ours is more strict. It turns out that our de nition is more appropriate for the purpose of formalising properties of rational belief change. For example, let T = fA0 v B u Cg and T 0 = fA v Cg be TBoxes, under Konev's de nition Di (T; T ) = fA v B u C; A v Bg whereas under ours Di (T; T 0 ) = fA v Bg. We will use the notion of logical di erence to specify how minimal are the changes that have been made to a TBox to accomplish a contraction. In other words, we want to identify the TBoxes that di er the least from the original one. Let T; T 0 and T 00 be TBoxes, it is natural to conclude that T 0 di ers less from T than T 00 does if Di (T; T 0 ) is logically weaker than Di (T; T 00 ), that is Di (T; T 00 ) j= Di (T; T 0 ). Continuing with the above example, let T 00 be empty, intuitively T 0 di ers less from T then T 00 does. However, under Konev's de nition Di (T; T 0 ) Di (T; T 00 )
Lemma 2 states that if T 0 does not entail C v D then it does not entail A v 9R:B
or B v A. From the proof of Lemma 2 in [
Generalising AGM
Belief Contraction A common approach in addressing belief change is to provide a set of rationality postulates for belief change operations. The AGM approach provides the best known set of postulates. The aim is to describe belief change at the knowledge level without referring to any representational formalism. In the AGM approach belief states are modelled by belief sets closed under the Tarskian consequence operator(Cn) for a logic including propositional logic in a language L. The expansion of a belief set K by ', K + ', is de ned as Cn(K [ f'g). Contraction represents situations in which an agent has to give up some information from its current beliefs. Formally, a contraction operation is a function from 2L L to 2L satisfying the following set of basic postulates. The contraction of a belief set by a sentence yields a new set, called the contracted belief set. (K . 1) K . ' = Cn(K . '). (Closure) (K . 2) K . ' K (Inclusion) (K . 3) If ' 62 K, then K . ' = K. (V acuity) (K . 4) If 6j= ', then ' 62 K . A (Success) (K . 5) If j= ' , then K . ' K . (Extensionality) (K . 6) K (K . ') + '. (Recovery)
Note that AGM presupposes full propositional logic which contains
connectives such as negation and disjunction that are not fully supported in DLs. For
instance, negations (:(A v B)) and disjunctions ((A v B) _ (C v D)) of DL
axioms are not expressible as DL axioms. As a result, the recovery postulate
(K . 6) cannot be satis ed by contraction operators de ned in most DLs [
To specify the minimal di erence between the original belief set and the contracted one, we need a notion of di erence between belief sets and a way of comparing them. A contraction that always picks the belief set that has the smallest (or weakest) di erence from the original belief set as the contracted one, will satisfy the minimal change property. In this paper, we use logical di erence as the measure of di erence. In Section 3 we de ned the notion of logical di erence between TBoxes in DLs. This can be easily extended to propositional logic by considering the TBoxes T and T 0 as belief sets and the GCI C v D; A v B as sentences in propositional logic.
The alternative postulate should be as close as possible to Recovery, in the sense that when propositional logic is assumed it coincides with recovery. The following is an equivalent formulation of the Recovery postulate in terms of logical di erence.
Lemma 3. Let K be a belief set, ' a sentence, . a contraction operator satissfying (K . 1) (K . 5) then . satis es (K . 6) i (K .
') [ f'g j= Di (K; K . ') ( ) Proof. (fFK)'rogj=)mj=DKDii(K( K(;KK;K.. ''.)')+)wh'i,chwiemhpalviees ((KK .. '')) ++ '' jj== DKi . (DKu;eKt o. 'd)e, tnhiutison(Kof. 'D)i [, W((e) rst prove K0 [ Di (K; K0 ) j= K. Assume K j= and K0 [ Di (K; K0 ) 6j= , t(choenndiittimonus3t),bseintchee Kcasj=e K,0 K6j=0 6j=; Di a(nKd; KDi0 )(6jK=; K. 0 F)r6j=om ththeedree enxiitsitosnaof Ds.it. tKh0!atj=is tf;ohflelotgwhsrj=eferocm.onSdKinitc0ieo6j=nKs ij=nantdheaKdn0edj=Kniti=.onNCoonwf(DKwie) p(mKrouvs.et1b)D,eiKs(aKtj=is;Ke0d!)bj=y . K!!0 6j=,. Condition 1 and 2 are already satis ed. Assume condition 3 is not satis ed then i(AtKs_m.Du'is!)t([Kbfe;)'Ktwgh0he)j=icjc=hDasiies (nt!Khota;tKp,oK.sKs'0ib0)j=l[iet Dafosi_lKlo( Kw0sj;=!K(K0 )a.jn=f'od)r K[s,o0fcm'6j=ogentj=srea(ndKftiec.;nticoen_. F,!i(nall!gy,j=frojm=t)u.
However, ( ) is not suitable for our purpose, as it still assumes certain expressive power of the underlying logic. As an example, take the TBox T = Cn(A v B) and let ' = A u C v B. If . satis es the Success postulate then TDL. 'su=chCasn(A;L),Cb,uwtefhAavue CT .v'B=g C6j=n(AAvvBB. tNCot)eththenat(, w)iitshsaatimsoerde. eTxapkriensgsiavlel the above into consideration, we propose the following set of postulates, where . is the contraction operator, ' a GCI: (T . 1) T . ' = Cn(T . ') (T . 2) T . ' T (T . 3) If ' 62 T , then T . ' = T . ((TT .. 45)) IIff 6jC=n'(',)th=enC'n (62 )T, t.h'en T . ' = T . (T . 6) There exists no T 0 such that T j= T 0 and T 0 6j= '
and Di (T; T . '.) j= Di (T; T 0 ) and T 0 6 .T1). '.
Postulates (T . 1) (T 5) are analogues of (K (K . 5). (T . 6) is the
alternative for (K . 6). It selects from all the belief sets which are faithful to
(T . 1) (T . 5) those that have the weakest logical di erence from the original
one. Most importantly, no expressive power of the underlying logic is assumed in
order to satisfy it. (T . 6) is stronger than (K . 6) as there are contraction
operators that satisfy (K . 6) but not (T . 6). The reason is that a contraction operator
which satis es (T . 6) must be a maxichoice contraction [
') [ f g) Proof.
We only sketch the proof from 1 to 2, the proof from 2 to 1 is similar. Assume Di 2(TK; Tan.d'), th62atKis. t'hebtuhtre'e c62onCdnit(i(oKns.i'n)th[efdeg)n. itWioen noofwDipromvuest b!esa'tis2saetdisbyed a!s '!.C'on62diKtio.n'1wishsicahtisfoleldowass f'ro2mK' a62ndCnK((=KC. n'()K[)f. Cgo).nCdiotniodnit2ioins 3 is satis ed where the reasoning is the same as in the proof of Lemma 3. Now let aKn0d=K(0K6 . K').['f ho!we'vegr,,tDhui s (K!;K'. 62')Dj=i (DKi ; (KK0 ;).KK0 )0, swathiischesvi(oKlat.e1s) (T( K.6)..5) In order for Lemma 4 to hold, the underlying logic needs to have certain expressive power, but as far as E L is concerned, this is not a problem. tu 5
The previous section proposed an alternative to the recovery postulate which assumes no expressive power of the underlying logic. We also proved that, assuming propositional logic, the proposed postulate characterises maxichoice contraction. In this section we develop algorithms that implement a contraction operator (maxichoice) for the DL E L.
Within the algorithms, let SubT(A) = fB j T j= B v Ag be the set of concept
names that are subsumed by A in a TBox T . Since E L has a polynomial time
subsumption checking procedure [
for A a subconcept of C or D do if A A0 2 T then
replace A with A0 in C or D T 0 ; for A 2 NC do if A is pseudo-primitive in T then
T 0 T 0 [ fB v AjB 2 SubT(A)g [ fA v CjA 2 SubT(C)g if A if A
A1 u u An 2 T then T 0 T 0 [ fB v AjB 2 SubT(A)g [ fA v CjA 2 SubT(C)g [ fA1 u u An v Ag
9R:A0 2 T then T 0 T 0 [ fB v AjB 2 SubT(A)g [ fA v CjA 2 SubT(C)g [ f9R:A0 v Ag [ fA v 9R:A0 g if A v 9R:C 2 T then
T 0 T 0 [ fB v 9R:CjB v A 2 T g if B v 9R:A 2 T then
T 0 T 0 [ fB v 9R:CjA v C 2 T g T
T 0
Algorithm 1: Algorithm Simplify(T; C v D)
Before carrying out steps that will result in contraction of a GCI C v D from a TBox T , we simplify C v D and reconstruct T in Algorithm 1. The main purpose is to deduce the implicit GCIs that involve a concept name on the left and an existential restriction on the right (such as A v 9R:B) and to deduce the implicit GCIs that involve only concept names (such as A v B). This will guarantee none of the implicit GCIs are eliminated unnecessarily in the contracted TBox. Upon termination T contains all subsumptions between concept names. Moreover, axioms of the form A B are replaced with A v B and B v A. The exception is that if A A1 u u An is in T , A v A1 u u An is not included as it can be deduced from the subsumptions between A and A1; : : : ; An. As a consequence of the simpli cation and reconstruction, when we reduce the contraction of C v D to contraction of either A v 9R:B or B v A for A; B concept names (as in Section 3) then concept A is guaranteed to be pseudo-primitive. At last, it is easy to check that Algorithm 1 returns a TBox that is equivalent to the input one.
Input: TBox T , GCI A1 u u An v B Output: TBox T 0 Simplify(T; A1 u u An v B) T 0 T if B is of the form B1 u u Bm then
Bi (B1; : : : ; Bm)
T 0 Contract(T; A1 u u An v Bi) else if B is pseudo-primitive in T then for i 1 to n do if Ai v B 62 T then
continue else
T 0
ContractCN(T 0 ; Ai; B) else if B is of the form 9R:C then for i 1 to n do if Ai v 9R:C 62 T then
continue else if Ai 2 NC then
T 0 ContractER(T 0 ; Ai; 9R:C) else if Ai is of the form 9R:A then
T 0 ContractCN(T 0 ; A; C) return T 0
Algorithm 2: Algorithm Contract(T; A1 u u An v B)
Algorithm 2 is our main algorithm. To contract GCIs of the form A1 u u An v B1 u u Bm, it is su cient to contract one of A1 u u An v Bi for 1 i m, as fA1 u u An v Big j= A1 u u An v B1 u u Bm. A selection function is used to model the user decision on which GCI to contract. According to Lemma 2, contraction of C v D can be reduced to contraction of either A v 9R:B in which case Algorithm 2 calls Algorithm 4 or B v A in which case Algorithm 2 calls Algorithm 3. Note that when concept B in the algorithm is pseudo-primitive, then due to Part 1 of Lemma 1, if T j= Ai v B then Ai must be a concept name. Similarly when B is of the form 9R:C, due to Part 2 of Lemma 1, the possible forms of concepts subsumed by B are xed.
Algorithm 3 handles contraction of GCIs of the form A v B where A; B are concept names (B is pseudo-primitive). It rst removes A v B from T as subsumption between concept names are all present in T . A v B may be implied by other GCIs which have to be eliminated. In detail, for every concept Input: TBox T , GCI A v B where A; B 2 NC Output: TBox T 0 T 0 T T 0 T 0 n fA v Bg for C 2 NC and A v C 2 T do if C v B then
T 0 T 0 n fA v C; C v Bg return T 0
Algorithm 3: Algorithm ContractCN(T; A v B) name C such that A v C; C v B 2 T , either A v C or C v B is eliminated. Once again the decision is modelled by the selection function . We do not have to consider the case that there are concepts of the form 9R:C such that A v 9R:C; 9R:C v B 2 T , because due to Lemma 1, this will imply B is not pseudo-primitive.
Algorithm 4 handles contraction of GCIs of the form A v 9R:B where A; B are concept names (A is pseudo-primitive). If T j= A v 9R:B then either there is a concept 9R:D such that A v 9R:D; D v 9B 2 T or there is a concept name D such that A v D; D v 9R:B 2 T . For each of the two cases there are two ways of breaking the entailment, the decision is again modelled by the selection function . Depending on the decision either Algorithm 4 or Algorithm 3 is called.
Input: TBox T , GCI A v 9R:B where A; B 2 NC Output: TBox T 0 T 0 T n fA v 9R:Bg foreach D 2 NC such that A v 9R:D 2 T and D v B 2 T do
T 0 fContractER(T 0 ; A v 9R:D); ContractCN(T 0 ; D v B)g foreach D 2 NC such that A v D 2 T and D v 9R:B 2 T do
T 0 fContractER(T 0 ; D v 9R:B); ContractCN(T 0 ; A v D)g return T 0
Algorithm 4: Algorithm ContractER(T; A v 9R:B)
The algorithms successfully implement a contraction operator for the DL EL as justi ed by the following theorem.
TDh)e=orCeomntr1a.ctLientgT(Tb;eCanvEDL),TtBheonx, .CsvatiDs easn(ETL. 1G)CI. If we de ne T . (C v (T . 6).
Proof.
We only sketch the proof for satisfaction of (T . 6) as others are straightforward. D u62e Cton(LTe m.'m)ath4e(nT'. 62) Cisns(a(tTis. 'ed) [if fthge)fofollrow'i;ng GhColIdss.: IItf is c2leaCrnf(rTo m) atnhde algorithm, whenever a GCI is removed, it must be the case that 1) there is a cGaCseIs, '22CCnn((T()T s.u'ch)[thfatg)f ; g j= ', and 2 T . ', and 2) = '. In bottuh The algorithms will run in polynomial time because each for loop in the algorithm iterates a constant number of times and the most time consuming operation is subsumption checking which has a polynomial procedure. In the following, we give an example for contracting a GCI from a TBox. At the beginning Algorithm 2 is called.
Example 1. T = fC v F; F v A; E v D u B; D v 9R:Ag, we want to contact E u9R:D v 9R:A from T . Firstly, upon termination of Simplify(T; E u9R:D v 9R:A), T = fC v F; F v A; C v A; E v B; E v D; D v 9R:A; E v 9R:Ag, that is the implicit GCIs C v A; E v B; E v D and E v 9R:A are made explicit. Now we will proceed to the last if statement of Algorithm 2. As E v 9R:A 2 T , ContractER(T; E v 9R:A) is called. Now in running ContractER(T; E v 9R:A), E v 9R:A is rst removed resulting in T = fC v F; F v A; C v A; E v B; E v D; D v 9R:Ag. As E v D and D v 9R:A are in T , one of them needs to be removed. Assume the selection function selects E v D, which means ContractCN(T; E; D) is called which removes E v D from T resulting in T = fC v F; F v A; C v A; E v B; D v 9R:Ag. Upon termination of Algorithm 2 T = fC v F; F v A; C v A; E v B; D v 9R:Ag. The GCIs removed are E v D and E v 9R:A. It is easy to see that T [ fE v Dg j= E u 9R:D v 9R:A and T [ fE v 9R:Ag j= E u 9R:D v 9R:A.
Note that if we were to use a belief base approach, where only the explicit GCIs are considered, we will end up with T = fC v F; F v A; D v 9R:Ag or T = fC v F; F v A; E v D u Bg. In either case we have some implicit GCIs removed unnecessarily. For instance, in the former case, E v D u B is removed therefore T no longer entails E v B, however E v B has nothing to do with T entailing E u 9R:D v 9R:A. In this respect our approach, which concerns belief contraction with belief sets (logically closed theory), turns out to be more plausible as it eliminates only what is necessary and preserves the rest. 6
Related Work
The problem of belief revision in DLs has been extensively studied. So far existing
works propose di erent constructions of revision operators that consider only
explicitly presented GCIs [6{8]. In these works the resulting TBox is obtained
by adding the new GCIs to the original TBox then resolving any inconsistency
caused. The latter part is achieved by rst using the debugging service in [
Conclusion and Future Work In this paper we have developed algorithms for contracting GCIs from an E L TBox. These algorithms are signi cant for a number of reasons. Firstly, the operation they realise adheres to all of the basic AGM contraction postulates except the recovery postulate. We argue that the original recovery postulate is not appropriate to DLs as they are less expressive than classical logics. Therefore, we introduced a variant of the recovery postulate that is based on the notion of logical di erence. In fact, when the underlying logic is classical, our postulates coincide with the AGM. As such, ours is the closest account of belief change for DLs to the AGM account of those currently proposed in the literature. We argue that it is more important to focus on contraction since revision behavior is simply set union in E L as it is not possible to have an inconsistent TBox.
It should be noted that as our contraction operation only guarantees minimal change in terms of logical di erence, all axioms could change their syntactic form so that it may be the case that the contracted TBox bears no syntactic resemblance to the original TBox. However, for the DL E L, this may not be undesirable. Additionally, the contracted TBox obtained by our contraction operator may contain arbitrary GCIs that violate our assumptions, thus preventing further application of the contraction operator. In other words our algorithm can not handle iterated contraction. In future work, we would like to address these issues. It would also be useful to consider the supplementary AGM postulates and how they or similar postulates would be satis ed.