Local Change in Ontologies with Atomic Decomposition Ricardo GUIMARÃES a,1 and Renata WASSERMANN a,2 a Institute of Mathematics and Statistics, University of Sã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 Krö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 Peñ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] Márcio Moretto Ribeiro and Renata Wassermann. Base revision for ontology debugging. The Journal of Logic and Computation, 19(5):721–743, 2009. [10] Má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. Alchourrón, Peter Gä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.