Vol-3197/paper2

From BITPlan ceur-ws Wiki
Jump to navigation Jump to search

Paper

Paper
edit
description  scientific paper published in CEUR-WS Volume 3197
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

load PDF

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
�