Vol-3197/paper2
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
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
οΏ½