=Paper=
{{Paper
|id=Vol-1193/paper_40
|storemode=property
|title=Rational Elimination of DL-Lite TBox Axioms
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_40.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/ZhuangWWA14
}}
==Rational Elimination of DL-Lite TBox Axioms==
https://ceur-ws.org/Vol-1193/paper_40.pdf
Rational Elimination of DL-Lite TBox Axioms
Zhiqiang Zhuang1 , Zhe Wang1 , Kewen Wang1 , and Grigoris Antoniou2
1
School of Information and Communication Technology, Griffith University, Australia
2
School of Computing and Engineering, University of Huddersfield, UK
Abstract. An essential task in managing description logic (DL) ontologies is the
elimination of problematic axioms. Such elimination is formalised as the opera-
tion of contraction in belief change. In this paper, we investigate contraction over
DL-LiteR TBoxes. In belief change, a well known approach for defining contrac-
tion is via epistemic entrenchments which are preference orderings over formulas.
The approach however is not applicable in DL-LiteR as classic belief change as-
sumes 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.
1 Introduction
Description logic (DL) [2] ontologies are subject to frequent changes. For instance, out-
dated or incorrect axioms have to be eliminated from the ontologies and newly formed
axioms have to be incorporated into the ontologies. Therefore a mandatory task for man-
aging DL ontologies is to deal with such changes. In the field of belief change, extensive
work has been done on formalising various kinds of changes over knowledge bases. In
particular, the elimination of old knowledge is called contraction and incorporation of
new knowledge is called revision. To handle changes over DL ontologies it makes sense
to take advantage of the many existing techniques in belief change. Consequently, many
have investigated contraction and revision under DLs [7,8,18,23,22,19,20].
The dominant approach in belief change is the so called AGM framework [1,9]
which assumes an underlying logic that includes propositional logic. In the framework,
the knowledge base to which changes are made is called a belief set which is a logically
.
closed set of formulas. An AGM contraction function − takes as input a belief set K
.
and a formula φ and returns another belief set K −φ such that φ is not entailed. The
epistemic entrenchment contraction function [9,10] is one such contraction function.
The basic idea for epistemic entrenchment contraction is to rank all the formulas by
their informational value. The higher up in the ranking the more informational value a
formula holds. The formulas returned by the contraction function are then determined
by comparing rankings of the related formulas with the intuition that if some formulas
have to be removed then remove the ones with the least informational value whenever
possible.
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 [5]. DL-Lite un-
derlies the OWL 2 QL profile of OWL 2 and gains its popularity through efficient query
answering. The contraction function to be defined is for logically closed DL-LiteR
TBoxes. Inspired by epistemic entrenchment contraction function, we first rank all the
DL-LiteR TBox axioms such that the higher up in the ranking the more preferred an ax-
iom is. As in epistemic entrenchment contraction function, we then need a mechanism
for comparing rankings of related axioms so as to determining the outcomes of the con-
traction function. However, due to the assumption of AGM framework on a logic that
subsumes propositional logic, the mechanism used in epistemic entrenchment contrac-
tion function are not applicable under DL-LiteR . An obvious obstacle is that DL-LiteR
does not allow disjunction of axioms whereas the comparison of rankings between dis-
junction of formulas with the formula to be contracted is essential to the mechanism for
epistemic entrenchment contraction.
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 reformu-
lated 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 DL-Lite
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 | ∃R C → B | ¬B R → P | P− E → R | ¬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 in-
terpretation 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 = {(o2 , o1 ) | (o1 , o2 ) ∈ P I },
(∃R)I = {o | ∃o0 .(o, o0 ) ∈ RI }, (¬B)I = ∆I \ B I , and (¬R)I = ∆I × ∆I \ RI .
An interpretation I satisfies a concept inclusion B v C if B I ⊆ C I , a role inclu-
sion R v E if RI ⊆ E I , a concept assertion A(a) if aI ∈ AI , a role assertion
P (a, b) if (aI , bI ) ∈ P I , and a functionality assertion (funct R) if (o, o1 ) ∈ RI and
(o, o1 ) ∈ 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 |= T (resp., I |= φ) 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
{> v ⊥} 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 |= φ. 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 [17]. In the upcoming sections all
TBoxes are assumed to be closed.
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 noth-
ing 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 DL-
Litecore 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 de-
note 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 {A v B, B v
C} 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. Fol-
lowing 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 φ 6∈ 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 asso-
ciated TBox are least entrenched (DE4); and tautologies are most entrenched (DE5).
(DE1)–(DE5) are obtained by recasting conditions (EE1)–(EE5) of [10] to DL-
LiteR thus they carry the same intuitions as (EE1)–(EE5) which are widely accepted
in belief revision community. Among other properties, it can be derived from (DE1)–
(DE5) that an epistemic entrenchment is connected, a conjunction of axioms is equally
entrenched to its least entrenched conjunct, and logically equivalent axioms are equally
entrenched.
Lemma 1 Let ≤ be an entrenchment.
1. Either φ ≤ ψ or ψ ≤ φ (Connectivity)
2. If ψ ≤ φ then φ ∧ ψ ' ψ
3. If φ ≡ ψ then φ ' ψ
for all φ, ψ ∈ LR .
Proof. 1. For any φ, ψ ∈ 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
φ ∧ ψ ' ψ.
3. Let φ ≡ ψ. Then it follows from Dominance that φ ≤ ψ and ψ ≤ φ which give
us φ ' ψ.
t
u
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 {ψ} ∪ S ` φ
then we can be sure it is safe to retain ψ. In fact ψ must be retained if we respect the
principle of minimal change [1,11] which requires to retain as much as possible axioms
of T . If ψ does play a part in the entailment of φ that is there is an S such that S 6` φ
and {ψ} ∪ S ` φ then it is safe to retain ψ only if for each such set S at least one axiom
of it is not retained. Thus we have to decide whether to favour ψ or axioms of S. We
propose the following notion of critical axioms that will aid such decisions. Basically,
the critical axioms of ψ with respect to φ are those axioms whose rankings in ≤ are
critical in deciding whether to retain ψ in the contraction of φ.
Definition 1 Let φ, ψ be DL-LiteR TBox axioms. The set of critical axioms of ψ with
respect to φ, denoted as C φ (ψ), is defined as follows:
If there is no set of axioms S such that {ψ} ∪ S ` φ and S 6` φ then C φ (ψ) = {>}.
Otherwise, σ ∈ C φ (ψ) iff
1. For each set of axioms S such that {ψ} ∪ S ` φ and S 6` φ we have {σ} ∪ 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
1. If ψ ` φ then C φ (ψ) = {φ}
2. If φ ≡ ψ then C ψ (δ) = C φ (δ) and C δ (ψ) = C δ (φ) for any δ ∈ LR
3. If σ ∈ C φ (ψ) then C φ (σ) ⊆ C φ (ψ)
Proof. 1. Since ψ ` φ we have ∅ 6` φ and {ψ} ∪ ∅ ` φ. Moreover, φ is the weakest
axiom such that {φ} ∪ ∅ ` φ 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 σ ∈ C φ (ψ) then for all S such that {ψ}∪S ` φ and S 6` φ, {σ}∪S ` φ.
Then by the definition of critical axioms, for any σ 0 ∈ C φ (σ) we have {σ 0 } ∪ S ` φ and
σ 0 is logically the weakest axiom satisfying the condition. Clearly, σ 0 fulfils all criteria
for being an element of C φ (ψ).
t
u
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 {ψ} ∪ 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
σ ∈ C φ (ψ) and φ < σ then for any set of axioms S such that {ψ} ∪ S ` φ and S 6` φ
there is γ ∈ S such that γ ≤ φ.
Proof. Suppose σ ∈ C φ (ψ) and φ < σ. The definition of critical axioms implies that
for any set of axioms S such that {ψ} ∪ S ` φ and S 6` φ, {σ} ∪ S ` φ. Suppose
without loss of generality that S = {γ1 , . . . , γn }, thus σ ∧ γ1 ∧ · · · ∧ γn ` φ. It then
follows from Dominance that σ ∧ γ1 ∧ · · · ∧ γn ≤ φ. Assumes φ < γi for 1 ≤ i ≤ n.
Then it follows from Conjunctiveness that φ < σ ∧ γ1 ∧ · · · ∧ γn which implies by
Transitivity φ < φ a contradiction! Thus there is γ ∈ S such that γ ≤ φ.
t
u
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 ∩ {ψ | there is σ ∈ C φ (ψ) such that φ < σ} if φ ∈ T and 6` φ
.
T −φ =
T otherwise
for all DL-LiteR TBox axioms φ.
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 origi-
nal TBox T is returned meaning that all axioms are retained. For convenience we refer
.
to φ as the contracting axiom, T the original TBox, and T −φ the resulting TBox and
.
we say the function − is determined by the epistemic entrenchment ≤. To show that
entrenchment-based contraction behaves properly and most importantly is always suc-
cessful 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 −φ)
. .
(T −2) T −φ ⊆ T
. .
(T −3) If φ 6∈ T , then T −φ = T
. .
(T −4) If 6` φ, then φ 6∈ T −φ
. . .
(T −cr) If ψ ∈ T and there is σ ∈ C φ (ψ) such that σ ∈ T −φ then ψ ∈ T −φ
. . .
(T −6) If φ ≡ ψ, then T −φ = T −ψ
.
Proof. Suppose − is an entrenchment-based contraction function for the DL-LiteR
.
TBox T with an associated epistemic entrenchment ≤. We need to show − satisfies
. . . . . .
(T −1)–(T −4), (T −cr), and (T −6). Satisfaction of (T −2) and (T −3) follows imme-
diately from Definition 2.
. .
(T −1): If ` φ or φ 6∈ T then it follows from Definition 2 that T −φ = T . Since
. .
T = cl(T ), we have T −φ = cl(T −φ). For the principal case, let 6` φ and φ ∈ T .
. .
Suppose ψ ∈ cl(T −φ), we need to show ψ ∈ T −φ. According to Definition 2, it
suffices to show ψ ∈ T and there is σ ∈ C φ (ψ) such that φ < σ. There are two cases:
.
Case 1, 6` ψ: Since ψ ∈ cl(T −φ), by the compactness of DL-LiteR , there is a finite
.
subset {δ1 , . . . , δn } of T −φ such that {δ1 , . . . , δn } ` ψ. Then by Definition 2, we have
{δ1 , . . . , δn } ⊆ T and there is σi ∈ C φ (δi ) such that φ < σi for 1 ≤ i ≤ n. Then since
T = cl(T ),{δ1 , . . . , δn } ⊆ T , and {δ1 , . . . , δn } ` ψ we have ψ ∈ T . If there is no S
such that S ∪ {ψ} ` φ and S 6` φ then by Definition 1, C φ (ψ) = {>}. 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 ∪ {ψ} ` φ and S 6` φ. Since {δ1 , . . . , δn } ` ψ, we
have {δ1 , . . . , δn } ∪ S ` φ. Now let’s show {σ1 , . . . , σn } ∪ S ` φ. If {δ2 , . . . , δn } ∪
S ` φ then by the monotonicity of DL-LiteR we have {δ1 } ∪ {δ2 , . . . , δn } ∪ S ` φ
and if {δ2 , . . . , δn } ∪ S 6` φ then it follows from Definition 1 and σ1 ∈ C φ (δ1 ) that
{δ1 } ∪ {δ2 , . . . , δn } ∪ S ` φ. Thus in either case we have {δ1 } ∪ {δ2 , . . . , δn } ∪ S `
φ. Similarly we can replace δi by σi for 2 ≤ i ≤ n to get {σ1 , . . . , σn } ∪ S ` φ
which implies {σ1 ∧ · · · ∧ σn } ∪ S ` φ. Since by Definition 1 any critical axiom
σ ∈ C φ (ψ) is logically the weakest one such that {σ} ∪ 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 ψ ∈ T . Since ` ψ, there is no S
such that S ∪ {ψ} ` φ and S 6` φ. Thus by Definition 1, C φ (ψ) = {>}. Since 6` φ we
have by Maximality and Connectivity that φ < >.
.
(T −4): Suppose 6` φ. By Lemma 2 (part 1) we have C φ (φ) = {φ}. It follows from
.
φ 6< φ, 6` φ, and Definition 2 that φ 6∈ T −φ.
.
(T −6): Suppose φ ≡ ψ. Then we have by Lemma 2 (part 2) C φ (δ) = C ψ (δ) for
.
any δ and we have by Lemma 1 (part 3) φ ' ψ. Then according to Definition 2, T −φ
.
and T −ψ can not be different.
. .
(T −cr): Suppose ψ ∈ T and σ ∈ C φ (ψ) is such that σ ∈ T −φ. If φ 6∈ T or ` φ
.
then ψ ∈ T −φ follows immediately from Definition 2. So suppose φ ∈ T and 6` φ. By
.
Definition 2, σ ∈ T −φ implies that σ ∈ T and there is δ ∈ C φ (σ) such that φ < δ.
Since σ ∈ C φ (ψ) we have by Lemma 2 (part 3) that C φ (σ) ⊆ C φ (ψ). Thus δ ∈ C φ (ψ).
.
It then follows from φ < δ and Definition 2 that ψ ∈ T −φ.
t
u
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 frame-
work. It captures the sufficient condition for retaining an axiom in our reformulated
mechanism.
( ) ( )
AvC BvD BvC
< <
CvD BvA AvD
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 [3,4], a set of axioms S must contain
B v A and C v D for S 6` B v D and {A v C} ∪ S ` B v D. Thus we have
C BvD (A v C) = {B v C, A v D, A v ¬B, B v D, A v C}. Since both B v C
and A v D are strictly more entrenched than B v D, A v C is retained. It is easy to
see the retained axioms do not entail B v D. Moreover, since C v D together with
B v C entails B v D and also B v A together with A v D, the removal of C v D
and B v A are necessary.
Notice that although we allow conjunction of axioms, we do not have to check for
. . .
their retainments. It follows from (T −1) that φ ∧ ψ ∈ T −δ if and only if φ ∈ T −δ
.
and ψ ∈ 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 σ ∈ C φ (ψ) do
4 if φ < σ then
5 Tφ− := Tφ− ∪ {ψ};
6 break;
7 return Tφ− ;
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 Related Work
In dealing with changes over DL ontologies, many [7,8,18,23,22,19,20,24] have taken
the same strategy as ours by considering it as a belief change problem. Instead of focus-
ing on contraction, [18,23] defined specific revision operators for incorporating new ax-
ioms. [22,19,20] studied both contraction and revision but over TBoxes and knowledge
bases that are not necessarily closed. This means only the axioms explicitly presented
in the TBox or knowledge base are considered. The implicit axioms which logically
follow from the explicit ones but are not presented are discarded during the operation.
Thus the logical contents are not maximally preserved during the operation as we did by
considering logically closed TBoxes. [24] works with logically closed TBoxes and pro-
vides a model-theoretic approach for both contraction and revision under DL-Litecore .
Axiom negation is not supported by most DLs but is required in defining some belief
change operations. [8] proposed several notions of negated axioms for DLs. They also
explored the notions of inconsistent and incoherent TBoxes.
In a more general setting, [7,21] identified properties of a monotonic logic under
which a contraction function can be defined that satisfies the postulates of Recovery
[1] and Relevance [14] respectively. By their results, it is possible to define DL-Lite
contraction functions that satisfy Relevance.
[13] studied operations that contract and revise at the same time. A constraint which
states the set of axioms to be incorporated and those to be eliminated is first specified.
Then the operation maps a knowledge base to another that satisfies the constraint. The
operation reduces to a revision and contraction after making empty the eliminating set
and the incorporating set respectively.
[12,6,15,16] also dealt with changes over DL-Lite ontologies. Instead of considering
it as a belief change problem, they focus on issues with expressibility of the outcomes
for model-based change operations.
5 Conclusion
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 guar-
antee 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.
References
1. Alchourrón, C.E., Gärdenfors, P., Makinson, D.: On the logic of theory change: Partial meet
contraction and revision functions. The Journal of Symbolic Logic 50(2), 510–530 (1985)
2. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The De-
scription Logic Handbook. CUP, Cambridge, UK (2003)
3. Borgida, A., Calvanese, D., Rodriguez-Muro, M.: Explanation in dl-lite. In: Proceedings of
the 21st Int. Workshop on Description Logics (DL-2008) (2008)
4. Borgida, A., Calvanese, D., Rodriguez-Muro, M.: Explanation in the dl-lite family of de-
scription logics. In: Proceedings of the 7th Int. Conf. on Ontologies, DataBases, and Appli-
cations of Semantics (ODBASE-2008). pp. 1440–1457 (2008)
5. Calvanese, D., Giacomo, G.D., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning
and efficient query answering in description logics: The DL-Lite family. Journal of Auto-
matic Reasoning 39(3), 385–429 (2007)
6. Calvanese, D., Kharlamov, E., Nutt, W., Zheleznyakov, D.: Evolution of dl-lite knowledge
bases. In: Proceedings of the 9th International Semantic Web Conference on The Semantic
Web (ISWC-2010). pp. 112–128. ISWC’10 (2010)
7. Flouris, G., Plexousakis, D., Antoniou, G.: Generalizing the AGM postulates: prelimi-
nary results and applications. In: Proceedings of the 10th International Workshop on Non-
Monotonic Reasoning (NMR-2004). pp. 171–179 (2004)
8. Flouris, G., Huang, Z., Pan, J.Z., Plexousakis, D., Wache, H.: Inconsistencies, negations
and changes in ontologies. In: Proceedings of the 21st National Concference on Artificial
Intelligence (AAAI-2006) (2006)
9. Gärdenfors, P.: Knowledge in Flux: Modelling the Dynamics of Epistemic States. MIT Press
(1988)
10. Gärdenfors, P., Makinson, D.: Revisions of knowledge systems using epistemic entrench-
ment. In: Proceedings of the 2nd conference on Theoretical Aspects of Reasoning about
Knowledge (TARK-1988). pp. 83–95 (1988)
11. Gärdenfors, P., Rott, H.: Belief revision. In: Handbook of Logic in AI and LP, vol. 4. OUP
(1995)
12. Giacomo, G.D., Lenzerini, M., Poggi, A., Rosati, R.: On instance-level update and erasure
in description logic ontologies. Journal of Logic Computation 19(5), 745–770 (2009)
13. Grau, B.C., Ruiz, E.J., Kharlamov, E., Zhelenyakov, D.: Ontology evolution under semantic
constraints. In: Proceedings of the 13th International Conference on Principles of Knowledge
Representation and Reasoning (KR-2012). pp. 137–147 (2012)
14. Hansson, S.O.: Belief Contraction Without Recovery. Studia Logica 50(2), 251–260 (1991)
15. Kharlamov, E., Zheleznyakov, D.: Capturing instance level ontology evolution for dl-lite. In:
Proceedings of the 10th International Conference on The Semantic Web (ISWC-2011). pp.
321–337 (2011)
16. Kharlamov, E., Zheleznyakov, D., Calvanese, D.: Capturing model-based ontology evolution
at the instance level: The case of dl-lite. Journal of Computer and System Sciences 79(6),
835–872 (2013)
17. Pan, J.Z., Thomas, E.: Approximating owl-dl ontologies. In: Proceedings of the 22nd Na-
tional Conference on Artificial Intelligence (AAAI-2007). pp. 1434–1439 (2007)
18. Qi, G., Du, J.: Model-based revision operators for terminologies in description logics. In:
Proc. IJCAI-2009. pp. 891–897 (2009)
19. Qi, G., Haase, P., Huang, Z., Ji, Q., Pan, J.Z., Vlker, J.: A kernel revision operator for termi-
nologies algorithms and evaluation. In: Proceedings of the 7th International Semantic Web
Conference, (ISWC-2008). pp. 419–434 (2008)
20. Ribeiro, M.M., Wassermann, R.: Base revision for ontology debugging. Journal of Logic
Computation 19(5), 721–743 (2009)
21. Ribeiro, M.M., Wassermann, R., Flouris, G., Antoniou, G.: Minimal change: Relevance and
recovery revisited. Artificial Intelligence 201, 59–80 (2013)
22. Ribeiro, M.M., Wassermann, R.: First step towards revising ontologies. In: Proc. WONTO-
2006 (2006)
23. Wang, Z., Wang, K., Topor, R.: A new approach to knowledge base revision in dl-lite. In:
Proc. AAAI-2010 (2010)
24. Zhuang, Z., Wang, Z., Wang, K., Qi, G.: Contraction and revision over dl-lite tboxes. In:
Proceedings of the 28th AAAI Conference (AAAI-2014) (2014)