=Paper=
{{Paper
|id=Vol-1193/paper_39
|storemode=property
|title=Instance-driven TBox Revision in DL-Lite
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_39.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/WangWQZL14
}}
==Instance-driven TBox Revision in DL-Lite==
https://ceur-ws.org/Vol-1193/paper_39.pdf
Instance-driven TBox Revision in DL-Lite
Zhe Wang1 , Kewen Wang1 , Guilin Qi2 , Zhiqiang Zhuang1 , and Yuefeng Li3
1
School of ICT, Griffith University, Australia
2
School of CSE, Southeast University, China
3
School of EECS, Queensland University of Technology, Australia
Abstract. The development and maintenance of large and complex ontologies
are often time-consuming and error-prone. Thus, automated ontology learning
and revision have attracted intensive research interest. In data-centric applica-
tions where ontologies are designed or automatically learnt from the data, when
new data instances are added that contradict to the ontology, it is often desirable
to incrementally revise the ontology according to the added data. This problem
can be intuitively formulated as the problem of revising a TBox by an ABox. In
this paper we introduce a model-theoretic approach to such an ontology revision
problem by using a novel alternative semantic characterisation of DL-Lite ontolo-
gies. We show some desired properties for our ontology revision. We have also
developed an algorithm for reasoning with the ontology revision without comput-
ing the revision result. The algorithm is efficient as its computational complexity
is in coNP in the worst case and in PT IME when the size of the new data is
bounded.
1 Introduction
A large number of professional and comprehensive ontologies have been developed for
accessing data, including the SNOMED CT [23] and the NCI ontologies [9]. The Web
Ontology Language (OWL), with its latest version, OWL 2 , is accepted as the WWW
Consortium (W3C) recommendation for ontology languages. OWL and OWL 2 are
based on description logics (DLs) [2]. Three profiles of OWL 2 are proposed, namely
EL, QL and RL , which are based on fine-tuned DLs for efficient reasoning.
Existing large ontologies like SNOMED CT are mostly hand-crafted by human
experts. The development and maintenance of such large ontologies are often time-
consuming and error-prone. Recently, automated ontology learning [3, 15, 13] and re-
vision [19, 18, 20, 17, 25, 26] have attracted intensive interest. Although it is often con-
ceived that ontologies, once established, are more stable and reliable than data, auto-
mated ontology crafting and revision are especially useful in data-centric applications
and for pre-mature ontologies. A typical scenario is ontology learning, where termino-
logical relations are learnt from example data provided by domain experts, which in
DL terms is learning TBox axioms from ABox assertions. Several TBox learning ap-
proaches have been proposed in the literature and effective learning tools have been de-
veloped [15]. An obvious requirement in ontology learning is that the learnt ontologies
must be consistent with the example data. However, when new data instances become
available, it is possible that the new data may contradict some previously learnt axioms.
Obviously, when the size(s) of the ontology and/or the data is large, it is undesirable
to re-learn the ontology from the scratch. Thus, a challenge is how to revise the ontol-
ogy according to the new data. In DLs, it amounts to the question of how to effectively
revise a TBox by an ABox.
TBox debugging and repair approaches [11, 22, 10] and interactive revision ap-
proaches [16] can be used to pinpoint the problematic axioms, and most of TBox
repair approaches seek to eliminate a minimal number of axioms to restore consis-
tency. Similar syntax-based approach was adopted in revision [8, 18, 20]. However,
most syntax-based approaches to TBox revision lack of a suitable semantic justifica-
tion, which is partially reflected in their inability of preserving implicit knowledge. For
example, given T = {Bird v CanFly, Mammal v ¬CanFly}, the revision of T by
A = {CanFly(bat), Mammal(bat)} using syntax-based approaches in [8, 20] will dis-
card implicit information Bird v ¬Mammal, though it does not involve in the contra-
diction. To resolve this issue, some more recent works, such as [5, 6], advocate to define
syntax-based ontology revision on the deductive closure cl(T ) of the initial TBox T in-
stead of T itself. This of course relies on the finiteness of the deductive closure (with the
exception of some special cases), and there may not exist a unique optimal solution to
syntax-based revision [5], since often multiple minimal sets of axioms in T (or cl(T ))
exist that are responsible for the contradictions.
Seeing the TBox as a formalisation of the conceptual model of the data, which is a
common perspective in ontology learning, the TBox essentially represents a collection
of possible DL models. Taking this perspective, one can argue that in TBox revision,
it is critical to ensure minimal changes to the prospective models. Extant model-based
TBox revision literature only cover the revision by TBox axioms [17, 26]. In this paper,
we develop a novel approach to revise a TBox by ABox assertions, and to full-fill the
minimal change principle in a model-theoretic manner. To the best of our knowledge, it
is the first work on this direction. However, as witnessed by previous model-based TBox
revision approaches, working directly with classical DL models is difficult. Thus, we
introduce the type semantics for DL-Litecore , which is the core logic underlying OWL
2 QL. We provide a concrete TBox revision operator based on types. We show that our
operator possess desired properties. In particular, our operator supports revision of ax-
ioms, and the result of revision is uniquely defined which eliminates non-determinism.
For the computational aspects, we transform the entailment problem of TBox revision in
DL-Lite into one in propositional logic. We show that entailment checking and revision
computation can be done efficiently, and in particular, do not shift the corresponding
complexity in propositional logic.
2 Preliminaries
A signature S is a union of three disjoint (possibly infinite) sets SC , SR , and SI , where
SC is the set of atomic concepts, SR is the set of atomic roles, and SI is the set of
individual names. Concepts and roles in DL-Litecore and DL-LiteR are built on atomic
ones as follows [4]:
B → A | ∃R C → B | ¬B | ⊥ R → P | P−
where A ∈ SC and P ∈ SR . B is a basic concept, C is a general concept, and R
is a basic role. In what follows, we often use A for an atomic concept, B for a basic
concept, C for a general concepts, P for an atomic role, and R for a basic role. B and
R denotes the sets of basic concepts and basic roles over S, respectively. We write R−
for P if R = P − ; and R+ for P , whenever R = P or R = P − . A DL-Litecore TBox is
a finite set of concept inclusions or axiom of the form B v C. An ABox is a finite set
of concept assertions of the form A(a) and role assertions of the form P (a, b), where
a, b ∈ SI . For the convenience of presentation, we sometimes write P − (a, b) ∈ A
meaning P (b, a) ∈ A. A knowledge base (KB) K = T ∪ A consists of a TBox T and
an ABox A. In this paper, an ontology is a DL-Lite TBox.
The semantics of DL-Litecore is defined as usual using interpretations I = (∆I , ·I ),
and we refer to [4] for the details. An interpretation I satisfies inclusion B v C if
B I ⊆ C I ; I satisfies assertion A(a) if aI ∈ AI ; and I satisfies assertion P (a, b)
if (aI , bI ) ∈ P I . I satisfies TBox T (or ABox A) if I satisfies each inclusion in T
(resp., each assertion in A). I is a model of T (A, or T ∪ A) if I satisfies T (resp., A,
or both T and A). T ∪ A is consistent if it has at least one model. We also say that T
is consistent with A. A concept or role E is satisfiable w.r.t. T if a model I of T exists
such that E I 6= ∅; otherwise, E is unsatisfiable. T is coherent if all atomic concepts
and atomic roles in T are satisfiable. T ∪ A entails an inclusion or assertion α, written
T ∪ A |= α, if all models of T ∪ A satisfy α. Two KBs K1 , K2 are equivalent, written
K1 ≡ K2 , if they have the same models.
3 Type Semantics
To revise a TBox T by an ABox A, the result of revision should be a new TBox T 0 , such
that T 0 is consistent with A and that T 0 preserves as much terminological knowledge
as possible from T . We address TBox revision and minimal change from a model-
theoretic perspective, that is, the models of the result of revision can be obtained from
the models of the initial TBox with minimal change. To achieve this, we adapt classical
model-based belief revision to DL-Lite, which measures change through a notion of
model distance. However, DL models may have complex structures and the number of
models is always infinite. This makes it hard to handle TBox revision directly through
classical DL models. Hence, we introduce a new relation of satisfaction for DL-Litecore
TBoxes based on the notion of types [14]. Such an alternative semantic characterisation
use structures that are finite and much simpler than classical DL models.
In TBox revision, it suffices to consider a finite signature S that covers the initial
TBox and the new data. In this case, B and R are both finite. Formally, a type τ ⊆ B
is a (possibly empty) set of basic concepts. The satisfaction relation between a type τ
and a TBox T (or concept C) can be defined in the propositional manner, seeing τ as a
propositional interpretation (with basic concepts seen as propositional atoms) and T (or
C) as a propositional theory. P M (T ) (P M (C)) denotes the set of types corresponding
to the propositional models of T (C). When T = {B v C} is a singleton, we also write
P M (B v C). However, classical relation of satisfaction is insufficient and we need to
introduce a refined definition of satisfaction. For example, let T = {∃P v ⊥}, then
T |= ∃P − v ⊥. Yet P M (T ) 6⊆ P M (∃P − v ⊥), witnessed by the type τ = {∃P − }.
For a well defined semantics, one would expect that the models of T are also models
of ∃P − v ⊥. Hence, the refined satisfaction relation needs to take care of the non-
propositional inference that ∃R v ⊥ implies ∃R− v ⊥ for any R ∈ R, and we
will show that this is the only non-propositional inference needing special care in DL-
Litecore . In [14, 25], this problem is remedied using a set of types (instead of a single
type) in a model. However, the cost of using arbitrary sets of types as in [25] is an
exponential blow up on the sizes of models. Although simpler (in particular polynomial-
sized) models are defined in [14], the model structures are still rather complex. In what
follows, we present a more succinct characterisation, the type semantics, and we will
extend the type semantics to ABoxes.
Definition 1. A type τ satisfies a DL-Litecore TBox T if the following conditions hold:
1. τ ∈ P M (T ).
2. if T |= ∃R v ⊥ then ∃R− 6∈ τ .
In this case, τ is a type model (T-model) of T . The set of T-models of T is denoted as
T M (T ).
Again, we write T M (B v C) for a singleton TBox T = {B v C}.
T-models can be used to characterise the semantics of DL-Litecore TBoxes, and
major reasoning problems such as concept satisfiability and subsumption w.r.t. TBoxes
can be characterised using T-models.
Proposition 1. Given a DL-Litecore TBox T , the following results hold:
1. T is consistent iff there exists a T-model of T .
2. For a concept C, C is satisfiable w.r.t. T iff T M (T ) ∩ P M (C) 6= ∅.
3. For an inclusion B v C, T |= B v C iff T M (T ) ⊆ T M (B v C).
4. For a DL-Litecore TBox T 0 , T ≡ T 0 iff T M (T ) = T M (T 0 ).
To prove this proposition, we first show a connection between the classical DL
models and the type models of a TBox. Each DL interpretation I and each element d
in the domain of I determines a unique type, i.e., τdI = {B ∈ B | d ∈ B I }. We call τdI
the type of d in I.
Lemma 1. Given a DL-Litecore TBox T and a DL interpretation I, I is a model of T
iff τdI ∈ T M (T ) for each d ∈ ∆I .
Lemma 1 shows for each DL interpretation I, a set M of types can be determined
by I, and I is a model of some DL-Litecore TBox if and only if each element of M is
a T-model of the TBox. The following lemma shows the converse is also true—given a
T-model τ of a TBox T , a DL model of T can be constructed from τ .
Lemma 2. Given a DL-Litecore TBox T and a T-model τ of T , there exists a DL model
I of T and a domain element d ∈ ∆I such that τdI = τ .
From Lemmas 1 and 2, we can prove Proposition 1.
Proposition 1 shows that T-models capture the semantics of DL-Litecore TBoxes.
In order to define the revision of a TBox by an ABox, our type semantics needs to
define also (partially) the interpretations on the ABox, that is, we need to define which
types constitute to the rational interpretations of the ABox. While type semantics cannot
completely capture the semantics of ABoxes, due to the fact that types do not refer
to individual names, we can define the “type-models” of an ABox A as those types
determined by the models of A.
As in the definition of interpretation-determined types, where each element in an
interpretation uniquely determines a type, each named individual b in A and each in-
terpretation I of A uniquely determines a type τbI = {B ∈ B | bI ∈ B I }. As there
are often multiple models of A, b is associated with multiple types in A. Formally, type
τ is an instance type of b (or a b-type) in A iff it is the type of bI in some model I
of A. Intuitively, a b-type in A is the set of basic concepts to whom b is interpreted
as a member by some model of A. For example, given A = {A(b), P (b, c)}, type
τ = {A, ∃P } is a b-type but not a c-type in A. This is because there exists a model
I of A (e.g., the model obtained by seeing A as a complete interpretation) such that
τbI = τ ; and for each model I of A, cI ∈ (∃P − )I but ∃P − 6∈ τ . Let T M (b, A) be
the set consisting
S of all the b-types in A. T M (A) is the set of instance types in A, i.e.,
T M (A) = b occurs in A T M (b, A).
The following proposition says that a TBox T is consistent with an ABox A iff for
each individual b occurring in A, there exists a T-model of T that is a b-type.
Proposition 2. Given a TBox T and an ABox A in DL-Litecore , T ∪ A is consistent iff
T M (T ) ∩ T M (b, A) 6= ∅ for each individual b occurring in A.
Without conjunction and disjunction, DL-Litecore cannot capture the full proposi-
tional logic. As a result, given a set M of types, M is not always expressible by DL-
Litecore TBoxes, i.e., M may not be the set of T-models of any DL-Litecore TBox. Also,
the set of T-models of a DL-Litecore TBox T needs to be role balanced. Formally, a set
of types is called role balanced if it includes a type containing ∃R whenever it includes
a type containing ∃R− for all R ∈ R.
Proposition 3. T M (T ) is role balanced for each DL-Litecore TBox T .
For a given set M of types, we define a corresponding TBox for M to be one that
has the minimal set of T-models that includes M . Formally, a DL-Litecore TBox T is
a corresponding TBox to M if M ⊆ T M (T ) and there is no DL-Litecore TBox T 0
such that M ⊆ T M (T 0 ) ⊂ T M (T ). Tcore (M ) denotes a corresponding TBox for
M . The corresponding TBoxes are not unique in general, as intuitively often multiple
role-balanced minimal supersets exist. For example, suppose M consists of only one
type τ = {∃P }. There are two corresponding TBoxes for M that are {∃P − v ∃P }
and {∃P − v ¬∃P }, with the T-models (other than τ ) {∃P, ∃P − } and {∃P − }, re-
spectively. Intuitively, Definition 1 enforces that a corresponding TBox T of M cannot
infer ∃P − v ⊥, and a DL model of T must instantiate ∃P − with at least one mem-
ber e. The above two TBoxes correspond to the cases where e is and is not a member
of ∃P , respectively. The following proposition shows that role-balance guarantees the
uniqueness.
Proposition 4. Each role balanced set of types has a unique corresponding TBox (up
to semantic equivalence).
When a unique corresponding TBox exists, the TBox has the same set of logical
consequences in DL-Litecore as the set of types.
Lemma 3. Let M be a role balanced set of types and T be its unique corresponding
TBox. For each inclusion B v C, M ⊆ P M (B v C) iff T |= B v C.
4 TBox Revision
In this section, we use our new semantic characterisation to define a specific TBox
revision operator. In classical model-based revision, to revise a propositional knowl-
edge base φ by a propositional formula ψ, it is sufficient to select the models of ψ that
have minimal distances to those of φ, and to define the propositional knowledge base
corresponding to the selected models to be the result of revision. Inspired by classical
model-based revision, we first introduce a notion of distance between T-models, and
then define a selection function that selects from a set of types those types having min-
imal distances to the T-models of the initial TBox. As we will see later, however, a
simple adoption of the classical approach to DL-Lite is insufficient to ensure the result
of revision has desired properties. We present our novel revision approach tailored for
instance-driven TBox revision applications.
We adopt a prominent notion of model distance in classical model-based revision
introduced by Satoh [21], where the distance between two propositional models (seen
as sets of propositional atoms) is defined as the symmetric difference between the
two models. The distance between two types τ and τ 0 is their symmetric difference
sd(τ, τ 0 ) = (τ \ τ 0 ) ∪ (τ 0 \ τ ). Intuitively, a pair of types τ1 , τ10 are considered to
be (strictly) closer than another pair τ2 , τ20 if sd(τ1 , τ10 ) ⊂ sd(τ2 , τ20 ). While we adopt
Satoh’s distance, we note that other notions of distance can also be applied in our re-
vision framework. Further, given two sets M and M 0 of types, a selection function γ
selects the types in M that are closest to those in M 0 , based on the notion of distance.
In particular,
γ(M, M 0 ) = {τ0 ∈ M | τ00 ∈ M 0 exists s.t.
for all τ ∈ M and τ 0 ∈ M 0 , sd(τ, τ 0 ) 6⊂ sd(τ0 , τ00 )}
For a TBox T and an ABox A, we could define the revision of T by A to be a TBox
corresponding to γ(T M (A), T M (T )), as a straightforward adoption of Satoh’s model-
based revision to DL-Lite. However, a result of revision defined in this manner may not
be coherent, and moreover, the result of revision is not guaranteed to be consistent with
the ABox A. For example, let T = {A v B, A v ¬B} and A = {A(b), B(c)}. Then,
γ(T M (A), T M (T )) = T M (A) ∩ T M (T ) consists of a single type {B}. The corre-
sponding TBox {A v ⊥} is incoherent and is inconsistent with A. Note that from the
above example, to achieve coherence and to ensure consistency with the ABox are not
necessarily two separate goals. That is, in many cases like T , the TBox is inconsistent
with the ABox because it is incoherent. Hence, if the inconsistency is caused by an un-
satisfiable concept or role, then both consistency between the TBox and the ABox and
the coherence of the TBox can be recovered simultaneously by revising only the TBox
(without changing the ABox). To this end, we introduce the coherence closure A∗ of
an ABox A, which extends A with A(cA ) for each A ∈ SC such that no assertion A(a)
occurs in A, where cA is a fresh individual name not occurring in A, and extends A
with P (cP , dP ) for each P ∈ SR such that no assertion P (a, b) occurs in A, where
cP , dP are fresh individual names not occurring in A. In the above example, A∗ = A.
Lemma 4. For a TBox T and an ABox A, T is coherent and T ∪ A is consistent iff
T ∪ A∗ is consistent.
The lemma show that the task of maintaining both the consistency of KB T ∪ A and
the coherence of TBox T can be reduced to that of maintaining only the consistency of
KB T ∪ A∗ .
If T ◦ A is the result of revising T by A, by Proposition 2, the consistency of KB
(T ◦ A) ∪ A∗ can be guaranteed by the condition T M (T ◦ A) ∩ T M (b, A∗ ) 6= ∅ for
each b occurring in A∗ , i.e., the set of T-models of T ◦A must contain at least one b-type
for each individual b in A∗ . It is clear that γ(T M (A∗ ), T M (T )) does not necessarily
satisfy this condition, as can be seen from the above example: There are two b-types
in A∗ , {A, B} and {A}, and γ(T M (A∗ ), T M (T )) = γ(T M (A), T M (T )) does not
contain either of them. Intuitively, for T ◦ A to be consistent with A∗ , the T-models of
T ◦ A needs to contain at least one of the b-types. In the example, both b-types have
the same distance to the T-models of T (types {B} and ∅) and both b-types should be
selected as T-models of T ◦ A. In general, for each individual b occurring in A∗ , the
b-types in A∗ that are closest to T M (T ) should be selected. Also, when T is already
coherent and is consistent with A, the revision operation should not change T . To this
end, all the initial T-models of T are also added as T-models of T ◦ A.
Based on the above intuitions, we define our TBox revision operator as follows.
Definition 2. Let T be a TBox and A be an ABox in DL-Litecore . The revision of T by
A is T ◦ A = Tcore (T M (T ) ∪ MA∗ ) where
[
MA∗ = γ(T M (b, A∗ ), T M (T )).
b occurs in A∗
Intuitively, MA∗ is constituted by, for each individual b occurring in A∗ , a set of b-types
that are closest to the T-models of T . MA∗ is constructed as such in order that the result
of revision is consistent with A∗ ; and the result of revising T by A is defined to be a
corresponding TBox of T M (T ) ∪ MA∗ . It is not hard to see that T M (T ) ∪ MA∗ is
role balanced: For each P ∈ SR , assertion P (b, c) occurs in A∗ for some b, c ∈ SI , and
as a result, a b-type containing ∃P and a c-type containing ∃P − are contained in MA∗ .
From Proposition 4, T ◦ A is uniquely defined (up to semantic equivalence).
Consider the following example adapted from the NCI ontology [9].
Example 1. Let TBox T consists of the following inclusions
Heart Disease v ∃has Site, (1)
−
∃has Site v Cardiovascular System, (2)
−
∃has Site v Respiratory System, (3)
Respiratory System v Organ System, (4)
Cardiovascular System v Organ System, (5)
Respiratory System v ¬Cardiovascular System, (6)
Heart Disease v ¬Organ System. (7)
The following two inclusions in the original NCI ontology are not DL-Litecore axioms
and thus they are replaced with inclusions (1)–(3) . While this is not a precise transla-
tion, it is sufficient to demonstrate the application of our new revision in handling such
medical ontologies.
Heart Disease v ∃has Site.Cardiovascular System,
Heart Disease v ∃has Site.Respiratory System.
The TBox T is incoherent, as both concept Heart Disease and role has Site are unsat-
isfiable.
Given A = {Heart Disease(hd1), has Site(hd1, s1), Organ System(s1)}. Then, by
Definition 2, T ◦ A consists of inclusions (1), (4)–(7), and the following inclusion
∃has Site− v Organ System. (8)
The inclusion (8) can be seen as a revision from axioms (2)–(5).
The example shows that our TBox revision operator allows modification of axioms, in
contrast to most existing TBox repair approaches that only support axiom removal.
Furthermore, the revision operator satisfies the following desired properties pre-
sented as AGM-style postulates [12]. Note that our revision operator is different from
the classical AGM ones in nature. The classical AGM approach concerns revision be-
tween propositional formulas of the same type, whereas our revision approach addresses
revising TBox axioms by ABox assertions, which is between different types of first-
order formulas. As a result, the following postulates are specially tailored for instance-
driven TBox revision.
Proposition 5. Let T be a TBox and A be an ABox in DL-Litecore . The following
properties hold.
(R1) T ◦ A is coherent.
(R2) (T ◦ A) ∪ A is consistent.
(R3) If T is coherent and T ∪ A is consistent, then T ◦ A ≡ T .
(R4) If T1 ≡ T2 and A1 ≡ A2 , then T1 ◦ A1 ≡ T2 ◦ A2 .
The first two properties (R1) and (R2) show that the result of revision is coherent and
is consistent with the new ABox as required. Then, (R3) says that no revision is needed
if the initial TBox is already coherent and consistent with the new ABox. Finally, (R4)
shows that the revision operator is syntax-independent, i.e., revising equivalent TBoxes
with equivalent new ABoxes results in equivalent revision.
5 Computational Aspects
In this section, we first look into the computational complexity of the entailment prob-
lem for revision, i.e., the problem of deciding whether T ◦A entails a given TBox axiom
B v C. We show that the entailment can be checked without first computing T ◦ A,
and is achieved through a reduction to propositional logic. After that, we will provide
an algorithm to compute T ◦ A through entailment checking. We show that when the
size of A is bounded, the computation can be done in polynomial time.
We first show that the entailment problem in DL-Lite can be reduced to one in
propositional logic. To this end, we introduce a propositional transformation for DL-
Lite TBoxes. This allows us to build essentially a connection between our revision
operator and propositional belief revision, and to make use of the existing belief revision
results and algorithms in propositional logics, e.g., [7]. The transformation is inspired
by [1], which introduces a transformation from a DL-Lite TBox into a theory in the
one variable fragment of first order logic. Using type semantics instead of classical DL
models allows us to obtain a novel transformation to propositional logic, which is much
simpler than theirs.
To achieve this, each basic concept in B is assigned a distinct propositional atom,
each A to pA and each ∃R to p∃R . Function φ(·) maps each basic concept in B to its
corresponding propositional atom, and a general concept to a propositional literal as
follows.
φ(⊥) = ⊥, φ(A) = pA , φ(∃R) = p∃R , φ(¬B) = ¬φ(B).
Then, φ(·) can be extended to map a DL-Litecore TBox T to a propositional formula
as follows
^ ^
¬φ(∃R) ∧ ¬φ(∃R− ) .
φ(T ) = φ(B) → φ(C) ∧
BvC∈T R∈R,T |=∃Rv⊥
Further, to encode the instance types of an ABox, a pair of a DL-Litecore ABox
A and an individual name b occurring in A is mapped to a propositional formula as
follows.
^ ^ ^
φ(b, A) = φ(A) ∧ φ(∃P ) ∧ φ(∃P − )
A(b)∈A P (b,c)∈A P (c,b)∈A
Note that the mapping does not translate an ABox into a propositional formula. Instead,
formula φ(b, A) is used to capture the b-types in A. Intuitively, the models of φ(T )
correspond to the T-models of T , and the models of φ(b, A) correspond to the b-types
in A, as shown in the following lemma. Let ωτ = {φ(B) | B ∈ τ } for a type τ . mod(φ)
denotes the set of models of propositional formula φ.
Lemma 5. Let T be a TBox and A be an ABox in DL-Litecore . Then,
1. mod(φ(T )) = {ωτ | τ ∈ T M (T )};
2. mod(φ(b, A)) = {ωτ | τ ∈ T M (b, A)}.
Let ◦s be Satoh’s revision operator in propositional logic. The following connection
between our revision operator and Satoh’s holds.
Proposition 6. Let T be a TBox andWA be an ABox in DL-Litecore . Given a TBox axiom
B v C, T ◦A |= B v C iff φ(T )∨ b occurs in A∗ φ(T )◦s φ(b, A∗ ) ` φ(B) → φ(C).
Proposition 6 allows us to reduce the entailment problem in DL-Litecore to a corre-
sponding problem in propositional logic, and thus to make use of existing complexity
results for propositional revision. Note that φ(T ) and φ(b, A) are both Horn proposi-
tional formulas, and the sizes of them are polynomial in the size of T ∪ A. From the
complexity results in [7], it is easy to conclude the following complexity results. In par-
ticular, our TBox revision operator for DL-Litecore does not shift the complexity of the
propositional case.
Theorem 1. For a TBox T , an ABox A, and a TBox axiom B v C in DL-Litecore ,
deciding T ◦ A |= B v C is in coNP.
If the size of A is bounded, i.e., a constant k exists s.t. |A| ≤ k, then deciding
T ◦ A |= B v C is in PT IME.
The coNP upper bound is not necessarily tight, but mainly shows the connection of
our revision operator with the propositional ones. We leave a tight complexity result
for the entailment problem in DL-Litecore (with inputs of unbounded sizes) open. Hav-
ing a bound on the size of A and the PT IME complexity are practically relevant, as
in ontology learning, the newly added example data is often small. The proof is not
straightforward as |A| being bounded does not necessarily implies that |A∗ | is bounded.
Indeed, the PT IME complexity result holds as long as the number of assertions about
each individual in A is bounded.
Algorithm 1: Revision
Input: TBox T and ABox A in DL-Litecore
Output: a DL-Litecore TBox T 0
T 0 := ∅;
foreach B1 , B2 ∈ B s.t. B1 6= B2 do
if T ◦ A |= B1 v B2 then
T 0 := T 0 ∪ {B1 v B2 } ;
end
if T ◦ A |= B1 v ¬B2 then
T 0 := T 0 ∪ {B1 v ¬B2 } ;
end
end
return T 0 ;
We provide an algorithm to compute T ◦ A using entailment checking as a sub-
method. The algorithm verifies each possible entailment and add those entailed axioms
to the result.
Proposition 7. Let T be a TBox, A be an ABox in DL-Litecore , and T 0 be the TBox
returned by the algorithm Revision. Then, T 0 ≡ T ◦ A.
Although DL-Lite ontologies are often associated with large ABoxes, the input ABox
A consists of only updated data and thus can be expected to be small. If the size of A
is bounded, the algorithm Revision runs in PT IME in the size of T ∪ A. In particular,
the number of possible inclusions in DL-Litecore is quadratic to the number of basic
concepts in T ∪ A, and the entailment check is in PT IME as discussed.
6 Conclusion
We have presented a novel approach to revise a DL-Lite TBox according to newly
added ABox instances, and the revision incurs only minimal change to the initial TBox
measured in a model-theoretic manner. To the best of our knowledge, our work is the
first attempt to address particularly the revision of a TBox by ABox assertions. To tackle
this problem, we have introduced the type semantics for DL-Litecore TBoxes, which is
superior over the classical DL semantics in that each TBox has a finite number of type
models and the new semantics still preserves most of major reasoning forms for DLs.
Based on this new semantics, we have developed an operator for revising a TBox by an
ABox. We show that the proposed revision operator possesses several desired properties
and have also developed an efficient algorithm for computing the revision.
We are currently working on extending our approach to DL-LiteR . To address this
issue, a key task is to extend the type semantics to DL-LiteR , which needs to take into
account the additional non-propositional inferences introduced by role inclusions. It
would be also interesting to look into practical applications of our revision approach in
ontology learning.
References
1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and re-
lations. Journal of Artificial Intelligence Research 36, 1–69 (2009)
2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.: The Descrip-
tion Logic Handbook. Cambridge University Press (2003)
3. Baader, F., Ganter, B., Sertkaya, B., Sattler, U.: Completing description logic knowledge
bases using formal concept analysis. In: Proceedings of the 20th International Joint Confer-
ence on Artificial Intelligence (IJCAI-07). pp. 230–235 (2007)
4. 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)
5. Calvanese, D., Kharlamov, E., Nutt, W., Zheleznyakov, D.: Evolution of DL-Lite knowledge
bases. In: Proceedings of the 9th International Semantic Web Conference (ISWC-10). pp.
112–128 (2010)
6. Cuenca Grau, B., 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-12). pp. 137–147 (2012)
7. Eiter, T., Gottlob, G.: On the complexity of propositional knowledge base revision, updates,
and counterfactuals. Artificial Intelligence 57, 227–270 (1992)
8. Haase, P., Stojanovic, L.: Consistent evolution of OWL ontologies. In: Proceedings of the
2nd European Semantic Web Conference (ESWC-05). pp. 182–197 (2005)
9. Hartel, F.W., de Coronado, S., Dionne, R., Fragoso, G., Golbeck, J.: Modeling a descrip-
tion logic vocabulary for cancer research. Journal of Biomedical Informatics 38(2), 114–129
(2005)
10. Horridge, M., Parsia, B., Sattler, U.: Laconic and precise justifications in OWL. In: Proceed-
ings of the 7th International Semantic Web Conference (ISWC-08). pp. 323–338 (2008)
11. Kalyanpur, A., Parsia, B., Sirin, E., Cuenca Grau, B.: Repairing unsatisfiable concepts in
OWL ontologies. In: Proceedings of the 3rd European Semantic Web Conference (ESWC-
06). pp. 170–184 (2006)
12. Katsuno, H., Mendelzon, A.: Propositional knowledge base revision and minimal change.
Artificial Intelligence 52(3), 263–294 (1991)
13. Konev, B., Lutz, C., Wolter, F.: Exact learning of tboxes in EL and DL-Lite. In: Informal
Proceedings of the 26th International Workshop on Description Logics (DL-13). pp. 341–
352 (2013)
14. Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and mod-
ule extraction, with an application to DL-Lite. Artificial Intelligence 174(15), 1093–1141
(2010)
15. Lehmann, J., Hitzler, P.: Concept learning in description logics using refinement operators.
Machine Learning 78(1-2), 203–250 (2010)
16. Nikitina, N., Rudolph, S., Glimm, B.: Interactive ontology revision. Journal of Web Seman-
tics 12, 118–130 (2012)
17. Qi, G., Du, J.: Model-based revision operators for terminologies in description logics. In:
Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI-09).
pp. 891–897 (2009)
18. Qi, G., Haase, P., Huang, Z., Ji, Q., Pan, J.Z., Völker, J.: A kernel revision operator for
terminologies - algorithms and evaluation. In: Proceedings of the 7th International Semantic
Web Conference (ISWC-08). pp. 419–434 (2008)
19. Qi, G., Yang, F.: A survey of revision approaches in description logics. In: Proceedings of
the 2nd International Conference of Web Reasoning and Rule Systems (RR-08). pp. 74–88
(2008)
20. Ribeiro, M.M., Wassermann, R.: Base revision for ontology debugging. Journal of Logic
Computation 19(5), 721–743 (2009)
21. Satoh, K.: Nonmonotonic reasoning by minimal belief revision. In: Proceedings of the Inter-
national Conference on Fifth Generation Computer Systems. pp. 455–462 (1988)
22. Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies.
Journal of Automated Reasoning 39(3), 317–349 (2007)
23. Spackman, K.A.: M. d. computing. SNOMED RT and SNOMED CT. Promise of an inter-
national clinical terminology 17(6), 29 (2000)
24. Staab, S., Studer, R. (eds.): Handbook on Ontologies. Springer-Verlag, 2. edn. (2009)
25. Wang, Z., Wang, K., Topor, R.: A new approach to knowledge base revision in DL-Lite.
In: Proceedings of the 24th National Conference on Artificial Intelligence (AAAI-10). pp.
369–374 (2010)
26. Zheleznyakov, D., Calvanese, D., Kharlamov, E., Nutt, W.: Updating TBoxes in DL-Lite. In:
Proceedings of the 23rd International Workshop on Description Logics (DL-10) (2010)