An essential task in managing description logic (DL) ontologies is the elimination of problematic axioms. Such elimination is formalised as the operation of contraction in belief change. In this paper, we investigate contraction over DL-LiteR TBoxes. In belief change, a well known approach for defining contraction is via epistemic entrenchments which are preference orderings over formulas. The approach however is not applicable in DL-LiteR as classic belief change assumes an underlying logic that is different from DL-LiteR. Thus we reformulate the epistemic entrenchment approach to make it applicable to DL-LiteR. We then provide instantiation for the reformulated approach.
Description logic (DL) [
The dominant approach in belief change is the so called AGM framework [
In this paper, we will define and instantiate contraction functions under DLs. We
focus on DL-LiteR which is the main language of the DL-Lite family [
Our solution to the inapplicability which is also our main technical contribution is to reformulate the mechanism so as to make it independent of the underlying logic. That means although we use it for DL-LiteR it has the potential to be applied for DLs in general. We first propose the notion of critical axioms. Roughly speaking, the critical axioms of with respect to are those axioms that are critical in deciding whether to retain or to remove when contracting by . The decision is then made by comparing the critical axioms with . The rule is that if any of the critical axioms are strictly more preferred than then will be retained otherwise it is removed. We identify a set of rationality postulates satisfied by the contraction functions defined with the reformulated mechanism. Among other properties, it is clear from the postulates, functions thus defined are always successful in accomplishing the required elimination of axioms. An algorithm that instantiates the functions is provided at the end. 2
In this section we introduce the family of DL-Lite languages. The core of the family is DL-Litecore which has the following syntax:
B ! A j 9R
C ! B j :B
R ! P j P
E ! R j :R where A denotes an atomic concept, P an atomic role, P the inverse of the atomic role P . B denotes a basic concept which can be either an atomic concept or an unqualified existential quantification on basic role. C denotes a general concept which can be either a basic concept or its negation. E denotes a general role which can be either an atomic role or its negation. We also include ? denoting the empty set and > denoting the whole domain. We use B to represent the universal set of basic concepts and R as the universal set of atomic roles and their inverses. For an inverse role R = P , we write R meaning P for the convenience of presentation. In this paper, we assume B and R are finite.
A DL-Litecore knowledge base consists of a TBox and an ABox. A TBox is a finite set of concept inclusion axioms of the form B v C. That is only basic concepts can appear on the left-hand side of a concept inclusion. An ABox is a finite set of assertions of the form A(a) or P (a; b).
There are two major extensions of DL-Litecore, namely DL-LiteR and DL-LiteF . DL-LiteR extends DL-Litecore with role inclusion axioms of the form R v E. That is only basic roles can appear on the left-hand side of a role inclusion. DL-LiteF extends DL-Litecore with assertions of the form (funct R) which specifies functionality on basic roles.
The semantics of a DL-Lite language is given in terms of interpretations. An interpretation I = ( I ; I ) consists of a nonempty domain I and an interpretation function I that assigns to each atomic concept A a subset AI of I , and to each atomic role P a binary relation P I over I , and to each individual name a an element aI of I . The interpretation function is extended to general concept, general roles, and special symbols as follows: ?I = ;, >I = I , (P )I = f(o2; o1) j (o1; o2) 2 P I g, (9R)I = fo j 9o0:(o; o0) 2 RI g, (:B)I = I n BI , and (:R)I = I I n RI . An interpretation I satisfies a concept inclusion B v C if BI CI , a role inclusion R v E if RI EI , a concept assertion A(a) if aI 2 AI , a role assertion P (a; b) if (aI ; bI ) 2 P I , and a functionality assertion (funct R) if (o; o1) 2 RI and (o; o1) 2 RI implies o1 = o2. I satisfies a TBox T (or ABox A) if I satisfies each axiom in T (resp., each assertion in A). I is a model of a TBox T (or a TBox axiom ) denoted as I j= T (resp., I j= ) if it satisfies T (resp., ). A TBox or an axiom is consistent if it has at least one model. A TBox T logically implies an axiom , written T ` , if all models of T are also models of . Two TBox axioms and are logically equivalent, written , if they have identical set of models. We use ` to denote that is a tautology such as A v A. > standing alone also denotes a tautology. We use f> v ?g to denote the (unique) inconsistent TBox.
The closure of a TBox T , denoted as cl(T ), is the set of all TBox axioms such
that T j= . The closure of a DL-Lite TBox is finite, in fact, the size of the closure of
a TBox T is quadratic with respect to the size of T [
In general, TBox axioms are logically connected meaning that they imply and are implied by other axioms. One exception is the functionality assertions. For DL-LiteF , if ABox is not considered and the TBox is coherent then a functionality assertion do not imply and is not implied by any other axioms, thus its removal and addition is nothing but set operations. For this reason, we only consider DL-Litecore and DL-LiteR TBoxes. Since DL-Litecore is a subset of DL-LiteR, contraction functions for DLLitecore can be obtained identically as for DL-LiteR only more simpler. We present the results for DL-LiteR only. In the upcoming sections all TBoxes are assumed to be DL-LiteR ones which are denoted by lower case Greek letters ( ; ; : : :). Also we denote the universal set of TBox axioms for DL-LiteR as LR. Given a set of TBox axioms 1; : : : ; n, their conjunction is denoted as 1 ^ ^ n. As expected, an interpretation I is a model of 1 ^ ^ n if it satisfies all the conjuncts. We assume LR contains any conjunction of TBox axioms. 3
Entrenchment-Based Contraction for DL-LiteR In this section, we deal with the problem of eliminating axioms from DL-LiteR TBoxes. Our strategy is to define a contraction function . that takes as input a logically closed TBox T and an axiom and returns as output a TBox T . such that is not entailed.
In order to eliminate an axiom from a TBox T , we need to remove at least one axiom from each subset S of T such that S ` . For example, if T consists of A v B; B v C, and A v C and we want to remove A v C then since the set fA v B; B v Cg implies A v C, either A v B or B v C must be removed from T . Obviously, we need some preference information over the axioms to guide us in deciding which one of A v B and B v C to remove.
Thus we start with specifying a preference ordering for all the TBox axioms. Following the AGM tradition we call the ordering an epistemic entrenchment. Formally, an epistemic entrenchment is a binary relation over LR and is associated with a TBox. Given an epistemic entrenchment , we say an axiom is equally or more entrenched than an axiom iff . The strict relation < is defined as and 6 and the equivalent relation ' is defined as and . We say is strictly more entrenched than iff < , and is equally entrenched to iff ' . The basic idea is that the more entrenched an axiom the more important or more preferred it is thus in deciding which axioms to remove it is intuitive to remove the less entrenched ones whenever possible.
Not all preference ordering are appropriate in this context. We require an epistemic
entrenchment to satisfy the following conditions:
(DE1) If and then (Transitivity)
(DE2) If ` then (Dominance)
(DE3) ^ or ^ (Conjunctiveness)
(DE4) If T is consistent then 62 T iff for every (Minimality)
(DE5) If for every then ` (Maximality)
Thus an epistemic entrenchment is transitive (DE1); logically weaker axioms are equally
or more entrenched than logically stronger ones (DE2); conjunctions of axioms are
equally or more entrenched than one of their conjuncts (DE3); axioms not in the
associated TBox are least entrenched (DE4); and tautologies are most entrenched (DE5).
(DE1)–(DE5) are obtained by recasting conditions (EE1)–(EE5) of [
Lemma 1 Let
be an entrenchment. 1. Either 2. If 3. If for all ; then then 2 LR.
or ^ ' '
(Connectivity) Proof. 1. For any ; 2 LR we have by Conjunctiveness that either ^ or ^ . If ^ we get from Dominance ^ and from Transitivity . If ^ we get from Dominance ^ and from Transitivity . 2. Suppose . We have by Conjunctiveness that either ^ or ^ . If ^ then we have by Transitivity that ^ . Thus in either case we have ^ . Since we also have ^ follows from Dominance, it must be that ^ ' . us 3. Let ' .
. Then it follows from Dominance that and which give tu As a direct consequence of Lemma 1 (i.e. Part 2) the ranking of a conjunction in an epistemic entrenchment is uniquely determined by its conjuncts. This means we only need to specify preferences between all the single axioms.
Having an epistemic entrenchment associated with each TBox is only the first step. It remains to devise mechanism to make use of the preference information in deciding the axioms to remove and to retain during a contraction. Although AGM epistemic entrenchment contraction provides such a mechanism, the contraction is defined while assuming an underlying logic that subsumes propositional logic. As most DLs including DL-LiteR do not subsume propositional logic, the direct transition of the mechanism to contraction under DLs is not possible. An obvious obstacle in such transition is that the mechanism refers to disjunctions of formulas and DLs do not allow disjunctions of axioms. We deal with this matter by reformulating the mechanism such that logic dependent terms such as disjunctions do not play a part.
Let’s consider the contraction of an axiom from a TBox T with an associated
epistemic entrenchment . Since the purpose is to eliminate , we have to make sure
the axioms retained do not entail . For each axiom of T if it has nothing to do with
the entailment of that is there is no set of axioms S such that S 6` and f g [ S `
then we can be sure it is safe to retain . In fact must be retained if we respect the
principle of minimal change [
Definition 1 Let ; be DL-LiteR TBox axioms. The set of critical axioms of respect to , denoted as C ( ), is defined as follows: If there is no set of axioms S such that f g [ S ` and S 6` Otherwise, 2 C ( ) iff then C ( ) = f>g.
with 1. For each set of axioms S such that f g [ S ` and S 6` we have f g [ S ` , 2. There is no axiom which satisfies condition 1 and is such that 6` and ` .
If has nothing to do with the entailment of , then intuitively no axiom is critical to in contracting , however, for technical reason we take that the only critical axiom in this case is the tautology. Besides the limiting cases, the critical axioms are logically the weakest axioms that can replace in entailing with the help of other axioms (i.e., the set of axioms S).
The following properties for critical axioms follow immediately from Definition 1. Lemma 2 Let ;
be DL-LiteR TBox axioms. Then Proof. 1. Since ` we have ; 6` and f g [ ; ` . Moreover, is the weakest axiom such that f g [ ; ` thus it is the only axiom qualified as an element of C ( ).
2. Since the definition of critical axioms only concerns the logical contents, logical equivalent axioms always produce the identical set of critical axioms.
3. Suppose 2 C ( ) then for all S such that f g [ S ` and S 6` , f g [ S ` . Then by the definition of critical axioms, for any 0 2 C ( ) we have f 0g [ S ` and 0 is logically the weakest axiom satisfying the condition. Clearly, 0 fulfils all criteria for being an element of C ( ).
Now let’s demonstrate why the critical set of axioms are so critical in deciding the axioms to retain in a contraction. Recall that the retainment of in contracting has a lot to do with the set S such that S 6` and f g [ S ` . We begin with a lemma showing how rankings of critical axioms of with respect to affect the rankings of axioms in S.
Lemma 3 Let ; be DL-LiteR TBox axioms and an epistemic entrenchment. If 2 C ( ) and < then for any set of axioms S such that f g [ S ` and S 6` there is 2 S such that .
Proof. Suppose 2 C ( ) and < . The definition of critical axioms implies that for any set of axioms S such that f g [ S ` and S 6` , f g [ S ` . Suppose without loss of generality that S = f 1; : : : ; ng, thus ^ 1 ^ ^ n ` . It then follows from Dominance that ^ 1 ^ ^ n . Assumes < i for 1 i n. Then it follows from Conjunctiveness that < n which implies by Transitivity < a contradiction! Thus there is . ^ 1 ^ ^ 2 S such that tu tu According to Lemma 3, if any critical axiom of with respect to is strictly more entrenched than then for any set of axioms S which does not entail but does so when united with , there is at least one axiom of S that is not strictly more entrenched than . This means together with all axioms strictly more entrenched than do not entail . It will be clear that in contracting if we only retain such ’s then it is guaranteed will no longer be entailed. This leads to the following definition of entrenchment-based contraction function.
Definition 2 Let T be a DL-LiteR TBox with an associated epistemic entrenchment . A function . is an entrenchment-based contraction function for T iff
T .
=
T \ f T j there is 2 C ( ) such that < g if 2 T and 6` otherwise
By Definition 2, in the contraction of T by , if is in T , then the existence of a critical axiom of (w.r.t. ) being strictly more entrenched than is a sufficient condition for retaining . In the two limiting cases that is a tautology or it is not in T , the original TBox T is returned meaning that all axioms are retained. For convenience we refer twoe saays tthhee cfounntcrtaioctning. aisxidoemte,rTmitnheedobryigtihnealeTpBisotexm,aicndenTtre.nchthmeernetsult.inTgo TshBoowx tahnadt entrenchment-based contraction behaves properly and most importantly is always successful in eliminating the contracting axioms we provide the following representation theorem.
Theorem 1 Let T be a DL-LiteR TBox and . an entrenchment-based contraction function for T then it satisfies the following postulates: (T .. 1) T .. = cl(T . ) (((((TTTTT .... c6342r)))))IIITfffI f6` 622,TthT,,Tettnahhneennd62TTthTe..re. i==s TT2. C ( ) such that 2 T . then 2 T . (PTTrBoo.ox1f.)T–S(uTwpip.toh4s)ae,n( T.as.issocrca)ina, taeendndtre(epTnisct.he6mm)e.icnStae-btniastrsfeaencdctihcomonneotnrfat(cTtio..nW2)feuannncedtei(doTnt o.f3os)rhoftohwlelo.DwLssa-iLtmisimtfieeeRsdTSiuapt=(epTloycsl.ef(r1To)m:),I2Dfw`eecfil(hnTaitoviore.nT)2,62..wTe=ntheecenld(Tittof.oshll)oo.wwFsorfrto2hmeTpDre.inficn.iipAtaioclnccoa2rsdetih,nalgettTto6`.Defia=nnditTio.nS22in,Tciet. ssuufbfisCceaetssfeto11;,s:6`h:o: w;: Snign2ocefTTa n2.dctslh(ueTcrhe.itsha)t, bf2y1Ct;h:e(: c:o;)msnupgcahc`ttnhea.stsTohfe<nDbL.y-TLDhiteeefirRen,iattirhoeentrwe2,oiswcaeafishenasiv:tee f 1; : : : ; ng T and there is i 2 C ( i) such that < i for 1 i n. Then since T = cl(T ),f 1; : : : ; ng T , and f 1; : : : ; ng ` we have 2 T . If there is no S such that S [ f g ` and S 6` then by Definition 1, C ( ) = f>g. It then follows from Maximality and Connectivity (part 1 of Lemma 1) that > and we are done. Now suppose there is S such that S [ f g ` and S 6` . Since f 1; : : : ; ng ` , we have f 1; : : : ; ng [ S ` . Now let’s show f 1; : : : ; ng [ S ` . If f 2; : : : ; ng [ S ` then by the monotonicity of DL-LiteR we have f 1g [ f 2; : : : ; ng [ S ` and if f 2; : : : ; ng [ S 6` then it follows from Definition 1 and 1 2 C ( 1) that f 1g [ f 2; : : : ; ng [ S ` . Thus in either case we have f 1g [ f 2; : : : ; ng [ S ` . Similarly we can replace i by i for 2 i n to get f 1; : : : ; ng [ S ` which implies f 1 ^ ^ ng [ S ` . Since by Definition 1 any critical axiom 2 C ( ) is logically the weakest one such that f g [ S ` , there must be a such that 1 ^ ^ n ` which implies by Dominance 1 ^ ^ n . Since < i for 1 i n, we have by Lemma 1 (part 2) and Transitivity that < 1 ^ ^ n. Again by Transitivity we have < and we are done.
Case 2, ` : Since T = cl(T ) and ` , we have 2 T . Since ` , there is no S such that S [ f g ` and S 6` . Thus by Definition 1, C ( ) = f>g. Since 6` we have by Maximality and Connectivity that < >.
(T . 4): Suppose 6` . By Lemma 2 (part 1) we have C ( ) = f g. It follows from 6<(T, .6`6):, SaunpdpDoesefinition 2. tThahten w62eTha.ve. by Lemma 2 (part 2) C ( ) = C ( ) for taaDhnneeydfin(TnTiat.i.n2ocdnrTwc)2a:,e.nShunafpo2vopteloblTobsewey.dsLifiefmi2emmrmemTpnelatid.aei1nsadt(tephlaayrt2tfr3oC)m2 (DT'e)fiainns.ditsTituohhcneehrn2et.haiScasoctosru2d2pinpCgTost(eo. D). 2seIufifcTnhita62itohnnadTt26`,oTr<.`B.y. Since 2 C ( ) we have by Lemma 2 (part 3) that C (. ) C ( ). Thus 2 C ( ). It then follows from < and Definition 2 that .
According to Theorem 1, an entrenchment-based contraction function produces a logically closed TBox (T . 1) which does not entail the contracting axiom unless it is a tautology (T . 4). The produced TBox is not larger than the original one (T . 2). If the contracting axiom is not entailed, then nothing has to be done (T . 3). The contraction function is syntax-insensitive (T . 6). (T . 1)–(T . 4) and (T . 6) all have their origins in the AGM framework. Unlike them, (T . cr) has no counterpart in the AGM framework. It captures the sufficient condition for retaining an axiom in our reformulated mechanism.
(
A v C C v D ) <
B v D B v A < ( B v C )
A v D
To illustrate entrenchment-based contraction, suppose a TBox T and its associated
epistemic entrenchment are as shown above. Notice that conjunction of axioms are
not shown as their rankings in the epistemic entrenchment uniquely are determined by
the least entrenched conjunct. In eliminating B v D through the entrenchment-based
contraction determined by , only the boxed axioms are retained. Let’s examine the
fate of A v C in this elimination. According to [
Notice that although we allow conjunction of axioms, we do not have to check for their retainments. It follows from (T . 1) that ^ 2 T . if and only if 2 T . and 2 T . . Thus it is sufficient to consider single axioms only. This significantly simplifies the computation of the contraction result. We provide the CONT algorithm for obtaining the contraction outcomes of entrenchment-based contraction functions. CONT takes as input a logically closed TBox T , the epistemic entrenchment for T , and the TBox axiom to be contracted. CONT starts by initiating the resulting TBox T to empty. Then it checks for each TBox axioms of T (line 2) weather any of its critical axioms (line 3) is strictly more entrenched than (line 4). If it is the case then is added to the resulting TBox T (line 5). Finally, the resulting TBox T is returned. It is easy to see that CONT instantiates entrenchment-based contraction function.
Algorithm 1: CONT
Input: TBox T , epistemic entrenchment for T , and TBox axiom
Output: TBox T 1 T := ;; 2 foreach TBox axiom of T do 3 foreach 2 C ( ) do
5 T := T [ f g;
Proposition 1 Let T be a DL-LiteR TBox with an associated epistemic entrenchment . A function . is an entrenchment-based contraction function for T and is determined by iff
T .
= CONT(T ; ; ) for all DL-LiteR TBox axioms . 4
In dealing with changes over DL ontologies, many [
In a more general setting, [
[
[
We looked into methods of eliminating problematic axioms of DL-LiteR TBoxes. The entrenchment-based contraction is thus defined by reformulating the AGM epistemic entrenchment contraction. The reformulation on the one hand solves the expressibility issues and on the other hand yields a proper contraction function.
There are many aspects of this work that are worth investigating further. We are in the process of devising an algorithm for computing the critical axioms which will guarantee CONT runs in polynomial time. The definition of critical axioms and also that of entrenchment-based contraction although assuming DL-LiteR are in fact independent of the underlying logic. Their generalisation to DLs in general is on the way. The main difficulty in the generalisation is that unlike DL-LiteR most DLs are not finite under logical closure.