=Paper= {{Paper |id=Vol-2050/dew-paper3 |storemode=property |title=Local Change in Ontologies with Atomic Decomposition |pdfUrl=https://ceur-ws.org/Vol-2050/DEW_paper_3.pdf |volume=Vol-2050 |authors=Ricardo F. Guimarães,Renata Wassermann |dblpUrl=https://dblp.org/rec/conf/jowo/GuimaraesW17 }} ==Local Change in Ontologies with Atomic Decomposition == https://ceur-ws.org/Vol-2050/DEW_paper_3.pdf

Local Change in Ontologies with Atomic
Decomposition
Ricardo GUIMARÃES a,1 and Renata WASSERMANN a,2
a Institute of Mathematics and Statistics, University of São Paulo, Brasil

Abstract. When debugging big ontologies, it can be convenient to isolate the prob-
lematic behaviour so that only the relevant part of the ontology will be analysed
during the repair. Selecting relevant fragments from an ontology is exactly the sub-
ject of study in Ontology Modularisation, while the procedures to make proper
changes to parts of logical knowledge bases are the central point of the theory of
Local Change. Even though these areas are related by the notion of relevance, they
still have not been used in conjunction. Moreover, while Ontology Modularisation
approaches have been used in practice, the same did not occur with Local Change,
despite its concise formalization and potential to improve the computational effi-
ciency of change operations. Thus, in this work, we aim to devise a relevance met-
ric using atomic decomposition, originated in the field of Ontology Modularisa-
tion, and embed it into the framework of Local Change. As a result, we give the
first steps towards the construction of operations for localized change in descrip-
tion logic ontologies, which could be useful to make debugging procedures more
feasible for both ontology designers and computer programs.
Keywords. ontologies, ontology revision, ontology modularisation, local change,
atomic decomposition

1. Introduction

The use of ontologies for representing formal knowledge was stimulated by the creation
of the Semantic Web. Nowadays, many of these ontologies are written in OWL [1] or
OWL 2 [2] the ontological languages recommended by the W3C3 . One of the most inter-
esting features of these languages is that they have profiles whose formalism is founded
on the family of the Description Logics [3].
Description Logics are decidable fragments of first order logic, varying in expres-
siveness and computational complexity of the associated inference task. Given an ontol-
ogy, a user can obtain the logical consequences of the information described with the aid
of computer programs (called reasoners). Thus, in this work, we consider that ontologies
are codified as finite sets of axioms (or formulas) written in some Description Logic.
The task of repairing inconsistent knowledge bases is a complex one, since a re-
pair must also avoid introducing new inconsistencies or undesired consequences as well
as losing important information. Approaches in the literature, such as those based on
1 ricardof@ime.usp.br
2 renata@ime.usp.br
3 https://www.w3.org/
MUPS (Minimal Unsatisfiability-Preserving Sub-terminologies) and MUPS (Minimal
Incoherence-Preserving Sub-terminologies) [4], MinAs (Minimal Axiom sets) [5] and
justifications [6], exploit the logical foundations of ontologies to aid ontology repair.
Identifying errors and devising repairs can be even more problematic when dealing
with large ontologies, as there may be many axioms in the ontology that, albeit unrelated
to the undesired behaviour, are still considered by engineers and algorithms when trying
to find a repair.
In this sense, there are two research areas that can provide solutions to aid ontology
engineers and users on ontology debugging: Ontology Change [7,8,9,10] and Ontology
Modularisation [11,12,13]. The first is derived from the field of Belief Change [14] and
studies how one may change an ontology consistently by respecting certain rules (ratio-
nality postulates). Furthermore, works such as those from Flouris [7] and Ribeiro and
Wassermann [9], elucidate a strong connection between ontology change and ontology
debugging. Ontology Modularisation consists in identifying parts of the ontology that are
interesting for a given task, be it by extracting relevant fragments or by giving a structure
to the ontology.
The theory of Local Change [15], has similar motivations as those from the mod-
ularisation area: improve the efficiency of procedures when handling large sets of for-
mulas and also comply with the rationale that upon repair, the unrelated axioms should
be left as they are. In particular, Local Change presents a well-founded framework that
encompasses most of the Belief Base Change operations, allowing them to have their
localized (and probably more efficient) counterparts.
From the field of Ontology Modularisation, we employ Atomic Decomposition [16,
13] as an approach to represent the underlying structure of ontologies. This is due to its
conciseness and formal properties as we discuss briefly in Section 4.
Despite the elegant formalization and the interesting results, Local Change was not
implemented in real-world situations. In contrast, atomic decomposition was proposed
essentially to practical ends. In this sense, we aim to bring together strong results in
theory and practice to obtain an approach to ontology revision that has good logical
properties and is also computationally efficient.
Moreover, we formulate a relevance metric over axioms using the atomic decompo-
sition and derive from it localized operators of change for description logic ontologies.
The remaining of this paper is organized as follows: in Section 2 we present the
background related to the field of Ontology Change, discuss the Local Change approach
in Section 3 and the Atomic Decomposition in Section 4. Our approach is detailed in
Section 5. We mention related work in Section 6, while Section 7 contains our final
remarks, including future work.

Notation: We will denote a logic (or language) by L, a consequence (inference) op-
erator by Cn, sets of formulas (such as ontologies) by upper case latin letters (A, B, ...),
formulas (axioms) by lower case Greek letters (α, ϕ, ψ). Additionally, the set of non-
logical terms (the signature) of a formula ϕ is denoted by ϕe and the signature of a set of
formulas X by X.e Also, we consider the reader familiar with Description Logics and its
usual notation (for further details we refer the reader to [3]).
2. Ontology Change

In this work, by Ontology Change we mean the branch of Belief Change adapted to
ontologies [7,10]. The Belief Change field is concerned with the process by which a
rational agent modifies its current beliefs when it receives new information. The field was
born with the AGM theory [17], that is also the cornerstone of many other formalizations
in the area.
In the AGM theory, the beliefs of an agent are represented as a set of logical formu-
las, closed under an inference operation, the belief sets. Over these sets, the authors de-
fined three fundamental operations that take as input a belief set K and a formula ϕ: ex-
pansion (+), contraction (−) and revision (∗). Expansion corresponds to simply adding
ϕ to the beliefs of the agent, contraction implies a removal of ϕ from K and revision
represents the consistent addition of ϕ to K, potentially removing previous conflicting
beliefs. These operations were characterized by rationality postulates and mathematical
constructions equivalent to these postulates were provided [17].
The AGM theory for Belief Change presents a polished framework to represent an
agent beliefs, however, it has shortcomings when one aims to apply the operations pro-
posed to ontologies in Description Logics. The first issue is that the AGM theory consid-
ers sets closed under logical consequence (i.e ϕ ∈ X if and only if X ϕ), which is not
feasible in many situations, since those sets may not be even finitely representable (at
least for some logics), but also these sets are incompatible with our notion of ontologies,
seeing that a reasoner is needed to compute its deductive closure.
Notwithstanding, there is a variation of the AGM theory which handles sets formu-
las that are not necessarily closed by logical consequence: the Base Change theory as
proposed by Hansson [14]. The studies in this variant adapted the operations defined in
the AGM theory to belief bases (sets of formulas not closed under consequence), charac-
terized them by new sets of postulates and ultimately provided similar constructions that
are linked to these postulates by representation theorems.
Still, one of the principal operations of change, namely revision, imposed an issue
when dealing with Description Logics, because this operation required that the logic sat-
isfy the property of α-local non-contravention (if ¬α ∈ Cn(B ∪ {α}), then ¬α ∈ Cn(B))
and relied on the closure by classical negation. Some Description Logics do not satisfy
α-local non-contravention and others are not closed under negation at the axiom level,
for instance the meaning of a GCI’s negation is still not clearly defined [9,10].
To overcome these restrictions, Ribeiro and Wassermann [9] devised versions of
the operations of revision that required solely that the logic involved be monotonic and
compact. These new operations also manage effectively two distinct accounts of incon-
sistency in ontologies: the one that defines that an ontology is inconsistent if it implies
> v ⊥, and the one usually called incoherence [18] where any of the concept names is
unsatisfiable (for more details we refer the reader to [9,10]).
Hence, we now have a framework to manage change in description logic ontologies
that provides operations and constructions ruled by rationality postulates.

3. Local Change

Hansson and Wassermann [15] devised an approach to optimize the operations of Belief
Base Change by ruling out formulas that would not interfere in the result of the change
operation for a given input. This could improve the computational efficiency of these op-
erations, what can be crucial for agents with limited resources such as time and memory.
Besides, this relates to the idea that the axioms that are irrelevant for an input should be
ignored by a change operation.
To this end, they define a compartmentalization function (Definition 2) whose role is
to select from the belief base which formulas are relevant to a given input formula. This
function is built upon the notion of kernel as in Definition 1. In the ontology literature
kernels are also known as MinAs [5] and justifications [6], while MIPS and MUPS in [4]
consist in particular types of kernel.

Definition 1 (Kernel [19]). For all belief bases B ⊆ L and formulas ϕ ∈ L, X ∈ B ⊥
⊥ϕ
if and only if:
1. X ⊆ B
2. ϕ ∈ Cn(X)
3. for all Y , if Y ⊂ X, then ϕ 6∈ B
The elements of B ⊥
⊥ ϕ are called ϕ-kernels of B.

The compartments around a formula are composed of the ϕ-kernels and ¬ϕ-kernels,
excluding those that are inconsistent. This notion is formalized in Definition 2.

Definition 2 (Compartmentalization Function [15]). The A-compartment of B, where
A, B ⊆ L is defined as: c(A, B) = α∈A ( (((B ⊥ ⊥ α) ∪ (B ⊥⊥ ¬α)) \ (B ⊥
⊥ ⊥)))
S S

The function c is the compartmentalization function.

The compartmentalization is in turn employed to define localized consequence op-
erators as shown by Definition 3:

Definition 3 (A-localization [15]). Let C be an inference operation on L, and c be the
compartmentalization function as in Definition 2. Then for any set of formula A ⊆ L the
A-localization of C, denoted by CA (B), is the inference operation such that for all sets
B ⊆ L: CA (B) = C(c(A, B)).

The compartmentalization function has interesting motivations and its definition is
closely related to the area of Belief Revision (since the kernel sets were born in that field).
Despite that, it has a notable computational issue: since the compartments are defined
using kernel sets, calculating them is potentially as expensive as the application of the
original change operations. Furthermore, the definition of this function depends on the
classic negation of sentences, which is not well-defined for many Description Logics.
Nevertheless, Wassermann [20] remarks that most of the results in local change do
not depend on the compartmentalization function itself, but on the properties of the local
consequence operator obtained, in particular monotonicity and compactness.
Wassermann [20] then proposes different strategies to replace the compartments.
The initial idea is to define a relation between formulas, ideally to capture the notion
that: if ϕ is related to ψ, then ϕ is either in the proof of ψ or ¬ψ. Given such a relation
it is possible to define a path between formulas as in Definition 4.

Definition 4 ([20]). Given B a belief base and R a relation between formulas, a R-path
between ϕ and ψ in B is a sequence P = hϕi i0≤i≤n of formulas such that:
1. ϕ0 = ϕ and ϕn = ψ
2. {ϕi }1≤i≤n−1 ⊆ B
3. R(ϕi , ϕi+1 ) for 0 ≤ i < n in B.

If the relation R is irrelevant or clear from the context we simply talk about a path in
P
B. We denote that the P is a path between ϕ and ψ by: ϕ ψ. Additionally, the length
of a path P = hϕi i0≤i≤n is l(P) = n.

From a relation, it is possible to define a metric of “unrelatedness” between two
formulas as in Definition 5.

Definition 5 (Unrelatedness [20]). Let L be a language (logic), B ⊆ L a belief base, R
a relation between formulas of L and ϕ and ψ formulas of L. The unrelatedness degree
between ϕ and ψ is defined as:

if ϕ = ψ and ϕ ∈ B

 0,
P
u(ϕ, ψ) = min{l(P) | ϕ ψ}, if R(ϕ, ψ) in B

∞, otherwise

With this metric of unrelatedness one can generate a family of retrieval operators for
belief bases, which select the “most relevant” formulas for a given input.

Definition 6 ([20]). Let B ⊆ L be a belief base and α ∈ L a formula. Then we define the
following family of retrieval operators:
∆i (α, B) = {ϕ ∈ B | u(α, ϕ) = i}, for i ≥ 0.

Definition 7 ([20]). Let B ⊆ L be a belief base and α ∈ L a formula. Then we define the
following family of retrieval operators:
∆≤n (α, B) = 0≤i≤n ∆i for n ≥ 0.
S

Also, ∆ω (α, B) = i≥0 ∆i (α, B) denotes the set of relevant formulas for α.
S

The simplest relation presented in [20] is the following: R(ϕ, ψ) if and only if ϕ and
ψ share a non-logical term. In propositional logic, this would be equivalent to sharing a
propositional atom, in Description Logics this means that the formulas share a concept
name, role name or individual in their signatures.
To illustrate this method of structuring observe Example 8 which depicts an extract
of a possible ontology for electronic account management. On this sample setting, the
accounts are either chat accounts or e-commerce accounts, this last type of account corre-
sponds to those which have a payment method (such as credit cards) linked. Also, while
general users can have any type of account, stores are restricted to having e-commerce
ones.

Example 8. Consider the ontology B1 :
B = {α1 : User ≡ ∃hasAccount.Account,
α2 : Account ≡ EcommerceAccount t ChatAccount,
α3 : EcommerceAccount ≡ ∃hasPaymentMethod.PaymentMethod,
α4 : CreditCard v PaymentMethod,
α5 : StoreAccount v EcommerceAccount}

In Figure 8, we see the axioms structured as an undirected graph, where the edges
represent signature sharing, a symmetric relation.

α1 α2 α3

α5 α4

Figure 1. B1 structured using signature intersection

4. Atomic Decomposition

The problem of extracting relevant parts or identifying structure in ontologies motivated
studies in the field of Ontology Modularisation [11,13]. Even though there are numer-
ous approaches, some of them lack either logical properties or are too computationally
expensive to compute.
The syntactic locality-based modules (syntactic LBMs) [11] are arguably the most
successful strategy in this area. These modules have interesting logical properties and can
be computed in polynomial time even for ontologies in expressive Description Logics
such as SROIQ. Moreover, they are already implemented in the OWL API4 .
This modularisation strategy consists in selecting from the ontology all the axioms
that pass a verification of relevance for a set of terms. This verification is defined by
matching to syntactic rules.
There are many notions of syntactic locality, which differ in the definition of the
syntactic rules, however, from here onwards, we will restrict our attention to the three
most studied and implemented locality notions: >-locality, ⊥-locality and >⊥∗ -locality
as defined in [21].
Also, we remark that the locality-based module of the ontology B for the signature
Σ (denoted by MBΣ ), using any of the three aforementioned notions, are justification-
ϕe
preserving [11,21], in other words, each ϕ-kernel is a subset of MB .
The fact that locality-based modules preserve justifications gives an interesting re-
lation between ontology modularisation and ontology change, since it guarantees that
one could ignore all axioms outside the LBM for the input formula when verifying if an
ontology entails a given formula.
Del Vescovo [13] evaluates the ability of different modularity techniques in the liter-
ature to induce structure over ontologies. Besides the logical and computational aspects
4 http://owlapi.sourceforge.net/
of the strategies considered, Del Vescovo also studies them with respect to the number
of modules created and meaningfulness of the relations established between them.
However, even the locality-based modules fail in the latter aspect, as the only relation
among the modules is set inclusion (⊆), and to structure an ontology over this relation
one would need to compute all the LBMs in an ontology, and there can be a number of
them exponential on the size (number of axioms) of the ontology [22].
This exponential characteristic occurs because there are locality-based modules that
can be written as the union of two incomparable modules (w.r.t set inclusion, ⊆). Mod-
ules that are redundant in this sense are called fake, while the others are called genuine
modules. Thus, using simply the set inclusion is not sufficient to represent the ontology
structure concisely [16].
To overcome this issue, Del Vescovo [13] devises a concise representation of the set
of all syntactic locality-based modules of an ontology. The formalization of this repre-
sentation is reproduced in Definitions 9 to 11.

Definition 9 (Co-occurrence Equivalence Relation [13]). Let F(B) be the set of all
locality-based modules of an ontology B. The relation ≈ is the binary relation over B
defined to hold between two axioms α, β ∈ B if, for all M ∈ F(B), α ∈ M if and only if
β ∈ M.

Definition 10 (Atom [13]). Let B be an ontology and ≈ the co-occurrence relation be-
tween atoms. We define an atom a of B to be an equivalence class [α]≈ for an axiom
α ∈ B. The set of atoms of B is denoted by A(B).

Definition 11 (Dependency Between Atoms [13]). Let a and b be two atoms induced by
≈ over an ontology B. We say that a is dependent on b (denoted as a b) if, for every
module M ∈ F(B) such that a ⊆ M, we have b ⊆ M.

The relation of Definition 11 generates a partial order of the atoms in A(B). Hence,
the strict part of this relation, denoted by is a strict partial ordered set. Finally, the
atomic decomposition of an ontology B is defined as the pair: (A(B), ).
As illustration, consider again the ontology B1 from Example 8, its atomic decom-
position using >⊥∗ -locality as notion (i.e. the >⊥∗ -AD of B1 ) is shown in Figure 2.

α1

α5 α2

α3 α4

Figure 2. >⊥∗ -AD of B1

From Figure 2, we can notice some improvements when using the >⊥∗ -AD instead
of the signature intersection one. The first is that the dependency relation is more infor-
mative than simply saying that two formulas are related. Second, some relationships in
Figure 1 can be seen as irrelevant, for instance, the one between α3 and α4 : even though
they share a term in their signature, they are not necessary to prove one another (or their
α
respective negations), since: α3 6∈ MBα14 and α4 6∈ MB13 , as they are in disjoint components
f f

of the atomic decomposition.
Also, there are results which sustain the atomic decomposition as a succinct repre-
sentation of all modules in an ontology [13], in particular the number of axioms of an
ontology is an upper bound of the number of atoms in its atomic decomposition. To bet-
ter understand the relation between the atomic decomposition and the genuine modules
we need to define principal ideals of atoms (Definition 12).

Definition 12 (Principal Ideal of an Atom [13]). Let B be an ontology and (A(B), ) its
atomic decomposition. Then, for each atom a ∈ A(B), we define the principal ideal of a
the set: ↓ a = {b | a b}.

Now, the following result from [16] ensures that the atomic decomposition repre-
sents in fact the genuine locality-based modules of an ontology:

Lemma 13 ([16,13]). The set of genuine modules and that of principal ideals coincide.
Furthermore, if α ∈ a ∈ A(B): MBαe = MBae =↓ a.

Moreover, as consequence of Definition 10 and Lemma 13, each locality-based mod-
ule (genuine or not) is the union of one or more principal ideals (the converse however it
is not true, some union of principal ideals do not correspond to modules).
Given the atomic decomposition of an ontology there are some possible strategies
to extract the module for a given signature, for instance, by labelling each atom with the
terms that it is relevant to. Among these approaches are the labelling with minimal seed
signatures (MSSs) [13] and the labelling with minimum globalising signatures (MGSs)
[23].

5. Local Change with Atomic Decomposition

In this section, we combine the structural representation of ontologies studied in Sec-
tion 4, the atomic decomposition, and the results obtained with the theory of Local
Change, discussed in Section 3. Specifically, we devise a replacement for Definition 6
using a distinct notion of (un)relatedness. The first step is to define the height of an atom
as in Definition 14.

Definition 14. The height of an atom a is defined as:

0, if a is minimal
h(a) =
maxb|ab (1 + h(b)), otherwise

We part from the principle that atoms that participate in more modules are more
relevant. Whenever a b, we can assume that a is less relevant than b, since b is included
in every module with a, and b ∈↓ b, while a 6∈↓ b. Hence, we expect that lower atoms
participate in more genuine modules that higher ones. As fake modules are composed of
genuine ones, we also expect this relation to be reflected for modules in general.
This argument also motivates our choice for the maximum in Definition 14, as it
guarantees that if a b, then h(a) > h(b).
Figure 3, shows the height of each atom of the >⊥∗ -AD of the ontology B1 from
Example 8.

α1 2

α5 1 α2 1

α3 0 α4 0

Figure 3. >⊥∗ -AD of B1 with the height metric to the right of each atom

With this metric as a substitute for unrelatedness (Definition 5), we can formulate a
new retrieval operator to replace that of Definition 6.
Definition 15. Let B, B0 ⊆ L be ontologies with B0 ⊆ B and α ∈ L a formula. Then we
define the following family of retrieval operators:
∇iB (α, B0 ) = B0 ∩ {a ∈ (A(B), ) | a ⊆ MBαe and h(a) = i}
Definition 16. Let B, B0 ⊆ L be ontologies with B0 ⊆ B and α ∈ L a formula. Then we
define the following family of retrieval operators:
∇≤n
B (α, B 0) = S i
0≤i≤n ∇B (α, B) for n ≥ 0.
Also, ∇ω (α, 0) = S i 0 0
B B i≥0 ∇B (α, B ) denotes the set of relevant formulas for α in B .

We argue that the function ∇ from Definitions 15 and 16 captures a sense of rel-
evance very close to the function ∆ from Definitions 6 and 7, even without an explicit
(un)relatedness metric. Besides, a LBM is also a good approximation for compartments
ϕe ¬ϕ
because: for ϕ ∈ L, if ¬ϕ ∈ L, we have that MB = MB .
f

In fact, one interesting observation from the definition of ∇ is that ∇ω α
B (α, B) = MB .
e

Thus, our operator will never return formulas outside the locality-based module for the
input, considering our reference base B. And, as discussed, earlier, the formulas outside
the module for α. should not intervene in the proof of α.
It is also important to note that it may be the case that, given a formula ϕ ∈ B0 ,
ϕ 6∈ ∇0B (ϕ, B0 ), what would never happen in the relatedness functions discussed in [20].
However, this is not a shortcoming, since it is guaranteed that ϕ ∈ ∇ω 0
B (ϕ, B ) and it is
even possible that ϕ is a consequence of a subset of the module that contains it.
Example 17 compares the operators ∆ and ∇:
Example 17. Consider the ontology B1 from Example 8 and the formula ϕ =
∃hasPaymentMethod.PaymentMethod v Account. Let ∆ be the retrieval operator as
in Definitions 6 and 7, using the signature intersection as relation (see Figure 1). Also, let
∇ be as in Definitions 15 and 16, using the >⊥∗ -AD of the ontology B1 (as in Figure 3).
Then, we have:

∆0 (ϕ, B1 ) = 0/ ∇0B1 (ϕ, B1 ) = {α3 }
∆1 (ϕ, B1 ) = {α1 , α2 , α3 , α4 } ∇1B1 (ϕ, B1 ) = {α2 }
2
∆ (ϕ, B1 ) = {α5 } ∇2B1 (ϕ, B1 ) = 0/
∆ω (ϕ, B1 ) = B1 ∇ωB1 (ϕ, B1 ) = {α2 , α3 }
As remarked in Section 4, the signature intersection usually brings too many ax-
ioms for retrieval operations. In particular, ∆1 (ϕ, B1 ) already includes two formulas that
are unnecessary (α1 and α4 ). In Example 17, the locality-based module of B1 for the
signature ϕe using >⊥∗ -locality is exactly ∇ω B1 (ϕ, B1 ).
The Proposition 18 is analogous to Proposition 15 in [20], as it defines a localized
consequence operator using our retrieval operator ∇ and also proves that the resulting
inference is monotonic and compact.

Proposition 18. Let B and B0 ontologies with B0 ⊆ B and ϕ a formula. For every n ∈ N
and any inference operator Cn, if Cn is monotonic and compact (as it is the case in the
DLs) then the local inference operations defined as CnnhB,ϕi (B0 ) = Cn(∇≤n 0
B (ϕ, B )), are
monotonic and compact.

Proof. (Also very similar to the proof of Proposition 15 in [20])
We can assume compactness since all sets involved (the ontology, modules, atoms)
are finite. To prove that the inference operator is monotonic, let B, B1 and B2 be on-
tologies, such that B1 ⊆ B2 ⊆ B. By the definition of ∇≤n ≤n
B , we have that ∇B (ϕ, B1 ) ⊆
∇≤n ≤n ≤n
B (ϕ, B2 ). Given that Cn is monotonic: Cn(∇B (ϕ, B1 )) ⊆ Cn(∇B (ϕ, B2 )).

With Proposition 18, we are able to replace the compartmentalization function in
the Local Change framework by any retrieval operator of the family ∇≤n B . Since the op-
erator obtained is monotonic and compact we can localize contraction [15] and revision
operations [10] for ontologies.
Additionally, for the operator ∇ω
B , we have the following result:

Corollary 19. Let B be an ontology and ϕ a formula. For every n ∈ N and any inference
operator Cn, if Cn is monotonic and compact (as it is the case in the DLs) then the local
inference operations defined as Cnω ω
ϕ (B) = Cn(∇B (ϕ, B)), are monotonic and compact.

Proof. As in the proof of Proposition 18 we can assume compactness. First we remark
ϕe
that ∇ωB (ϕ, B) = MB . Since locality-based modules are monotonic w.r.t. ontology en-
largement [21], we have that if B1 ⊆ B2 , then ∇ω
B1 (ϕ, B1 ) ⊆ ∇B2 (ϕ, B2 ). Finally, by mono-
ω

tonicity of Cn: Cn(∇B1 (ϕ, B1 )) ⊆ Cn(∇B2 (ϕ, B2 )).
ω ω

Corollary 19 implies that for ∇ω one does not need to fix a reference ontology.
The two methods that we compared in this section, the ∆ operator with signature
intersection, and the ∇ operator derived from the atomic decomposition, have the benefit
of not requiring any external information besides the ontology itself. In both cases, the
relationships between formulas are obtained purely from the syntax and pre-determined
rules (be it intersection between signatures or matching locality rules).
This way of obtaining relationships makes both approaches syntax dependent in the
sense that two logically equivalent ontologies may have different structures. Even so, we
do not consider this as a shortcoming, as we consider that the way how formulas are
written elucidate the meaning intended by the designer. Yet, Proposition 18 is agnostic
with respect to the structuring of the base, thus, other methods can be devised to replace
the approaches discussed here.
One downside of the metric proposed here is that it is not easy to extend the unre-
latedness valuation to formulas outside the belief base of reference. This problem occurs
because any modification, even the addition of a single formula, to the base may trans-
form the atomic decomposition significantly, changing the atoms and the dependency
relations between them [24].
We remark that applying change methods to limited portions of the module (some
∇≤i
B (ϕ, B0 ) 6= ∇ω 0
B (ϕ, B ), for instance) does not guarantee that the whole ontology is re-
paired at axiom level. Still, these retrieval operators can be useful to obtain suggestions
for repairs, even more in situations were the locality-based module obtained is too big.

6. Related Work

While here we intend to relate the modularisation techniques with the theory of Local
Change so one can manage a part of the ontology at a time on tasks such as repair, there
are also works which apply a similar idea, such as the one by Grau et al. [25], where
they provide a framework for incremental reasoning which avoids recomputing infer-
ences when an ontology changes. Another example is due to Suntisrivaraporn [26], where
locality-based modules are employed to compute the set of all justifications (kernels) of
an ontology.

7. Conclusion

The fields of ontology modularisation and ontology change are linked by the notion of
relevance. In this work, we devised a relevance metric based on techniques of ontology
modularisation and employed them in a framework for ontology change.
Both local change and the atomic decomposition have solid formal foundations and
are concerned with the efficiency of the operations over ontologies and with the ability
to concentrate procedures to portions of the ontology. This is particularly interesting for
debugging methods over such knowledge bases, since a designer may aim to change a
problematic fragment of the ontology causing the least impact possible on unrelated parts
of the ontology.
We remark that when defining notions of relevance for certain applications, it is re-
quired that it provides good logical properties to be used in procedures such as reason-
ing and change operations. Furthermore, it is important to consider how computationally
expensive it is to compute the proposed metric, otherwise this could render the selection
of relevant formulas too demanding to be applied in practice.
Following this work, we propose the implementation of this metric to empirically
evaluate its efficiency in real scenarios. In addition, despite the existence of polynomial
algorithms to compute the atomic decomposition, it is necessary to develop a method to
avoid recomputing it at every operation of change; thus an interesting proposal would
be to continue the work by Klinov, Del Vescovo and Schneider [24] which has the first
results in this direction.

Acknowledgements: This work has been partially funded by CAPES and partially
by FAPESP, through grant 2017/04410-0.
References

[1] Mike Dean, Guus Schreiber, Sean Bechhofer, Frank van Harmelen, Jim Hendler, and Ian Horrocks.
OWL Web Ontology Language Reference. W3C Recommendation (http://www.w3.org/TR/owl-ref/),
10:2006–01, 2004.
[2] Pascal Hitzler, Markus Krötzsch, Bijan Parsia, Peter F. Patel-Schneider, and Sebastian Rudolph, editors.
OWL 2 Web Ontology Language: Primer. W3C Recommendation, 27 October 2009. Available at
http://www.w3.org/TR/owl2-primer/.
[3] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider,
editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge Uni-
versity Press, 2003.
[4] Stefan Schlobach and Ronald Cornet. Non-standard reasoning services for the debugging of description
logic terminologies. In Georg Gottlob and Toby Walsh, editors, Proceedings of the Eighteenth Interna-
tional Joint Conference on Artificial Intelligence (IJCAI 2003) , Acapulco, Mexico, August 9-15, 2003,
pages 355–362. Morgan Kaufmann, 2003.
[5] Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn. Pinpointing in the description logic
EL. In Diego Calvanese, Enrico Franconi, Volker Haarslev, Domenico Lembo, Boris Motik, Anni-
Yasmin Turhan, and Sergio Tessaris, editors, Proceedings of the 2007 International Workshop on De-
scription Logics (DL2007), Brixen-Bressanone, near Bozen-Bolzano, Italy, 8-10 June, 2007, volume 250
of CEUR Workshop Proceedings. CEUR-WS.org, 2007.
[6] Matthew Horridge. Justification based explanation in ontologies. PhD thesis, University of Manchester,
2011.
[7] Giorgos Flouris. On Belief Change and Ontology Evolution. PhD thesis, University of Crete, 2006.
[8] Guilin Qi, Weiru Liu, and David A. Bell. A revision-based approach to handling inconsistency in
description logics. Artificial Intelligence Review, 26:115–128, October 2006.
[9] Márcio Moretto Ribeiro and Renata Wassermann. Base revision for ontology debugging. The Journal
of Logic and Computation, 19(5):721–743, 2009.
[10] Márcio Moretto Ribeiro. Belief Revision in Non-Classical Logics. Springer Briefs in Computer Science.
Springer, 2013.
[11] Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler. Modular reuse of ontolo-
gies: Theory and practice. The Journal of Artificial Intelligence Research, 31:273–318, 2008.
[12] Chiara Del Vescovo, Bijan Parsia, Ulrike Sattler, and Thomas Schneider. The modular structure of an
ontology: an empirical study. In Proceedings of the 4th International Workshop on Modular Ontologies
(WoMO 2010), Toronto, ON, Canada, May 11, 2010, pages 11–24, 2010.
[13] Chiara Del Vescovo. The modular structure of an ontology: Atomic decomposition. PhD thesis, Univer-
sity of Manchester, 2013.
[14] Sven Ove Hansson. A Textbook of Belief Dynamics. Springer, 1999.
[15] Sven Ove Hansson and Renata Wassermann. Local change. Studia Logica, 70(1):49–76, 2002.
[16] Chiara Del Vescovo, Bijan Parsia, Ulrike Sattler, and Thomas Schneider. The modular structure of an
ontology: Atomic decomposition. In Toby Walsh, editor, Proceedings of the 22nd International Joint
Conference on Artificial Intelligence (IJCAI 2011), Barcelona, Catalonia, Spain, July 16-22, 2011, pages
2232–2237. IJCAI/AAAI, 2011.
[17] Carlos E. Alchourrón, Peter Gärdenfors, and David Makinson. On the logic of theory change: Partial
meet contraction and revision functions. The Journal of Symbolic Logic, 50(2):510–530, 1985.
[18] Giorgos Flouris, Zhisheng Huang, Jeff Z. Pan, Dimitris Plexousakis, and Holger Wache. Inconsistencies,
negations and changes in ontologies. In Proceedings, The Twenty-First National Conference on Artificial
Intelligence (AAAI), pages 1295–1300, 2006.
[19] Sven Ove Hansson. Kernel Contraction. The Journal of Symbolic Logic, 59(3):845–859, 1994.
[20] Renata Wassermann. On structured belief bases. In Hans Rott and Mary-Anne Williams, editors, Fron-
tiers in Belief Revision. Kluwer, 2001.
[21] Ulrike Sattler, Thomas Schneider, and Michael Zakharyaschev. Which kind of module should I extract?
In Bernardo Cuenca Grau, Ian Horrocks, Boris Motik, and Ulrike Sattler, editors, Proceedings of the
22nd International Workshop on Description Logics (DL 2009), Oxford, UK, July 27-30, 2009, volume
477 of CEUR Workshop Proceedings. CEUR-WS.org, 2009.
[22] Chiara Del Vescovo, Bijan Parsia, Ulrike Sattler, and Thomas Schneider. The modular structure of
an ontology: an empirical study. In Volker Haarslev, David Toman, and Grant E. Weddell, editors,
Proceedings of the 23rd International Workshop on Description Logics (DL 2010), Waterloo, Ontario,
Canada, May 4-7, 2010, volume 573 of CEUR Workshop Proceedings. CEUR-WS.org, 2010.
[23] Venkata Krishna Chaitanya Turlapati and Sreenivasa Kumar Puligundla. Efficient module extraction for
large ontologies. In Pavel Klinov and Dmitry Mouromtsev, editors, Proceedings of the 4th International
Conference on Knowledge Engineering and the Semantic Web (KESW 2013), St. Petersburg, Russia,
October 7-9, 2013., volume 394 of Communications in Computer and Information Science, pages 162–
176. Springer, 2013.
[24] Pavel Klinov, Chiara Del Vescovo, and Thomas Schneider. Incrementally updateable and persistent
decomposition of OWL ontologies. In Pavel Klinov and Matthew Horridge, editors, Proceedings of
OWL: Experiences and Directions Workshop 2012 (OWLED 2012), Heraklion, Crete, Greece, May 27-
28, 2012, volume 849 of CEUR Workshop Proceedings. CEUR-WS.org, 2012.
[25] Bernardo Cuenca Grau, Christian Halaschek-Wiener, Yevgeny Kazakov, and Boontawee Suntisrivara-
porn. Incremental classification of description logics ontologies. J. Autom. Reasoning, 44(4):337–369,
2010.
[26] Boontawee Suntisrivaraporn, Guilin Qi, Qiu Ji, and Peter Haase. A Modularization-Based Approach
to Finding All Justifications for OWL DL Entailments. In The Semantic Web - Proceedings of the 3rd
Asian Semantic Web Conference, ASWC 2008, volume 5367 of Lecture Notes in Computer Science,
pages 1–15. Springer, 2008.