Vol-3197/paper2
Jump to navigation
Jump to search
Paper
Paper | |
---|---|
edit | |
description | |
id | Vol-3197/paper2 |
wikidataid | Q117338337→Q117338337 |
title | Repairing Ontologies via Kernel Pseudo-Contraction |
pdfUrl | https://ceur-ws.org/Vol-3197/paper2.pdf |
dblpUrl | https://dblp.org/rec/conf/nmr/MatosW22 |
volume | Vol-3197→Vol-3197 |
session | → |
Freitext
Repairing Ontologies via Kernel Pseudo-Contraction
Repairing Ontologies via Kernel Pseudo-Contraction Vinícius Bitencourt Matos1,∗ , Renata Wassermann1,∗ , PhD 1 Universidade de São Paulo (USP), São Paulo, Brazil Abstract Rational agents must have some internal representation of their knowledge or belief system. Belief Revision is a research area that aims at understanding how they should change their representations when they are faced with new information. In a contraction operation, a sentence is removed from a knowledge base and must not be logically entailed by the resulting set. Pseudo-contraction was proposed by Hansson as an alternative to base contraction where some degree of syntax independence is allowed. In this work, we analyse kernel constructions for pseudo-contraction operations and their formal properties. Also, we show the close relationship between concepts and definitions of Belief Revision and Ontology Repair (such as pseudo-contractions and gentle repairs, respectively). Keywords Belief revision, Description logics, Ontology repair, Pseudo-contraction 1. Introduction inclusion — no new beliefs are added [5]. There are two main constructions associated to contraction operations: Belief Revision is a research area that deals with problems partial meet contraction [1] with respect to a sentence is related to changing knowledge bases or logical theories, defined as the intersection of some inclusion-maximal especially in the face of new, possibly conflicting, in- subsets that do not entail it, and kernel contraction [6] is formation. The work of Alchourrón, Gärdenfors, and obtained by removing at least one sentence from each Makinson [1] is widely recognised as the initial hallmark inclusion-minimal subset entailing the sentence to be of this area, and gave rise to what is known as the AGM removed. paradigm. Originally, it required the underlying logic to The area of Ontology Repair groups together tools satisfy some assumptions, such as compactness, mono- and formal definitions related to the task of debugging tonicity and the deduction theorem, and most work fol- ontologies and getting rid of unwanted inferences. Dif- lowing AGM was developed with propositional logic in ferent approaches have been proposed, depending on mind. In the AGM paradigm, the beliefs of an agent are which parts of the knowledge base one wants to change represented by sets closed under logical consequences, [7, 8, 9, 10, 11]. the belief sets. Over the past decades, the AGM theory Both in Belief Revision and in Ontology Repair, classi- has been adapted to belief bases (sets of sentences that are cal approaches assume that no information can be added not necessarily closed) represented in different logical to a knowledge base when we perform the task of remov- formalisms, such as Horn or Description Logics [2, 3, 4]. ing some unwanted consequence. Whilst this assumption The AGM paradigm defines three change operations may be reasonable, it is usually formalised as a syntactic on belief sets: expansion, which incorporates a new be- requirement of inclusion, in a way that forces the removal lief; contraction, which removes a belief; and revision, of too much information. The assumption can be for- which incorporates a new belief retaining consistency. malised as a less restrictive constraint which only states In this paper, we will only address the problem of re- that we cannot add new consequences to the knowledge tracting beliefs, thus contraction operations and their base, thus allowing to add sentences that were logically variations. In a contraction operation, a sentence must entailed by the original set. Note that this formalisa- be removed from a set and must not be entailed by the tion still captures the intuition that no new information contracted set. Some of the minimal requirements for an should be added, but “information” is now seen as inde- operation to be a belief contraction are that it satisfies pendent from the syntax. This idea has been proposed success — the removed set is not entailed anymore — and and developed in both areas in the last decades, with different terminologies and notations. In Belief Revision, NMR 2022: 20th International Workshop on Non-Monotonic Reasoning, pseudo-contractions are generalisations of contractions August 07–09, 2022, Haifa, Israel that allow the addition of sentences as long as they were ∗ Corresponding author. already entailed by the initial set. Similarly, in Ontology Envelope-Open vinicius.matos@alumni.usp.br (V. B. Matos); renata@ime.usp.br (R. Wassermann) Repair, a gentle repair of an ontology is built by removing Orcid 0000-0001-7342-6668 (V. B. Matos); 0000-0001-8065-1433 sentences or replacing them with weaker versions so that (R. Wassermann) the resulting set does not imply the unwanted sentence, © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). and new consequences are not allowed [12]. CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 16 � Recently, a pseudo-contraction construction based on This can be formalised, for example, in a Description partial meet contraction was proposed and characterised Logic: [13, 14]. It uses a weak consequence operator (i.e. a con- 𝑆𝑤𝑒𝑑𝑖𝑠ℎ ⊑ 𝐸𝑢𝑟𝑜𝑝𝑒𝑎𝑛; sequence operator that may not include all the conse- 𝐸𝑢𝑟𝑜𝑝𝑒𝑎𝑛 ⊓ 𝑆𝑤𝑎𝑛 ⊑ ∃ℎ𝑎𝑠𝐶𝑜𝑙𝑜𝑢𝑟.{𝑤ℎ𝑖𝑡𝑒}; quences of a classical Cn) to expand the initial set of sentences before applying the classical partial meet con- 𝑠 ∶ 𝑆𝑤𝑎𝑛 ⊓ 𝑆𝑤𝑒𝑑𝑖𝑠ℎ. traction. If we want to contract by 𝑠 ℎ𝑎𝑠𝐶𝑜𝑙𝑜𝑢𝑟 𝑤ℎ𝑖𝑡𝑒, one of the In this text, we analyse a pseudo-contraction construc- sentences must be removed; thus, for example, if we tion that is based on a kernel contraction and expands choose to remove the third sentence, the fact that 𝑠 is a the set with some of its consequences before applying swan is lost. the classical kernel contraction. Furthermore, we show that some concepts and definitions of Belief Revision Intuitively, in Example 1, we should consider replacing and Ontology Repair are closely related, extending some the sentence 𝑠 ∶ 𝑆𝑤𝑎𝑛 ⊓ 𝑆𝑤𝑒𝑑𝑖𝑠ℎ with a weaker version previous work and showing that the new kernel pseudo- 𝑠 ∶ 𝑆𝑤𝑎𝑛, which is forbidden by the inclusion postulate. contraction is also connected to gentle repairs. In order Another intuitive idea prohibited by that postulate is to to facilitate the integration between the areas, we will weaken 𝐸𝑢𝑟𝑜𝑝𝑒𝑎𝑛 ⊓ 𝑆𝑤𝑎𝑛 ⊑ ∃ℎ𝑎𝑠𝐶𝑜𝑙𝑜𝑢𝑟.{𝑤ℎ𝑖𝑡𝑒} by adding adopt a functional notation for Belief Revision, which we an intersection to the left-hand side, in order to convey have proposed in a previous work (e.g. the contraction the idea that all European swans that satisfy a certain of 𝐵 by 𝛼 will be denoted by c(𝐵, 𝛼) rather than 𝐵 − 𝛼). property (e.g. “normal” or “typical”) are white. We expect it to be clearer and less ambiguous than the Hansson has proposed a weakening of inclusion, logi- classical infix notation. cal inclusion [5], which is satisfied by operations he has The results of this paper appeared in the first author’s called pseudo-contractions [16]: thesis [15, sections 3.2, 3.3 and 4.2], which contains the (logical inclusion) Cn(c(𝐵, 𝛼)) ⊆ Cn(𝐵). proofs that have been omitted here due to space con- straints. The proofs are also available at https://www. (success) If 𝛼 ∉ Cn(∅), then 𝛼 ∉ c(𝐵, 𝛼). ime.usp.br/~renata/papers/NMR2022_supplement.pdf. This text is structured as follows. Section 2 introduces Definition 2 (Pseudo-contraction [16]). An operation pseudo-contractions and presents some definitions that c is a pseudo-contraction if c satisfies success and logical will be used throughout the paper. In Section 3, we de- inclusion. fine our new operation (Cn* kernel pseudo-contraction), explain its properties and characterise it by means of a With logical inclusion, whilst we still do not allow set of postulates. Section 4 shows our prototype of a tool the addition of arbitrary sentences, the resulting set no that computes some pseudo-contractions in ontologies. longer has to be a subset of the original set, thus making Ontology Repair is introduced in Section 5, and its con- it possible to insert the sentence 𝑠 ∶ 𝑆𝑤𝑎𝑛 in Example 1. nections with Belief Revision are presented in Section 6. From now on, we will consider a generic consequence Section 7 finishes the text with the conclusions. operator Cn that is Tarskian and compact, such as CnFOL and the consequence operators that correspond to some fragments of first-order logic. Thus, the operations we 2. Pseudo-contraction Operations will present do not assume any other syntactic or seman- Contractions over belief bases can lead to unnecessary tic features of the logic, which makes them applicable to waste of information, largely due to the inclusion postu- logics that do not satisfy the AGM requirements (such late [16]: as Description Logics, which usually do not have a sen- tence ¬𝜑 for every sentence 𝜑). Results that require extra (inclusion) c(𝐵, 𝛼) ⊆ 𝐵. properties will explicitly mention them. The set of all The postulate requires that the result of contracting a sentences in the language will be denoted by 𝔏. Subclas- belief base 𝐵 by a sentence 𝛼 is included in the original sicality will be defined with respect to Cn. belief base. This postulate prevents the weakening of In the following sections, we will present some pseudo- formulae, which can be seen as an argument against its contraction constructions that depend on the kind of for- use for belief bases. mulae that we are allowed to add when contracting by a formula. Before computing the kernel set, our operations Example 1. Consider a knowledge base that contains will “close” the set under a new consequence operator, the following three sentences: Cn*, which will make possible the insertion of new sen- - All Swedish things are European; tences. This is a generic operator whose definition is - European Swans are white; deliberately unspecified, and we will explicitly state the - 𝑠 is a Swedish Swan. conditions that are required by each theorem. 17 � The properties of pseudo-contraction constructions Definition 3 (Kernel and kernel set [6]). Let 𝐵 ⊆ 𝔏 and depend on the properties that are satisfied by Cn*, es- 𝛼 ∈ 𝔏. The kernel set of 𝐵 with respect to 𝛼, denoted by pecially inclusion and subclassicality: if both are satis- Ker[𝐵, 𝛼], is such that a set 𝑋 is in Ker[𝐵, 𝛼] if and only fied, then Cn* is in an intermediate level between the if 𝑋 ⊆ 𝐵, 𝛼 ∈ Cn(𝑋 ), and there is no 𝑌 ⊂ 𝑋 such that original base (which would be used in a base contrac- 𝛼 ∈ Cn(𝑌 ). Each such 𝑋 is an 𝛼-kernel. tion) and its closure (as in classical AGM contraction), i.e. 𝐵 ⊆ Cn*(𝐵) ⊆ Cn(𝐵). For practical applications, Cn*(𝐵) We will show later (Proposition 28) that the definition should always be finite if 𝐵 is finite, but we will not as- above is related to that of justification (Definition 18), sume this restriction. which is well-known in Ontology Repair. Automatic reasoners for ontologies — such as HermiT1 Definition 4 (Incision function [6]). Let 𝐵 ⊆ 𝔏. A and Fact++2 — allow the user to choose the types of con- function 𝑓 is an incision function6 for 𝐵 if, for every sequences that will be generated. Each configuration can 𝛼 ∈ 𝔏, it is the case that 𝑓 (Ker[𝐵, 𝛼]) ⊆ ⋃ Ker[𝐵, 𝛼] and be seen as a Cn*, which satisfies inclusion3 and is usu- 𝑓 (Ker[𝐵, 𝛼]) ∩ 𝑋 ≠ ∅ for every non-empty 𝑋 ∈ Ker[𝐵, 𝛼]. ally subclassical4 . Since they are syntactically restricted, they are good examples of weak consequence operators. Definition 5 (Cn* kernel pseudo-contraction). Let 𝐵 be Those reasoners can be embedded in ontology editors, a set of sentences, Cn* a consequence relation and 𝑓 such as Protégé5 , as shown in Figure 1. an incision function for Cn*(𝐵). The Cn* kernel pseudo- contraction of 𝐵 by a sentence 𝛼, denoted by kcCn* 𝑓 (𝐵, 𝛼), is such that, for all sentences 𝛼: kcCn* 𝑓 (𝐵, 𝛼) = Cn*(𝐵) ⧵ 𝑓 (Ker[Cn*(𝐵), 𝛼]). The following examples illustrate this construction: Example 6. Let Cn*break be a consequence operator that preserves the existing sentences and adds 𝑎 ∶ 𝐶𝑖 (for 𝑖 = 1, … , 𝑛) for every sentence 𝑎 ∶ 𝐶1 ⊓ ⋯ ⊓ 𝐶𝑛 in the original set. This is analogous to the consequence opera- tor that “breaks conjunctions into conjuncts”, originally presented in [17]. If 𝐵 is the knowledge base defined in Example 1, then Cn*break (𝐵) = 𝐵 ∪ {𝑠 ∶ 𝑆𝑤𝑎𝑛, 𝑠 ∶ Figure 1: Screenshot of the Protégé window where the user 𝑆𝑤𝑒𝑑𝑖𝑠ℎ}. Let 𝛼 be the sentence 𝑠 ℎ𝑎𝑠𝐶𝑜𝑙𝑜𝑢𝑟 𝑤ℎ𝑖𝑡𝑒. We can choose which types of consequences will be exported. have Ker[Cn*break (𝐵), 𝛼] = {{𝛽1 , 𝛽2 , 𝛽3 }, {𝛽1 , 𝛽2 , 𝛽3′ , 𝛽3″ }}, where Another example of Cn* is the conversion of sentences 𝛽1 = 𝑆𝑤𝑒𝑑𝑖𝑠ℎ ⊑ 𝐸𝑢𝑟𝑜𝑝𝑒𝑎𝑛, into some standard format, such as conjunctive and dis- 𝛽2 = 𝐸𝑢𝑟𝑜𝑝𝑒𝑎𝑛 ⊓ 𝑆𝑤𝑎𝑛 ⊑ ∃ℎ𝑎𝑠𝐶𝑜𝑙𝑜𝑢𝑟.{𝑤ℎ𝑖𝑡𝑒}, junctive normal forms, and normal forms tailored to spe- 𝛽3 = 𝑠 ∶ 𝑆𝑤𝑎𝑛 ⊓ 𝑆𝑤𝑒𝑑𝑖𝑠ℎ, cific logics, as long as no new symbols are introduced. 𝛽3′ = 𝑠 ∶ 𝑆𝑤𝑎𝑛 and Since inclusion is not satisfied by those consequence op- 𝛽3″ = 𝑠 ∶ 𝑆𝑤𝑒𝑑𝑖𝑠ℎ. erators, some desirable properties may not be satisfied by constructions that use them; on the other hand, they may If the definition of the incision function 𝑓 is such that be of use if good inference algorithms exist for them. 𝑓 (Ker[Cn*break (𝐵), 𝛼]) = {𝛽3 , 𝛽3″ }, then the result of the Cn* operation is kc𝑓 break (𝐵, 𝛼) = (𝐵 ⧵ 𝛽3 ) ∪ {𝛽3′ }, i.e., the 3. Cn* kernel pseudo-contraction pseudo-contraction replaces 𝛽3 with its weaker version 𝛽3′ . In this section, we will present a pseudo-contraction op- In order to characterise this operation, we will need a eration that is defined as a kernel contraction starting starred version of some postulates: from the expanded set Cn*(𝐵). (inclusion*) c(𝐵, 𝛼) ⊆ Cn*(𝐵). 1 http://www.hermit-reasoner.com/ 2 3 http://owl.cs.manchester.ac.uk/tools/fact/ (uniformity*) If for all 𝐵′ ⊆ Cn*(𝐵), 𝛼 ∈ Cn(𝐵′ ) if One step after the window shown in Figure 1, users can choose whether the original sentences should be kept. and only if 𝛽 ∈ Cn(𝐵′ ), then c(𝐵, 𝛼) = c(𝐵, 𝛽). 4 Except, maybe, for some highly-complex ontologies that cannot be 6 represented in classical logic. It should be noted that incision functions depend only on the kernel 5 http://protege.stanford.edu/ set, which may be the same for distinct pairs of 𝐵 and 𝛼. 18 � (core-retainment*) If 𝛽 ∈ Cn*(𝐵)⧵c(𝐵, 𝛼), then there Theorem 9. [18] The function 𝑓 𝑔 (as in Definition 8) is an incision function for 𝑋. is some 𝐵′ ⊆ Cn*(𝐵) such that 𝛼 ∈ Cn(𝐵′ ∪ {𝛽}) ⧵ Cn(𝐵′ ). The representation theorem follows. As mentioned earlier, Cn* kernel pseudo-contraction Theorem 7 (Cn* kernel pseudo-contraction: represen- subsumes Cn* partial meet pseudo-contraction. The fol- tation theorem). If Cn* satisfies monotonicity, then an lowing proposition shows the explicit construction: operation is a Cn* kernel pseudo-contraction if and only if Proposition 10. If pmcCn* 𝑔 is a Cn* partial meet pseudo- it satisfies success, inclusion*, core-retainment* and unifor- contraction, then it is equivalent to the Cn* kernel pseudo- mity*. contraction kcCn* 𝑓𝑔 . Proof sketch. Construction-to-postulates: Success can be shown by contradiction: if 𝛼 ∈ Cn(kcCn* Cn* 𝑓 (𝐵, 𝛼)), then Proof. Let pmc𝑔 be a Cn* partial meet pseudo-contrac- the fact that Cn is Tarskian implies that there is some tion. We can rewrite it as follows: non-empty 𝑋 ∈ Ker[Cn*(𝐵) ⧵ 𝑓 (Ker[Cn*(𝐵), 𝛼]), 𝛼], and such 𝑋 must be in Ker[Cn*(𝐵), 𝛼], but this implies that pmcCn*𝑔 (𝐵, 𝛼) 𝑓 (Ker[Cn*(𝐵), 𝛼]) ∩ 𝑋 = ∅, violating the definition of = ⋂ 𝑔(Rem[Cn*(𝐵), 𝛼]) incision function. Inclusion* and core-retainment follow directly from the definitions. For uniformity*, if 𝛼 and = Cn*(𝐵) ⧵ [Cn*(𝐵) ⧵ ⋂ 𝑔(Rem[Cn*(𝐵), 𝛼])] 𝛽 satisfy the antecedent but not the consequent, then = Cn*(𝐵) ⧵ 𝑓 𝑔 (Ker[𝑋 , 𝛼]) there must be some 𝑋 ∈ Ker[Cn*(𝐵), 𝛼] ⧵ Ker[Cn*(𝐵), 𝛽] (w.l.o.g., swapping 𝛼 and 𝛽 for the other case); thus, either = kcCn* 𝑓 𝑔 (𝐵, 𝛼), ′ 𝛽 ∉ Cn(𝑋 ) or there is some 𝑋 ⊊ 𝑋 such that 𝛽 ∈ Cn(𝑋 ), ′ and neither can hold because 𝑋 ∈ Ker[Cn*(𝐵), 𝛼]. where 𝑓 𝑔 is the incision function defined as in Defini- Postulates-to-construction: This part of the proof is analo- tion 8 (for 𝑋 = Cn*(𝐵)). gous to the proof of the corresponding theorem in [6]. If cCn* satisfies the postulates, then the function 𝑓 defined In general, not every kernel contraction is equiva- as 𝑓 (Ker[Cn*(𝐵), 𝛼]) ∶= Cn*(𝐵) ⧵ cCn* (𝐵, 𝛼) is a well-de- lent to a partial meet contraction. By taking Cn* as the fined incision function for Cn*(𝐵) and the operations identity function, Cn* partial meet and kernel pseudo- kcCn* and cCn* are equivalent. contractions become partial meet and kernel contractions 𝑓 for belief bases, which means that they are not equiv- Cn* partial meet pseudo-contraction, a pseudo-con- alent. Therefore, Cn* kernel pseudo-contractions may traction construction that “closes” the set under Cn* be- not have the same properties as Cn* partial meet pseudo- fore applying a classical partial meet contraction, was contractions. proposed by [13]. The result of the operation, denoted Since inclusion* implies logical inclusion for every by pmcCn* 𝑔 (𝐵, 𝛼), is obtained by taking the intersection subclassical Cn* [14], we can see that a Cn* kernel pseudo- of the output of a selection function 𝑔 that chooses some contraction is indeed a pseudo-contraction as long as Cn* elements (at least one) of Rem[Cn*(𝐵), 𝛼], which is the satisfies subclassicality. If Cn* also satisfies inclusion, set of all inclusion-maximal subsets of Cn*(𝐵) that do not then the following property holds: entail 𝛼. (logical core-retainment) If 𝛽 ∈ 𝐵 ⧵ c(𝐵, 𝛼), then Cn* partial meet pseudo-contractions satisfy rele- vance*, and Cn* kernel pseudo-contractions satisfy core- there is a 𝐵′ such that 𝐵′ ⊆ Cn(𝐵) and 𝛼 ∈ Cn(𝐵′ ∪ {𝛽}) ⧵ retainment*; moreover, the other three postulates are Cn(𝐵′ ). identical (success, inclusion* and uniformity*). Hence, every Cn* partial meet pseudo-contraction is also a Cn* Observation 11. If Cn* satisfies subclassicality and in- kernel pseudo-contraction. We will now show how to clusion, then any operation that satisfies core-retainment* obtain the explicit construction of a Cn* kernel pseudo- also satisfies logical core-retainment. contraction from a Cn* partial meet pseudo-contraction. A desirable property that is not necessarily satisfied This will use the definition of an incision function derived by kernel contractions (hence, not always satisfied by from a selection function: Cn* kernel pseudo-contractions) is relative closure [19]: Definition 8 (Incision function associated to a selection (relative closure) 𝐵 ∩ Cn(c(𝐵, 𝛼)) ⊆ c(𝐵, 𝛼). function [18]). Let 𝑔 be a selection function for 𝑋. The function 𝑓 𝑔 defined as Nonetheless, kernel contractions and Cn* kernel pseudo-contractions satisfy relative closure if they are 𝑓 𝑔 (Ker[𝑋 , 𝛼]) = 𝑋 ⧵ ⋂ 𝑔(Rem[𝑋 , 𝛼]) smooth: is the 𝑔-associated incision function for 𝑋. 19 �Definition 12 (Smooth incision function and smooth kernel contraction [6]). An incision function 𝑓 for 𝑋 is smooth if 𝑋 ′ ∩ 𝑓 (Ker[𝑋 , 𝛼]) ≠ ∅ for all 𝑋 ′ ⊆ 𝑋 such that Cn(𝑋 ′ ) ∩ 𝑓 (Ker[𝑋 , 𝛼]) ≠ ∅. A kernel (pseudo-)contrac- tion is smooth if its incision function is smooth. Proposition 13. If 𝑓 is smooth and Cn* satisfies inclu- sion, then the Cn* kernel pseudo-contraction cCn* 𝑓 satisfies relative closure. Proof sketch. If the proposition does not hold, then there must be a sentence 𝛽 ∈ (𝐵 ∩ Cn(cCn* 𝑓 (𝐵, 𝛼))) such that 𝛽 ∉ cCn* 𝑓 (𝐵, 𝛼), and 𝛽 must be in 𝑓 (Ker[Cn*(𝐵), 𝛼]) and in Cn*(𝐵) due to inclusion of Cn*. The set 𝐵′ ∶= Figure 2: Screenshot of Protégé window with the pseudo- 𝐵⧵𝑓 (Ker[Cn*(𝐵), 𝛼]) is such that 𝛽 ∈ Cn(𝐵′ ) from its defi- contraction tab. nition, thus Cn(𝐵′ )∩𝑓 (Ker[Cn*(𝐵), 𝛼]) is non-empty, and smoothness of 𝑓 implies that 𝐵′ ∩ 𝑓 (Ker[Cn*(𝐵), 𝛼]) ≠ ∅, which contradicts the definition of 𝐵′ . • Cn*: the types of consequences that will be gen- The vacuity postulate states that the set should re- erated by the reasoner before the operation; main unchanged if it does not entail the sentence to be • construction: partial meet or kernel; contracted: (vacuity) If 𝛼 ∉ 𝐵, then c(𝐵, 𝛼) = 𝐵. • strategies: methods used to compute the remain- der and kernel sets (see: [22, 23, 24, 25, 20]). Cn* kernel pseudo-contraction does not satisfy vacuity: as shown by [13], it is not satisfied by Cn* partial meet After the user clicks on Run, the program obtains the pseudo-contraction. However, a weaker version of this set Cn*(𝒪) from the original ontology 𝒪 and computes property is satisfied: Rem[Cn*(𝒪), 𝛼] or Ker[Cn*(𝒪), 𝛼], according to the cho- sen construction. The remainders or kernels are then (vacuity*) If 𝛼 ∉ Cn(𝐵), then c(𝐵, 𝛼) = Cn*(𝐵). shown on a dialogue window, where they can be se- lected by the user. The kernel set and the incision func- Proposition 14. If Cn* satisfies subclassicality, an oper- tion discussed in Example 6 are depicted in Figure 3 ation that satisfies inclusion* and core-retainment* also (it contains more kernels than in the example because satisfies vacuity*. the consequence generator Class assertions is more gen- eral than Cn*break and generates the additional sentence Proof sketch. Inclusion* implies that c(𝐵, 𝛼) ⊆ Cn*(𝐵), 𝑠 ∶ 𝐸𝑢𝑟𝑜𝑝𝑒𝑎𝑛). and ⊇ is a consequence of core-retainment* and In all cases, the sentences that will be removed are the assumptions that Cn* is subclassical and Cn is displayed in red. To avoid cluttering the window, Decla- Tarskian. ration sentences and obvious tautologies (such as 𝑎 ∶ ⊤ and 𝐶 ⊑ ⊤) are omitted. After a click on the button 4. Pseudo-contraction plug-in for Execute operation, the plug-in transforms the active on- tology 𝒪 into pmcCn* Cn* 𝑔 (𝒪, 𝛼) or kc𝑓 (𝒪, 𝛼), where Cn* is Protégé: a prototype determined by the selected sentence generators and the chosen remainders or kernel elements define the function We have implemented a prototype of a tool that com- 𝑔 or 𝑓 . putes Cn* (partial meet and kernel) pseudo-contractions. The plug-in is written in Java 8 and supports Protégé The algorithms for obtaining remainder and kernel sets 5.5.0, which is the latest version at the time of writing. It 7 were adapted from Guimarães’ repository [20] . It is a uses OWL API8 4.2.5 to manipulate OWL objects9 . The Protégé plug-in that provides a tab which can be added source code is available on GitLab10 . to the program window. The user can type the sentence to be contracted using Manchester syntax [21] and the 8 traditional notation of Description Logics is displayed 9 http://owlcs.github.io/owlapi/ Version 5.1.17 of OWL API is already available, but it is not sup- below the input field, as shown in Figure 2. ported by Protégé yet, which is why we had to use a previous Besides the sentence 𝛼 to be removed, the user chooses: version. 10 The source code is publicly available in a GitLab repository: https: 7 https://gitlab.com/rfguimaraes/owl-change //gitlab.com/viniciusbm/pseudo-contraction-protege-plugin. 20 � Definition 17 (Optimal repair). A repair 𝒪 ′ of the on- tology 𝒪 with respect to the sentence 𝛼 is an optimal repair if no other repair 𝒪 ″ (of 𝒪 w.r.t. 𝛼) is such that Cn(𝒪𝑠 ∪ 𝒪 ′ ) ⊂ Cn(𝒪𝑠 ∪ 𝒪 ″ ). An optimal classical repair is a classical repair which is optimal in the sense that no classical repair contains it. Unlike optimal repairs, optimal classical repairs always exist. In order to find classical repairs, a construction based on justifications and hitting sets can be used. Justifica- tions are minimal subsets of a base that imply the un- wanted sentence: Definition 18 (Justification [9]). Let 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩ be an ontology and 𝛼 a sentence entailed by 𝒪 but not by 𝒪𝑠 . A justification for 𝛼 in 𝒪 is an inclusion-minimal subset 𝐽 of 𝒪𝑟 such that 𝛼 ∈ Cn(𝒪𝑠 ∪ 𝐽 ). We will denote the set of all justifications for 𝛼 in 𝒪 as Just(𝒪, 𝛼). Figure 3: Screenshot of Protégé window with the kernel set The definition above is often presented without parti- of Example 6. tioning the ontology, which corresponds to a particular case where 𝒪𝑟 = ∅. [26] has proposed an algorithm to debug incoherent ontologies inspired by Reiter’s hitting set tree [22]. Other 5. Ontology Repair authors [9, 24, 11] extended and generalised this algo- Ontology Repair consists in transforming an ontology so rithm to find all justifications for any given entailment. that it does not imply a certain formula. In what follows, Definition 19 (Hitting set [22]). Given a set 𝒥 of justifi- we define the main concepts based on the presentation cations for a sentence in an ontology, a hitting set of 𝒥 is given by [12]. Consider that 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩ is an ontology a set 𝐻 of sentences contained in ⋃ 𝒥 such that 𝐻 ∩ 𝐽 ≠ ∅ consisting of a static and a refutable part (𝒪𝑠 and 𝒪𝑟 , for every 𝐽 ∈ 𝒥. respectively), which are assumed to be disjoint.11 The static part contains the axioms which we want to preserve A repair 𝒪 ′ of 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩ with respect to 𝛼 is ob- when we repair the ontology, while the refutable part tained by computing an inclusion-minimal hitting set contains those which we are willing to give up if needed. 𝐻 of 𝐽 𝑢𝑠𝑡(𝒪, 𝛼) and defining 𝒪 ′ as the set 𝒪𝑟 after the We assume that the separation into static and refutable removal of each sentence in 𝐻. is given. Example 20. Let 𝛼 be the sentence 𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ 𝑃𝑒𝑟𝑠𝑜𝑛. Definition 15 (Repair). Let 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩ be an ontology Consider the knowledge base 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩, where 𝒪𝑠 = and let 𝛼 be a sentence entailed by 𝒪 but not by 𝒪𝑠 . An {𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ 𝐶𝑜𝑚𝑝𝑢𝑡𝑒𝑟𝑃𝑟𝑜𝑔𝑟𝑎𝑚} and ontology 𝒪 ′ is a repair of 𝒪 with respect to 𝛼 if Cn(𝒪𝑠 ∪ 𝒪 ′ ) ⊆ Cn(𝒪) ⧵ {𝛼}. 𝒪𝑟 = {𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟, 𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟, Classically, a repair consists of a subset of the refutable part of the ontology: 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛}. Definition 16 (Classical repair). A repair 𝒪 ′ of the on- In order to obtain a repair of the ontology 𝒪 with re- tology 𝒪 with respect to the sentence 𝛼 is a classical repair spect to 𝛼, we start by computing the set of justifica- if it is contained in 𝒪𝑟 . tions 𝒥, which in this case is {{𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟, 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛}, {𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ In order to preserve as much knowledge as possible, 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟, 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛}}. Then, we look for an optimal repair (which in general does not it obtains a minimal hitting set of 𝒥, which may be exist [12]): the set 𝐻 ∶= {{𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛}}. Lastly, it returns the set obtained by removing from ′ 11 The notation ⟨𝒪𝑠 , 𝒪𝑟 ⟩ is meant to represent the set 𝒪𝑠 ∪ 𝒪𝑟 in a way 𝒪𝑟 the elements of 𝐻, i.e. the set 𝒪 ∶= {𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ that makes it possible to tell if a sentence is in the static part or in 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟, 𝑎𝑙𝑝ℎ𝑎𝑍 𝑒𝑟𝑜 ∶ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟}. the refutable part. 21 � A special case of Ontology Repair is ABox Repair, replacing 𝛽 with 𝛽 ′ is enough to prevent such entailment, where the TBox is fixed, i.e., the TBox is contained in 𝒪𝑠 . and the algorithm stops, returning the repair {𝒪𝑟 ⧵ {𝛽}) ∪ It is easy to see that when 𝒯 = 𝒪𝑠 and 𝒜 = 𝒪𝑟 , an ABox {𝛽 ′ }. repair is an optimal repair according to Definition 17. Previously, we have shown that contraction opera- A modified version of the procedure above was pro- tions in classical Belief Revision are too restrictive for posed by [12] where, instead of weakening each ele- belief bases because of the inclusion postulate, and we ment of the minimal hitting set, only a single formula analysed pseudo-contraction operations — a generalisa- in each justification needs to be changed. Starting with tion of contraction that satisfies logical inclusion rather 𝒪𝑟 = 𝒪 ′ , if 𝛼 ∈ Cn(𝒪𝑠 ∪ 𝒪 ′ ), a single justification 𝐽 for than inclusion. Similarly, in Ontology Repair, classical 𝛼 in 𝒪𝑠 ∪ 𝒪 ′ is computed, and for some arbitrary sen- repairs do not allow the inclusion of new sentences, and tence 𝛽 in 𝐽, we replace it with a weaker 𝛽 ′ such that the same issue is present: sentences are either kept or 𝛼 ∉ Cn (𝒪𝑠 ∪ (𝐽 ⧵ {𝛽}) ∪ {𝛽 ′ }) (as discussed earlier, such removed altogether. In our Example 20, the sentence as 𝛽 ′ always exists). [12] remark that as the unmodi- 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛 was discarded, but we fied version requires the computation of minimal hitting might want to replace it with a less constraining sentence sets, which is expensive, the modified version has an that preserves some of the original information. A very important advantage, even though both may consume similar idea was introduced by [12] in Ontology Repair: exponential time [12]. They are guaranteed to stop after in a gentle repair, one can either remove a sentence or a number of steps that grows at most exponentially in substitute it with a weaker version, retaining part of the the size of the refutable part [12]. information it represented. Definition 21 (Weakening [12]). A sentence 𝛼1 is 6. Correspondence between weaker than a sentence 𝛼2 if Cn({𝛼1 }) ⊂ Cn({𝛼2 }). Belief Revision and Repairs in Definition 22 (Gentle Repair [12]12 ). Let 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩ Description Logics be an ontology and let 𝛼 be a sentence entailed by 𝒪 but not by 𝒪𝑠 . An ontology 𝒪 ′ is a gentle repair of 𝒪 with In this section, we will analyse the close relationship respect to 𝛼 if Cn(𝒪𝑠 ∪ 𝒪 ′ ) ⊆ Cn(𝒪) ⧵ {𝛼} and, for every between the concepts and constructions presented for 𝜑 ∈ 𝒪 ′ , either 𝜑 ∈ 𝒪𝑟 or 𝜑 is weaker than 𝜓 for some Ontology Repair and Belief Revision. 𝜓 ∈ 𝒪𝑟 ⧵ 𝒪 ′ . We start by giving two definitions that generalise sev- eral concepts in the literature. The algorithm that computes a gentle repair is very similar to the procedure described earlier. The only differ- Definition 24 (Maximal Non-Implying Subsets [27]). ence is that 𝒪 ′ is defined by replacing sentences that are Let 𝐵 be a knowledge base, 𝛼 a sentence, and Φ a set in 𝐻 with weaker versions rather than removing them. of static sentences (i.e. which should be preserved in any More specifically, for each 𝛽 that would be removed by operation). The set of maximal 𝛼-non-implying subsets the original algorithm, we replace it with a 𝛽 ′ weaker of 𝐵 with respect to Φ, denoted by MaxNon(𝐵, 𝛼, Φ), is than 𝛽 such that 𝛼 ∉ Cn (𝒪𝑠 ∪ (𝐽 ⧵ {𝛽}) ∪ {𝛽 ′ }) for ev- such that 𝑋 ∈ MaxNon(𝐵, 𝛼, Φ) if and only if 𝑋 ⊆ 𝐵, ery 𝐽 ∈ 𝒥 such that 𝛽 ∈ 𝐽. Such a 𝛽 ′ always exists: a 𝛼 ∉ Cn(Φ ∪ 𝑋 ), and there is no 𝑌 such that 𝑋 ⊂ 𝑌 ⊆ 𝐵 tautology satisfies the requirements (note, though, that and 𝛼 ∉ Cn(Φ ∪ 𝑌 ). replacing a sentence with a tautology is logically equiva- For brevity, we shall omit the last argument of MaxNon lent to removing it, which means that a classical repair is whenever it is empty: MaxNon(𝐵, 𝛼, ∅) is the same as obtained if we only use tautologies). In order to illustrate MaxNon(𝐵, 𝛼). what is different in the outcome of this algorithm, we will use the same example: Remark 25 ([27]). If Φ ⊆ 𝐵, then the maximal 𝛼-non- implying subsets of 𝐵 with respect to Φ contain all of the Example 23. Consider again the problem discussed in elements of Φ, i.e., 𝑋 ⊇ Φ for every 𝑋 ∈ MaxNon(𝐵, 𝛼, Φ). Example 20. Starting with 𝒪 ′ = 𝒪𝑟 , we compute 𝒥 and 𝐻 as before. Then, instead of removing the sentence 𝛽 ∶= Definition 24 corresponds to a remainder if Φ = ∅, i.e., 𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔ 𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛, it is replaced with a MaxNon(𝐵, 𝛼) = Rem[𝐵, 𝛼]. weaker version, such as 𝛽 ′ ∶= (𝐶ℎ𝑒𝑠𝑠𝑃𝑙𝑎𝑦𝑒𝑟 ⊔𝐺𝑜𝑃𝑙𝑎𝑦𝑒𝑟)⊓ Definition 26 (Minimal Implying Subsets [27]). Let 𝐵 ¬𝐶𝑜𝑚𝑝𝑢𝑡𝑒𝑟𝑃𝑟𝑜𝑔𝑟𝑎𝑚 ⊑ 𝑃𝑒𝑟𝑠𝑜𝑛. This procedure is repeated be a knowledge base, 𝛼 a sentence, and Φ a set of static until the set 𝒪𝑠 ∪ 𝒪 ′ fails to entail 𝛼. In our example, sentences. The set of minimal 𝛼-implying subsets of 𝐵 12 In [12], the concept of gentle repair has not been formally defined, with respect to Φ, denoted by MinImp(𝐵, 𝛼, Φ), is such that only explained in intuitive terms. We will use this definition, which 𝑋 ∈ MinImp(𝐵, 𝛼, Φ) if and only if 𝑋 ⊆ 𝐵, 𝛼 ∈ Cn(Φ ∪ 𝑋 ), we proposed in [27]. and there is no 𝑌 ⊂ 𝑋 such that 𝛼 ∈ Cn(Φ ∪ 𝑌 ). 22 � As in the previous definition, the last argument will Proposition 32 (Gentle Repair ⟹ Pseudo- be omitted if empty: MinImp(𝐵, 𝛼) = MinImp(𝐵, 𝛼, ∅). contraction). Let GRep be an operation that yields a gentle repair. Define the operation c(GRep) as Remark 27 ([27]). The minimal 𝛼-implying subsets of 𝐵 with respect to Φ do not contain elements of Φ, i.e., 𝑋 ∩Φ = ∅ for every 𝑋 ∈ MinImp(𝐵, 𝛼, Φ). GRep(⟨∅, 𝐵⟩ , 𝛼), if 𝐵 ⊧ 𝛼; c(GRep) (𝐵, 𝛼) = { 𝐵, otherwise. If Φ = ∅, Definition 26 corresponds to Definition 3, i.e., MinImp(𝐵, 𝛼) = Ker[𝐵, 𝛼]. Moreover, Definition 26 Then, c(GRep) is a pseudo-contraction operation. is closely related to Definition 18: MinImp(𝐵, 𝛼, Φ) = Just(⟨Φ, 𝐵 ⧵ Φ⟩ , 𝛼), or conversely, Just(⟨𝒪𝑠 , 𝒪𝑟 ⟩ , 𝛼) = The result above follows from Definition 22, which MinImp(𝒪𝑠 ∪ 𝒪𝑟 , 𝛼, 𝒪𝑠 ). As shown in [27], the definitions guarantees that c(GRep) satisfies success and logical in- of MaxNon and MinImp also encompass concepts such clusion. as MaNAs (maximal non-axiom sets), MinAs (minimal For the other direction (pseudo-contractions as gentle axiom sets), MISs (minimal inconsistent sets) and argu- repairs), we will introduce general partial meet pseudo- ments [28, 29, 30]. contractions and general kernel pseudo-contractions. We can now analyse the relation between the defi- Pseudo-contractions allow the result to contain some nitions and operations of Belief Revision and Ontology weakened versions of formulae that were originally in Repair. the belief base. This can be achieved by applying a partial Let 𝐵 ⊆ 𝔏 and 𝛼 ∈ 𝔏. The following two properties meet or kernel operation on a “weak closure” of the belief follow straightly from Definition 3 and Definition 18. base [14]. However, as this closure does not depend on the sentence that is being contracted, we cannot add only Proposition 28 (Kernel ∼ Justification [27]). If 𝛼 ∈ weakenings of formulae that would be removed. General Cn(𝐵), then a set 𝑋 is an 𝛼-kernel of 𝐵 with respect to 𝛼 if (partial meet and kernel) pseudo-contractions employ a and only if 𝑋 is a justification for 𝛼 in ⟨∅, 𝐵⟩. consequence operator (Cn**) that depends on both the The set of those sets, which we denote by set of beliefs and the input sentence. Before defining MinImp(𝐵, 𝛼), unifies the concepts of the following them, we need the following concepts: proposition: Definition 33 (Extension of a selection function [32, Remark 29 (Kernel set ∼ Set of all justifications [27]). adapted]). Let 𝑔 be a selection function for 𝐵, and let 𝐵 ⊆ ∗ ′ ∗ If a sentence 𝛼 and a set 𝐵 are such that 𝛼 ∈ Cn(𝐵), then 𝐵 ⊆ 𝔏. We say that a selection function 𝑔 for 𝐵 is an ∗ ′ extension of 𝑔 to 𝐵 if 𝑔 is such that for every 𝛼 ∈ 𝔏 and Ker[𝐵, 𝛼] = Just(⟨∅, 𝐵⟩ , 𝛼). 𝑋 ∈ 𝑔(MaxNon(𝐵, 𝛼)) there is a 𝑌 ∈ 𝑔 ′ (MaxNon(𝐵∗ , 𝛼)) A classical repair (Definition 16) can be seen as a con- such that 𝑋 ⊆ 𝑌. traction operation that satisfies two of Hansson’s postu- lates for base contraction (success and inclusion) [27]. Definition 34 (Extension of an incision function). Let 𝑓 The following proposition, which is an immediate con- be an incision function for a set of sentences 𝐵, and let 𝐵 ⊆ ∗ ′ ∗ sequence of the upper bound property [31], will be useful 𝐵 ⊆ 𝔏. The incision function 𝑓 for 𝐵 is an extension ∗ ′ ∗ ∗ to show the connection between partial meet base con- of 𝑓 for 𝐵 if 𝑓 (MinImp(𝐵 , 𝛼)) ⊇ 𝑓 (MinImp(𝐵 , 𝛼)) for traction and classical repairs. all sentences 𝛼. Proposition 30 (Existence of 𝛼-remainder preserving 𝒪𝑠 The general partial meet pseudo-contraction13 was [27]). Let 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩ be an ontology and 𝛼 be a sentence proposed by [32] and generalised by [14] as a way to entailed by 𝒪 but not by 𝒪𝑠 . Then, there is at least one weaken sentences in belief base pseudo-contractions, in- 𝛼-remainder 𝑋 of 𝒪𝑠 ∪ 𝒪𝑟 such that 𝒪𝑠 ⊆ 𝑋. stead of removing them: Now we can show that partial meet base contractions Definition 35 (General partial meet pseudo-contrac- that include the static part of the ontology yield classical tion). [32, 14] Let 𝛼 ∈ 𝔏, 𝐵 ⊆ 𝔏, Cn’ be a conse- repairs. quence relation, and 𝑔 be a selection function for 𝐵. Let us define Cn**(𝐵, 𝛼) ∶= Cn’(𝐵 ⧵ ⋂ 𝑔(MaxNon(𝐵, 𝛼))) ∪ Theorem 31 (Partial meet base contraction ⟹ Classi- 𝐵, and let 𝑔 ′ be an extension of 𝑔 to Cn**(𝐵, 𝛼). cal repair [27]). Under the conditions of Proposition 30, if The general partial meet pseudo-contraction of 𝐵 by 𝑔 is such that 𝒪𝑠 ⊆ 𝑋 for every 𝑋 ∈ 𝑔(Rem[𝒪, 𝛼]), then the 𝛼, denoted by gpmcCn**′ (𝐵, 𝛼), is defined as the set 𝑔,𝑔 operation Rep𝑔 defined as Rep𝑔 (𝒪, 𝛼) = pmc𝑔 (𝒪, 𝛼) ⧵ 𝒪𝑠 ⋂ 𝑔 ′ (MaxNon(Cn**(𝐵, 𝛼), 𝛼)). yields a classical repair. 13 In [27], this operation was referred to as “two-place partial meet We can now show the relationship between pseudo- pseudo-contraction”, which in [14] refers to a more general type contractions and gentle repairs. of operations. 23 � We will use a similar idea to define the general kernel cCn** (𝐵, 𝛽) = ∅ and Cn**(𝐵) ∶= 𝐵 ∪ Cn’(𝐵 ⧵ c(𝐵, 𝛽)) for pseudo-contraction: all sentences 𝛽 and the consequence relation Cn’ is mono- tonic, subclassical and strictly weakening. If the ontology Definition 36 (General kernel pseudo-contraction). Let 𝒪 ∶= ⟨𝒪𝑠 , 𝒪𝑟 ⟩ is such that 𝒪𝑠 ⊆ c(𝒪, 𝛽) ∩ cCn** (𝒪, 𝛽) for 𝛼 ∈ 𝔏, 𝐵 ⊆ 𝔏, Cn’ be a consequence relation, and 𝑓 be all sentences 𝛽 and 𝛼 is a sentence such that 𝛼 ∉ Cn(𝒪𝑠 ), an incision function for 𝐵. Let us define Cn**(𝐵, 𝛼) ∶= then the set 𝒪 ′ ∶= cCn** (𝒪, 𝛼) ⧵ 𝒪𝑠 is a gentle repair of 𝒪 𝐵 ∪ Cn’(𝑓 (MinImp(𝐵, 𝛼))), and let 𝑓 ′ be an extension of with respect to 𝛼. 𝑓 to Cn**(𝐵, 𝛼). The general kernel pseudo-contraction of 𝐵 by 𝛼, denoted by gkcCn** 𝑓 ,𝑓 ′ (𝐵, 𝛼), is defined as the set Proof sketch. Using monotonicity, inclusion and idempo- Cn**(𝐵, 𝛼) ⧵ 𝑓 ′ (MinImp(Cn**(𝐵, 𝛼), 𝛼)). tence of Cn, and also subclassicality of Cn’ and success of cCn** , we can show that 𝒪 ′ is a repair, and the extra Consider the following properties for selection and condition required for it to be a gentle repair is derived incision functions: from the assumption that Cn’ is strictly weakening. Definition 37 (𝐴-inclusion [27]). Let 𝐵 ⊆ 𝔏, and let Theorem 42 (When a general partial meet pseudo- 𝐴 ⊆ 𝐵. A selection function 𝑔 for 𝐵 satisfies 𝐴-inclusion if, contraction is a gentle repair [27, adapted]). Let for all 𝛼 ∉ Cn(𝐴), 𝐴 ⊆ 𝑋 for every 𝑋 ∈ 𝑔(MaxNon(𝐵, 𝛼)). gpmcCn**′ and Cn** be as in Definition 35, Cn** based 𝑔,𝑔 on a consequence relation Cn’ that satisfies subclassical- Definition 38 (𝐴-exclusion). Let 𝐵 ⊆ 𝔏, and let 𝐴 ⊆ ity, 𝑔 and 𝑔 ′ satisfy 𝒪𝑠 -inclusion, Cn’ be monotonic and 𝐵. An incision function 𝑓 for 𝐵 satisfies 𝐴-exclusion if strictly weakening, and 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩. If 𝛼 ∉ Cn(𝒪𝑠 ), then 𝐴 ∩ 𝑓 (MinImp(𝐵, 𝛼)) = ∅ for all 𝛼 ∉ Cn(𝐴). 𝒪 ′ ∶= gpmcCn** 𝑔,𝑔 ′ (𝒪, 𝛼) ⧵ 𝒪𝑠 is a gentle repair of 𝒪 w.r.t. 𝛼. Intuitively, a selection function (for 𝐵) that satisfies 𝐴-inclusion only selects 𝛼-remainders that preserve 𝐴, Proof sketch. The result Cn** follows from Lemma 41 by tak- Cn** . unless 𝛼 itself is entailed by 𝐴, in which case 𝐴 cannot be a ing pmc 𝑔 as c and gpmc 𝑔,𝑔 ′ as c subset of any 𝛼-remainder; similarly, an incision function Theorem 43 (When a general kernel pseudo-contraction (for 𝐵) that satisfies 𝐴-exclusion only selects sentences is a gentle repair). Let gkcCn** 𝑓 ,𝑓 ′ and Cn** be as in Defini- that are not in 𝐴, preserving 𝐴 in the operation, unless 𝛼 is entailed by 𝐴, in which case it is impossible to have tion 36, Cn** based on a consequence relation Cn’ that ′ an incision function that does not contain elements of 𝐴. satisfies subclassicality, 𝑓 and 𝑓 satisfy 𝒪𝑠 -exclusion, Cn’ be monotonic and strictly weakening, and 𝒪 = ⟨𝒪𝑠 , 𝒪𝑟 ⟩. Lemma 39. Consider a general partial meet pseudo-con- If 𝛼 ∉ Cn(𝒪𝑠 ), then 𝒪 ′ ∶= gkcCn** 𝑓 ,𝑓 ′ (𝒪, 𝛼) ⧵ 𝒪𝑠 is a gentle traction defined as in Definition 35. For every sentence 𝜑 repair of 𝒪 w.r.t. 𝛼. in 𝐵 ⧵ ⋂ 𝑔(MaxNon(𝐵, 𝛼)), there is a set 𝑋 such that 𝑋 ∈ 𝑔 ′ (MaxNon(Cn**(𝐵, 𝛼), 𝛼)) and 𝜑 ∉ 𝑋. Proof sketch. The result follows from Lemma 41 by tak- ing kc𝑓 as c and gkcCn** 𝑓 ,𝑓 ′ as cCn** . Proof sketch. The conditions imply the existence of a set 𝑌 ∈ 𝑔(MaxNon(𝐵, 𝛼)) such that 𝜑 ∉ 𝑌. Since 𝑔 ′ is an extension of 𝑔 to Cn**(𝐵, 𝛼), there is an 𝑋 ∈ 7. Conclusions 𝑔 ′ (MaxNon(Cn**(𝐵, 𝛼), 𝛼)) such that 𝑌 ⊆ 𝑋, and such 𝑋 cannot contain 𝜑 due to the definition of remainder. In this paper, we have introduced a construction for pseudo-contraction based on kernel contraction, and we If a consequence operator returns only sentences that have characterised it by means of a representation theo- are in the given set or are weaker than some of its sen- rem. Furthermore, we have implemented a prototype of tences, then we say it is strictly weakening: a tool that computes Cn* partial meet and kernel pseudo- contractions, built upon existing software that computes Definition 40 (Strictly weakening operator [27]). A con- remainder and kernel sets. Lastly, we have analysed the sequence operator Con is strictly weakening if, for every similarities between some concepts and definitions of 𝜑 ∈ 𝔏 and every 𝐵 ⊆ 𝔏, 𝜑 ∈ Con(𝐵) if and only if 𝜑 ∈ 𝐵 Belief Revision and Ontology Repair (more specifically, or Con({𝜑}) ⊂ Con({𝜓 }) for some 𝜓 ∈ 𝐵. pseudo-contractions and gentle repairs, respectively), ex- tending previous work [27] and showing that the new Now we can show under which conditions a general operation that we have introduced is also connected to (partial meet or kernel) pseudo-contraction yields a gen- gentle repairs. The last two theorems show that gentle tle repair. repairs can be constructed by restricted forms of pseudo- Lemma 41. Let c be a contraction operation for a set contraction. One question that remains is whether we of sentences 𝐵. Let cCn** be a pseudo-contraction opera- need these restrictions from the point of view of Ontol- tion such that cCn** (𝐵, 𝛽) ⊆ Cn**(𝐵), where (𝐵 ⧵ c(𝐵, 𝛽)) ∩ ogy Repair, i.e., whether it makes sense to define more 24 �general forms of repair that lie in between gentle and in: S. Zhang, M. Wirsing, Z. Zhang (Eds.), Knowl- classical repairs. edge Science, Engineering and Management - 8th In the future, we would like to evaluate the perfor- International Conference, KSEM 2015, Chongqing, mance of pseudo-contractions in both artificial and real- China, October 28–30, 2015, Proceedings, volume world ontologies in order to compare the practical effi- 9403 of Lecture Notes in Computer Science, Springer, ciency of the constructions. In particular, it would be 2015, pp. 28–39. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 3 1 9 - 2 5 1 5 9 - 2 _ 3 . useful to apply the operations to benchmarks designed [9] A. Kalyanpur, Debugging and Repair of OWL On- for ontology repair problems such as [33]. tologies, Ph.D. thesis, University of Maryland at Also, we think it would be relevant to explore families College Park, College Park, MD, USA, 2006. of Cn* consequence operators that are interesting for [10] Q. Ji, P. Haase, G. Qi, P. Hitzler, S. Stadtmüller, theoretical or practical purposes. As an example, we can RaDON – repair and diagnosis in ontology net- think of approximations as defined in [34] as generating works, in: Proceedings of the 6th European Se- consequences in less expressive logics. mantic Web Conference on The Semantic Web: Research and Applications, ESWC 2009 Herak- lion, Springer-Verlag, Berlin, Heidelberg, 2009, pp. Acknowledgments 863–867. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 6 4 2 - 0 2 1 2 1 - 3 _ 7 1 . [11] M. Horridge, Justification based explanation in on- The authors of this work would like to thank the Center tologies, Ph.D. thesis, University of Manchester, for Artificial Intelligence (C4AI-USP) and the support 2011. from the São Paulo Research Foundation (FAPESP grant [12] F. Baader, F. Kriegel, A. Nuradiansyah, R. Peñaloza, #2019/07665-4) and from the IBM Corporation. Making repairs in description logics more gentle, The first author was supported by the Brazilian Na- in: M. Thielscher, F. Toni, F. Wolter (Eds.), Princi- tional Council for Scientific and Technological Develop- ples of Knowledge Representation and Reasoning: ment (CNPq grant 131803/2018-2). Proceedings of the Sixteenth International Confer- ence, KR 2018, Tempe, Arizona, 30 October — 2 References November 2018., AAAI Press, 2018, pp. 319–328. [13] Y. D. Santos, Pseudo-Contractions in Belief Revi- [1] C. Alchourrón, P. Gärdenfors, D. Makinson, On the sion, Master’s thesis, Universidade de São Paulo, logic of theory change: Partial meet contraction 2016. and revision functions, Journal of Symbolic Logic [14] Y. D. Santos, V. B. Matos, M. M. Ribeiro, R. Wasser- 50 (1985) 510–530. mann, Partial meet pseudo-contractions, Interna- [2] G. Flouris, D. Plexousakis, G. Antoniou, On apply- tional Journal of Approximate Reasoning 103 (2018) ing the AGM theory to DLs and OWL., in: Proceed- 11–27. doi:1 0 . 1 0 1 6 / j . i j a r . 2 0 1 8 . 0 8 . 0 0 6 . ings of the International Semantic Web Conference, [15] V. B. Matos, Pseudo-contraction Oper- 2005, pp. 216–231. ations for Description Logics, Master’s [3] M. M. Ribeiro, R. Wassermann, Base revision for thesis, Universidade de São Paulo, 2021. ontology debugging, Journal of Logic and Computa- doi:1 0 . 1 1 6 0 6 / D . 4 5 . 2 0 2 1 . t d e - 0 2 0 9 2 0 2 1 - 1 3 1 7 5 0 , tion 19 (2009) 721–743. doi:1 0 . 1 0 9 3 / l o g c o m / e x n 0 4 8 . available at https://www.teses.usp.br/teses/ [4] R. Wassermann, On AGM for non-classical logics, J. disponiveis/45/45134/tde-02092021-131750/en.php. Philosophical Logic 40 (2011) 271–294. doi:1 0 . 1 0 0 7 / [16] S. O. Hansson, Changes of disjunctively closed s10992- 011- 9178- 2. bases, Journal of Logic, Language and Information [5] S. O. Hansson, New operators for theory change, 2 (1993) 255–284. Theoria 55 (1989) 114–132. [17] Y. D. Santos, M. M. Ribeiro, R. Wassermann, Be- [6] S. O. Hansson, Kernel contraction, The Journal of tween belief bases and belief sets: Partial meet Symbolic Logic 59 (1994) 845–859. contraction, in: R. Booth, G. Casini, S. Klarman, [7] D. Lembo, M. Lenzerini, R. Rosati, M. Ruzzi, D. F. G. Richard, I. J. Varzinczak (Eds.), Proceedings of Savo, Inconsistency-tolerant semantics for descrip- the International Workshop on Defeasible and Am- tion logics, in: P. Hitzler, T. Lukasiewicz (Eds.), Web pliative Reasoning, DARe 2015, co-located with the Reasoning and Rule Systems - Fourth International 24th International Joint Conference on Artificial Conference, RR 2010, Bressanone/Brixen, Italy, Intelligence (IJCAI 2015), Buenos Aires, Argentina, September 22-24, 2010. Proceedings, volume 6333 July 27, 2015, volume 1423 of CEUR Workshop Pro- of Lecture Notes in Computer Science, Springer, 2010, ceedings, CEUR-WS.org, 2015, pp. 50–56. pp. 103–117. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 6 4 2 - 1 5 9 1 8 - 3 _ 9 . [18] M. A. Falappa, E. L. Fermé, G. Kern-Isberner, On the [8] J. Du, G. Qi, Tractable computation of representa- logic of theory change: Relations between incision tive ABox repairs in description logic ontologies, and selection functions, in: G. Brewka, S. Corade- 25 � schi, A. Perini, P. Traverso (Eds.), Proceedings of C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter the 17th European Conference on Artificial Intel- (Eds.), Description Logic, Theory Combination, and ligence (ECAI 2006), Riva del Garda, Italy, August All That - Essays Dedicated to Franz Baader on the 29—September 1, 2006, volume 141 of Frontiers in Occasion of His 60th Birthday, volume 11560 of Lec- Artificial Intelligence and Applications, IOS Press, ture Notes in Computer Science, Springer, 2019, pp. 2006, pp. 402–406. 385–403. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 0 3 0 - 2 2 1 0 2 - 7 _ 1 8 . [19] S. O. Hansson, Belief contraction without recovery, [28] F. Baader, R. Peñaloza, Axiom pinpointing in gen- Studia Logica 50 (1991) 251–260. URL: https://doi. eral tableaux, in: N. Olivetti (Ed.), Automated Rea- org/10.1007/BF00370186. doi:1 0 . 1 0 0 7 / B F 0 0 3 7 0 1 8 6 . soning with Analytic Tableaux and Related Meth- [20] R. F. Guimarães, Modularity in belief change of ods, Springer Berlin Heidelberg, Berlin, Heidelberg, description logic bases, Ph.D. thesis, Universidade 2007, pp. 11–27. de São Paulo, São Paulo, 2020. doi:h t t p s : / / d o i . o r g / [29] J. Fang, Z. Huang, Reasoning with inconsistent on- 10.11606/T.45.2020.tde- 19032020- 043422. tologies, Tsinghua Science & Technology 15 (2010) [21] M. Horridge, N. Drummond, J. Goodwin, A. L. Rec- 687–691. doi:1 0 . 1 0 1 6 / S 1 0 0 7 - 0 2 1 4 ( 1 0 ) 7 0 1 1 6 - 4 . tor, R. Stevens, H. Wang, The Manchester OWL [30] P. Besnard, A. Hunter, A logic-based theory of de- syntax, in: B. C. Grau, P. Hitzler, C. Shankey, E. Wal- ductive arguments, Artif. Intell. 128 (2001) 203–235. lace (Eds.), Proceedings of the OWLED*06 Work- doi:1 0 . 1 0 1 6 / S 0 0 0 4 - 3 7 0 2 ( 0 1 ) 0 0 0 7 1 - 6 . shop on OWL: Experiences and Directions, Athens, [31] C. Alchourrón, D. Makinson, New studies in De- Georgia, USA, November 10-11, 2006, volume 216 ontic Logic, Reidel Publishing Company, 1981, pp. of CEUR Workshop Proceedings, CEUR-WS.org, 2006, 125–148. pp. 52–62. [32] M. M. Ribeiro, R. Wassermann, Degrees of re- [22] R. Reiter, A theory of diagnosis from first principles, covery and inclusion in belief base dynamics, in: Artificial Intelligence 32 (1987) 57–95. doi:1 0 . 1 0 1 6 / M. Pagnucco, M. Thielscher (Eds.), Proceedings 0004- 3702(87)90062- 2. of the Twelfth International Workshop on Non- [23] R. Wassermann, An algorithm for belief revision, Monotonic Reasoning, Sydney, 2008, pp. 43–49. in: A. G. Cohn, F. Giunchiglia, B. Selman (Eds.), KR [33] Q. Ji, W. Li, S. Zhou, G. Qi, Y. Li, Benchmark con- 2000, Principles of Knowledge Representation and struction and experimental evaluations for inco- Reasoning Proceedings of the Seventh International herent ontologies, Knowledge-Based Systems 239 Conference, Breckenridge, Colorado, USA, April (2022). 11–15, 2000, Morgan Kaufmann, 2000, pp. 345–352. [34] A. Bötcher, C. Lutz, F. Wolter, Ontology approxima- [24] A. Kalyanpur, B. Parsia, M. Horridge, E. Sirin, Find- tion in horn description logics, in: Proceedings of ing all justifications of OWL DL entailments, in: the Twenty-Eighth International Joint Conference Proceedings of the 6th International Semantic Web on Artificial Intelligence, IJCAI 2019, Macao, China, Conference (ISWC 2007), Busan, Korea, Novem- 2019, pp. 1574–1580. ber 11—15, 2007, volume 4825 of Lecture Notes in Computer Science, Springer, 2007, pp. 267–280. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 5 4 0 - 7 6 2 9 8 - 0 _ 2 0 . [25] R. Cóbe, R. Wassermann, Ontology repair through partial meet contraction, in: R. Booth, G. Casini, S. Klarman, G. Richard, I. J. Varzinczak (Eds.), Pro- ceedings of the International Workshop on Defea- sible and Ampliative Reasoning, DARe 2015, co- located with the 24th International Joint Confer- ence on Artificial Intelligence (IJCAI 2015), Buenos Aires, Argentina, July 27, 2015., volume 1423 of CEUR Workshop Proceedings, CEUR-WS.org, 2015, pp. 9–15. [26] S. Schlobach, Debugging and semantic clarification by pinpointing, in: Proceedings of the 2nd Euro- pean Semantic Web Conference (ESWC 2005), Her- aklion, Crete, Greece, May 29 – June 1, 2005, volume 3532 of Lecture Notes in Computer Science, Springer, 2005, pp. 226–240. doi:1 0 . 1 0 0 7 / 1 1 4 3 1 0 5 3 _ 1 6 . [27] V. B. Matos, R. F. Guimarães, Y. D. Santos, R. Wasser- mann, Pseudo-contractions as gentle repairs, in: 26 �