When debugging big ontologies, it can be convenient to isolate the problematic 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 subject 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 efficiency of change operations. Thus, in this work, we aim to devise a relevance metric using atomic decomposition, originated in the field of Ontology Modularisation, 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 description logic ontologies, which could be useful to make debugging procedures more feasible for both ontology designers and computer programs.
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 W3C 3 . One of the most interesting 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 expressiveness and computational complexity of the associated inference task. Given an ontology, 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 repair must also avoid introducing new inconsistencies or undesired consequences as well as losing important information. Approaches in the literature, such as those based on 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 (rationality 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 modularisation area: improve the efficiency of procedures when handling large sets of formulas 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 decomposition 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) operator 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 nonlogical terms (the signature) of a formula ϕ is denoted by ϕ and the signature of a set of formulas X by X. Also, we consider the reader familiar with Description Logics and its usual notation (for further details we refer the reader to [3]).
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 formulas, closed under an inference operation, the belief sets. Over these sets, the authors defined three fundamental operations that take as input a belief set K and a formula ϕ: expansion (+), 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 proposed to ontologies in Description Logics. The first issue is that the AGM theory considers 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 formulas 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), characterized 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 satisfy 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 inconsistency in ontologies: the one that defines that an ontology is inconsistent if it implies ⊥, 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.
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 operations, 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:
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
The function c is the compartmentalization function.
The compartmentalization is in turn employed to define localized consequence operators 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 C A (B), is the inference operation such that for all sets B ⊆ L:
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.
). Given B a belief base and R a relation between formulas, a R-path between ϕ and ψ in B is a sequence P = ϕ i 0≤i≤n of formulas such that:
If the relation R is irrelevant or clear from the context we simply talk about a path in B. We denote that the P is a path between ϕ and ψ by: ϕ P ψ. Additionally, the length of a path P = ϕ i 0≤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:
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.
). Let B ⊆ L be a belief base and α ∈ L a formula. Then we define the following family of retrieval operators:
). Let B ⊆ L be a belief base and α ∈ L a formula. Then we define the following family of retrieval operators:
) denotes the set of relevant formulas for α.
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 corresponds 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 B 1 :
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 numerous 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 API 4 .
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 M Σ B ), using any of the three aforementioned notions, are justificationpreserving [11,21], in other words, each ϕ-kernel is a subset of M ϕ B . The fact that locality-based modules preserve justifications gives an interesting relation 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 literature to induce structure over ontologies. Besides the logical and computational aspects 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, ⊆). Modules 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 representation 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 between 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 B 1 from Example 8, its atomic decomposition using ⊥ * -locality as notion (i.e. the ⊥ * -AD of B 1 ) is shown in Figure 2.
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 informative 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:
B 1 , as they are in disjoint components of the atomic decomposition. Also, there are results which sustain the atomic decomposition as a succinct representation 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 better 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 represents 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):
Moreover, as consequence of Definition 10 and Lemma 13, each locality-based module (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].
In this section, we combine the structural representation of ontologies studied in Section 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:
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 ∈↓ 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).
) denotes the set of relevant formulas for α in B . We argue that the function ∇ from Definitions 15 and 16 captures a sense of relevance 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 because: for ϕ ∈ L, if ¬ϕ ∈ L, we have that
In fact, one interesting observation from the definition of ∇ is that ∇ ω B (α, B) = M α B . 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 ϕ ∈ B , ϕ ∈ ∇ 0 B (ϕ, B ), what would never happen in the relatedness functions discussed in [20]. However, this is not a shortcoming, since it is guaranteed that ϕ ∈ ∇ ω 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 B 1 from Example 8 and the formula ϕ = ∃hasPaymentMethod.PaymentMethod 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 B 1 (as in Figure 3). Then, we have:
because any modification, even the addition of a formula, to the base may transform 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 (ϕ, B ) = ∇ ω B (ϕ, B ), for instance) does not guarantee that the whole ontology is repaired 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.
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 inferences 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.
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 required that it provides good logical properties to be used in procedures such as reasoning 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.
As remarked in Section 4, the signature intersection usually brings too many axioms retrieval operations. In particular, ∆ 1 (ϕ, B 1 ) already includes two formulas that are unnecessary (α 1 and α 4 ). In Example 17, the locality-based module of B 1 for the signature ϕ using ⊥ * -locality is exactly ∇ ω B 1 (ϕ, B 1 ). 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 B ontologies with B ⊆ 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 Cn n B,ϕ (B ) = Cn(∇ ≤n 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, B 1 and B 2 be ontologies, such that
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 operator 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 that
Since locality-based modules are monotonic w.r.t. ontology enlargement [21], we have that if
). 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 unrelatedness valuation to formulas outside the belief base of reference. This problem occurs