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).
Belief Revision is a research area that deals with problems
related to changing knowledge bases or logical theories,
especially in the face of new, possibly conflicting,
information. The work of Alchourrón, Gärdenfors, and
Makinson [
The AGM paradigm defines three change operations
lief; contraction, which removes a belief; and revision,
which incorporates a new belief retaining consistency.
tracting beliefs, thus contraction operations and their
variations. In a contraction operation, a sentence must
be removed from a set and must not be entailed by the
contracted set. Some of the minimal requirements for an
operation to be a belief contraction are that it satisfies
success — the removed set is not entailed anymore — and
inclusion — no new beliefs are added [5]. There are two
main constructions associated to contraction operations:
partial meet contraction [
The area of Ontology Repair groups together tools ontologies and getting rid of unwanted inferences. Different approaches have been proposed, depending on which parts of the knowledge base one wants to change
Both in Belief Revision and in Ontology Repair,
classical approaches assume that no information can be added
to a knowledge base when we perform the task of
removmay be reasonable, it is usually formalised as a syntactic
of too much information. The assumption can be
formalised as a less restrictive constraint which only states
base, thus allowing to add sentences that were logically
entailed by the original set. Note that this
formalisation still captures the intuition that no new information
should be added, but “information” is now seen as
independent from the syntax. This idea has been proposed
and developed in both areas in the last decades, with
diferent terminologies and notations. In Belief Revision,
satisfy some assumptions, such as compactness, mono- and formal definitions related to the task of debugging
the belief sets. Over the past decades, the AGM theory
has been adapted to belief bases (sets of sentences that are
not necessarily closed) represented in diferent logical
represented by sets closed under logical consequences, [
CEUR (R. Wassermann) (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 and new consequences are not allowed [12]. Attribution 4.0 International (CC BY 4.0).
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 consequences 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, logiclassical 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 constraints. 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 pseudo-contractions and presents some definitions that Definition 2 (Pseudo-contraction [16]). An operation will be used throughout the paper. In Section 3, we de- c is a pseudo-contraction if c satisfies success and logical ifne our new operation (Cn* kernel pseudo-contraction), inclusion. 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 2. Pseudo-contraction Operations fragments of first-order logic. Thus, the operations we will present do not assume any other syntactic or semanContractions 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 sentence ¬ 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 . Subclasbelief 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 pseudoformulae, which can be seen as an argument against its contraction constructions that depend on the kind of foruse 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.
The properties of pseudo-contraction constructions depend on the properties that are satisfied by Cn*, especially inclusion and subclassicality: if both are satisifed, then Cn* is in an intermediate level between the Definition 3 (Kernel and kernel set [6]). Let ⊆
and ∈ . The kernel set of with respect to , denoted by Ker[, ] , is such that a set is in Ker[, ] if ⊆ , ∈
Cn( ) , and there is no ⊂ if and only 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*() should always be finite if is finite, but we will not assume this restriction. sequences that will be generated. Each configuration can ally subclassical4. Since they are syntactically restricted, be seen as a Cn*, which satisfies inclusion 3 and is usu- (Ker[, ]) ∩ ≠ ∅ such as Protégé5, as shown in Figure 1. they are good examples of weak consequence operators.
Those reasoners can be embedded in ontology editors,
and Fact++2 — allow the user to choose the types of con- function is an incision function6 for if, for every Definition 4 (Incision function [6]). Let ⊆ . A
We will show later (Proposition 28) that the definition above is related to that of justification (Definition
18), which is well-known in Ontology Repair. ∈ , it is the case that (Ker[, ]) ⊆ ⋃ Ker[, ]
and for every non-empty ∈
Ker[, ] .
Definition 5 (Cn* kernel pseudo-contraction). Let be a set of sentences, Cn* a consequence relation and an incision function for Cn*() . The Cn* kernel pseudocontraction of by a sentence , denoted by kcCn*(, ) , is such that, for all sentences :
kcCn*(, ) =
Cn*() ⧵ (Ker[Cn*(), ]).
The following examples illustrate this construction:
where
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
operator that “breaks conjunctions into conjuncts”, originally
presented in [
. We 2 = ⊓ ⊑
∃ℎ .{ℎ}, 1 = ℎ
⊑ , 3 = ∶ ⊓ ℎ, 3′ = ∶ 3″ = ∶ ℎ.
and 3′.
If the definition of the incision function is such that (Ker[Cn*break(), ]) = { operation is kcCn*break(, ) =
( ⧵ 3) ∪ { 3′}, i.e., the pseudo-contraction replaces 3 with its weaker version
In order to characterise this operation, we will need a starred version of some postulates: (inclusion*) c(, ) ⊆
In this section, we will present a pseudo-contraction operation that is defined as a kernel contraction starting from the expanded set Cn*() . 3One step after the window shown in Figure 1, users can choose whether the original sentences should be kept. 4Except, maybe, for some highly-complex ontologies that cannot be represented in classical logic. contraction kcCn*.
lowing proposition shows the explicit construction: Proposition 10. If pmcCn* is a Cn* partial meet pseudocontraction, then it is equivalent to the Cn* kernel pseudotion. We can rewrite it as follows: Proof. Let pmcCn* be a Cn* partial meet pseudo-contrac
pmcCn*(, ) = ⋂ (Rem[Cn*(), ]) = Cn*() ⧵ (Ker[ , ]) = kcCn*(, ),
= Cn*() ⧵ [Cn*() ⧵
⋂ (Rem[Cn*(), ]) ] where is the incision function defined as in DefiniPostulates-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
as (Ker[Cn*(), ]) ∶= ifned incision function for kcCn* and cCn* are equivalent.
Cn*() and the operations Cn*() ⧵ cCn*(, ) is a well-de- lent to a partial meet contraction. By taking Cn* as the
identity function, Cn* partial meet and kernel pseudo
Cn* partial meet pseudo-contraction, a pseudo-con- alent. Therefore, Cn* kernel pseudo-contractions may tation theorem). If Cn* satisfies monotonicity, then an operation is a Cn* kernel pseudo-contraction if and only if it satisfies success, inclusion*, core-retainment* and uniformity*.
Proof sketch. Construction-to-postulates: Success can be shown by contradiction: if ∈
Cn(kc
Cn*(, )) , then the fact that Cn is Tarskian implies that there is some non-empty ∈
Ker[Cn*() ⧵ (Ker[Cn*(), ]), ]
, and such
must be in Ker[Cn*(), ] , but this implies that (Ker[Cn*(), ]) ∩ = ∅
, violating the definition of incision function. Inclusion* and core-retainment follow directly from the definitions. For uniformity*, if and satisfy the antecedent but not the consequent, then there must be some ∈
Ker[Cn*(), ] ⧵
Ker[Cn*(), ] ∉ (w.l.o.g., swapping and for the other case); thus, either
Cn( ) or there is some ′ ⊊ such that ∈
Cn( ′), and neither can hold because ∈
Ker[Cn*(), ] . by pmcCn*(, ) entail . traction construction that “closes” the set under Cn* before applying a classical partial meet contraction, was proposed by [13]. The result of the operation, denoted
, is obtained by taking the intersection of the output of a selection function that chooses some elements (at least one) of Rem[Cn*(), ] , which is the
Cn* partial meet pseudo-contractions satisfy releretainment*; moreover, the other three postulates are identical (success, inclusion* and uniformity*). Hence, every Cn* partial meet pseudo-contraction is also a Cn* kernel pseudo-contraction. We will now show how to obtain the explicit construction of a Cn* kernel pseudocontraction from a Cn* partial meet pseudo-contraction.
This will use the definition of an incision function derived from a selection function: Definition 8 (Incision function associated to a selection function [18]). Let be a selection function for . The function defined as (Ker[ , ]) = ⧵
⋂ (Rem[ , ]) is the -associated incision function for . set of all inclusion-maximal subsets of Cn*() that do not then the following property holds: vance*, and Cn* kernel pseudo-contractions satisfy core- there is a ′ such that ′ ⊆ Cn() and ∈ Cn( ′ ∪ {}) ⧵ (core-retainment*) If ∈ Cn*()⧵ c(, ) , then there is some ′ ⊆ Cn*() such that ∈
Cn( ′ ∪ {}) ⧵ Cn( ′).
The representation theorem follows.
an incision function for .
Theorem 9. [18] The function (as in Definition 8) is
As mentioned earlier, Cn* kernel pseudo-contraction Theorem 7 (Cn* kernel pseudo-contraction: represen- subsumes Cn* partial meet pseudo-contraction. The fol
In general, not every kernel contraction is equivacontractions become partial meet and kernel contractions for belief bases, which means that they are not equivnot have the same properties as Cn* partial meet pseudocontractions.
Since inclusion* implies logical inclusion for every subclassical Cn* [14], we can see that a Cn* kernel pseudocontraction is indeed a pseudo-contraction as long as Cn* satisfies subclassicality. If Cn* also satisfies inclusion, (logical core-retainment) If ∈ ⧵
c(, ) , then Cn( ′).
Observation 11. If Cn* satisfies subclassicality and inclusion, then any operation that satisfies core-retainment* also satisfies logical core-retainment.
A desirable property that is not necessarily satisfied by kernel contractions (hence, not always satisfied by Cn* kernel pseudo-contractions) is relative closure [19]: (relative closure) ∩ Cn(c(, )) ⊆
c(, ) .
Nonetheless, kernel contractions and Cn* kernel pseudo-contractions satisfy relative closure if they are smooth: Definition 12
(Smooth incision function and smooth kernel contraction [6]). An incision function for is smooth if ′ ∩ (Ker[ , ]) ≠ ∅ Cn( ′) ∩ (Ker[ , ]) ≠ ∅
for all ′ ⊆ such that . A kernel (pseudo-)contraction is smooth if its incision function is smooth.
Proposition 13. If is smooth and Cn* satisfies inclusion, then the Cn* kernel pseudo-contraction cCn* satisfies relative closure.
in Cn*() Proof sketch. If the proposition does not hold, then there must be a sentence ∈ ( ∩
Cn(cCn*(, ))) ∉ cCn*(, ) , and must be in (Ker[Cn*(), ])
and due to inclusion of Cn*. ⧵ (Ker[Cn*(), ]) is such that ∈ nition, thus Cn( ′)∩ (Ker[Cn*(), ]) which contradicts the definition of ′. smoothness of implies that ′ ∩ (Ker[Cn*(), ]) ≠ ∅ ,
The set ′ ∶=
is non-empty, and
The vacuity postulate states that the set should remain unchanged if it does not entail the sentence to be contracted: (vacuity) If ∉ , then c(, ) = .
Cn* kernel pseudo-contraction does not satisfy vacuity: as shown by [13], it is not satisfied by Cn* partial meet pseudo-contraction. However, a weaker version of this property is satisfied: (vacuity*) If ∉ Cn() , then c(, ) = 5.5.0, which is the latest version at the time of writing. It uses OWL API8 4.2.5 to manipulate OWL objects9. The 8http://owlcs.github.io/owlapi/ 9Version 5.1.17 of OWL API is already available, but it is not supported by Protégé yet, which is why we had to use a previous version. 10The source code is publicly available in a GitLab repository: https: //gitlab.com/viniciusbm/pseudo-contraction-protege-plugin.
Ontology Repair consists in transforming an ontology so that it does not imply a certain formula. In what follows, Definition 19 (Hitting set [22]). Given a set of justifiwe 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 obwhen 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.
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.
Justifications are minimal subsets of a base that imply the
unwanted sentence:
Definition 18 (Justification [
The definition above is often presented without partitioning 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
authors [
Example 20. Let be the sentence ℎ ∶ .
Consider the knowledge base = ⟨ , ⟩, where = {ℎ ∶ } and Definition 15 (Repair). Let = ⟨ , ⟩ be an ontology and let be a sentence entailed by but not by . An 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: = {ℎ ∶ ℎ , ℎ ∶ , ℎ ⊔ ⊑ }. 11The notation ⟨ , ⟩ is meant to represent the set ∪ in a way that makes it possible to tell if a sentence is in the static part or in the refutable part.
Definition 16 (Classical repair). A repair ′ of the on- In order to obtain a repair of the ontology with retology with respect to the sentence is a classical repair spect to , we start by computing the set of justificaif 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 the elements of , i.e. the set ′ ∶= {ℎ ∶ ℎ , ℎ ∶ } .
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 protions in classical Belief Revision are too restrictive for posed by [12] where, instead of weakening each elebelief 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 senrepairs 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 ifed 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 22 (Gentle Repair [12]12). Let = ⟨ , ⟩ be an ontology and let be a sentence entailed by but not by . An ontology ′ is a gentle repair of with respect to if Cn( ∪ ′) ⊆ Cn( ) ⧵ { } and, for every ∈ ′, either ∈ or is weaker than for some ∈ ⧵ ′.
The algorithm that computes a gentle repair is very similar to the procedure described earlier. The only diference is that ′ is defined by replacing sentences that are in with weaker versions rather than removing them. More specifically, for each that would be removed by the original algorithm, we replace it with a ′ weaker than such that ∉ Cn ( ∪ ( ⧵ {}) ∪ { ′}) for every ∈ such that ∈ . Such a ′ always exists: a tautology satisfies the requirements (note, though, that replacing a sentence with a tautology is logically equivalent to removing it, which means that a classical repair is obtained if we only use tautologies). In order to illustrate what is diferent in the outcome of this algorithm, we will use the same example: Example 23. Consider again the problem discussed in Example 20. Starting with ′ = , we compute and as before. Then, instead of removing the sentence ∶= ℎ ⊔ ⊑ , it is replaced with a weaker version, such as ′ ∶= (ℎ ⊔ )⊓ ¬ ⊑ . This procedure is repeated until the set ∪ ′ fails to entail . In our example, 12In [12], the concept of gentle repair has not been formally defined, only explained in intuitive terms. We will use this definition, which we proposed in [27].
In this section, we will analyse the close relationship between the concepts and constructions presented for Ontology Repair and Belief Revision.
We start by giving two definitions that generalise several concepts in the literature.
Definition 24 (Maximal Non-Implying Subsets [27]).
Let be a knowledge base, a sentence, and Φ a set of static sentences (i.e. which should be preserved in any operation). The set of maximal -non-implying subsets of with respect to Φ, denoted by MaxNon(, , Φ) , is such that ∈ MaxNon(, , Φ) if and only if ⊆ , ∉ Cn(Φ ∪ ) , and there is no such that ⊂ ⊆ and ∉ Cn(Φ ∪ ) .
For brevity, we shall omit the last argument of MaxNon whenever it is empty: MaxNon(, , ∅) is the same as MaxNon(, ) .
Remark 25 ([27]). If Φ ⊆ , then the maximal -nonimplying subsets of with respect to Φ contain all of the elements of Φ, i.e., ⊇ Φ for every ∈ MaxNon(, , Φ) .
Definition 24 corresponds to a remainder if Φ = ∅, i.e., MaxNon(, ) = Rem[, ] .
Definition 26 (Minimal Implying Subsets [27]). Let be a knowledge base, a sentence, and Φ a set of static sentences. The set of minimal -implying subsets of with respect to Φ, denoted by MinImp(, , Φ) , is such that ∈ MinImp(, , Φ) if and only if ⊆ , ∈ Cn(Φ ∪ ) , and there is no ⊂ such that ∈ Cn(Φ ∪ ) . As in the previous definition, the last argument will
Proposition 32 (Gentle Repair ⟹
Pseudobe omitted if empty: MinImp(, ) =
MinImp(, , ∅) .
contraction). Let GRep be an operation that yields a gentle axiom sets), MISs (minimal inconsistent sets) and argu- repairs), we will introduce general partial meet pseudoRemark 27 ([27]). The minimal -implying subsets of with respect to Φ do not contain elements of Φ, i.e., ∩Φ = ∅ for every ∈
MinImp(, , Φ) .
If Φ = ∅, Definition
26 corresponds to Definition 3, i.e., MinImp(, ) =
Ker[, ] . Moreover, Definition 26 is closely related to Definition 18:
MinImp(, , Φ) = Just(⟨Φ, ⧵ Φ ⟩ , ) , or conversely, Just(⟨ , ⟩ , ) = MinImp( ∪ , ,
). As shown in [27], the definitions
of MaxNon and MinImp also encompass concepts such
as MaNAs (maximal non-axiom sets), MinAs (minimal
ments [
We can now analyse the relation between the definitions and operations of Belief Revision and Ontology Repair.
Let ⊆
and ∈ . The following two properties follow straightly from Definition 3 and Definition 18.
Proposition 28 (Kernel ∼ Justification [ 27]). If ∈ Cn() , then a set is an -kernel of with respect to if and only if is a justification for in ⟨∅, ⟩.
The set of those sets,
which we denote by MinImp(, ) , unifies the concepts of the following proposition: Remark 29 (Kernel set ∼ Set of all justifications [ 27]). adapted]). Let be a selection function for , and let ⊆ repair. Define the operation c(GRep) as c(GRep)(, ) = { , GRep(⟨∅, ⟩ , ), if ⊧ ; otherwise.
Then, c(GRep) is a pseudo-contraction operation. clusion.
The result above follows from Definition
22, which guarantees that c(GRep) satisfies success and logical in
For the other direction (pseudo-contractions as gentle contractions and general kernel pseudo-contractions.
Pseudo-contractions allow the result to contain some weakened versions of formulae that were originally in the belief base. This can be achieved by applying a partial meet or kernel operation on a “weak closure” of the belief base [14]. However, as this closure does not depend on the sentence that is being contracted, we cannot add only weakenings of formulae that would be removed. General (partial meet and kernel) pseudo-contractions employ a consequence operator (Cn**) that depends on both the set of beliefs and the input sentence. Before defining them, we need the following concepts: Definition 33 (Extension of a selection function [32, extension of to ∗ if ′ is such that for every ∈ ∗ ⊆ . We say that a selection function ′ for ∗ is an
and ∈ (MaxNon(, ))
there is a ∈ ′(MaxNon( ∗, )) Definition 34 (Extension of an incision function). Let If a sentence and a set are such that ∈
Cn() , then
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 to show the connection between partial meet base con- of for ∗ if ′(MinImp( ∗, )) ⊇ (MinImp( ∗, )) for ′ for ∗ is an extension traction and classical repairs.
[27]). Let = entailed by ⟨ , ⟩ be an ontology and be a sentence but not by . Then, there is at least one -remainder of ∪ such that ⊆ .
Now we can show that partial meet base contractions that include the static part of the ontology yield classical repairs. yields a classical repair. operation Rep defined as Rep ( , ) = Theorem 31 (Partial meet base contraction cal repair [27]). Under the conditions of Proposition 30, if is such that ⊆ for every ∈ (Rem[ , ]) , then the pmc ( , ) ⧵
We can now show the relationship between pseudocontractions and gentle repairs. all sentences .
proposed by [32] and generalised by [14] as a way to weaken sentences in belief base pseudo-contractions, instead of removing them: Definition 35
(General partial meet pseudo-contraction). [32, 14] Let ∈ , ⊆ , Cn’ be a consequence relation, and be a selection function for . Let us define
Cn**(, ) ∶=
Cn’( ⧵ ⋂ (MaxNon(, ))) ∪ ⋂ ′(MaxNon(Cn**(, ), )) .
The general partial meet pseudo-contraction of by , denoted by gpmcC,n*′*(, ) , is defined as the set 13In [27], this operation was referred to as “two-place partial meet pseudo-contraction”, which in [14] refers to a more general type of operations. ⟹
to Cn**(, ) .
We will use a similar idea to define the general kernel pseudo-contraction: Definition 36 (General kernel pseudo-contraction). Let ∈ , ⊆ , Cn’ be a consequence relation, and be an incision function for . Let us define Cn**(, ) ∶= ∪ Cn’( (MinImp(, ))) , and let ′ be an extension of to Cn**(, ) . The general kernel pseudo-contraction of by , denoted by gkcC,n*′*(, ) , is defined as the set Cn**(, ) ⧵ ′(MinImp(Cn**(, ), )) cCn**(, ) = ∅ and Cn**() ∶= ∪ Cn’( ⧵ c(, )) for all sentences and the consequence relation Cn’ is monotonic, subclassical and strictly weakening. If the ontology ∶= ⟨ , ⟩ is such that ⊆ c( , ) ∩ cCn**( , ) for all sentences and is a sentence such that ∉ Cn( ), then the set ′ ∶= cCn**( , ) ⧵ is a gentle repair of with respect to .
Proof sketch. Using monotonicity, inclusion and idempotence of Cn, and also subclassicality of Cn’ and success of cCn**, we can show that ′ is a repair, and the extra condition required for it to be a gentle repair is derived 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(, )) . gpmcC,n*′* and Cn** be as in Definition 35, Cn** based Definition 38 ( -exclusion). Let ⊆ , and let ⊆ on a consequence relation Cn’ that satisfies subclassical . An incision function for satisfies -exclusion if ity, and ′ satisfy -inclusion, Cn’ be monotonic and ∩ (MinImp(, )) = ∅ for all ∉ Cn() . strictly weakening, and = ⟨ , ⟩. If ∉ Cn( ), then ′ ∶= gpmcC,n*′*( , ) ⧵ 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 follows from Lemma 41 by takunless itself is entailed by , in which case cannot be a ing pmc as c and gpmcC,n*′* as cCn**. 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 gkcC,n*′* and Cn** be as in Definithat 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 ′ ∶= gkcC,n*′*( , ) ⧵ 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 taking kc as c and gkcC,n*′* 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 ∈ ′(MaxNon(Cn**(, ), )) such that ⊆ , and such cannot contain due to the definition of remainder.
Lemma 41. Let c be a contraction operation for a set of sentences . Let cCn** be a pseudo-contraction operation such that cCn**(, ) ⊆ Cn**() , where ( ⧵ c(, ) )∩ 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 theoare 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 pseudocontractions, 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
Now we can show under which conditions a general tending previous work [27] and showing that the new (partial meet or kernel) pseudo-contraction yields a gen- operation that we have introduced is also connected to gentle repairs. The last two theorems show that gentle tle repair. repairs can be constructed by restricted forms of pseudocontraction. One question that remains is whether we need these restrictions from the point of view of Ontology Repair, i.e., whether it makes sense to define more general forms of repair that lie in between gentle and in: S. Zhang, M. Wirsing, Z. Zhang (Eds.), Knowlclassical 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 efi- 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 [
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 [
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 .
[
The first author was supported by the Brazilian Na- in: M. Thielscher, F. Toni, F. Wolter (Eds.),
Princitional Council for Scientific and Technological Develop- ples of Knowledge Representation and Reasoning:
ment (CNPq grant 131803/2018-2). Proceedings of the Sixteenth International
Conference, 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[
Philosophical Logic 40 (2011) 271–294. doi:1 0 . 1 0 0 7 / [16] S. O. Hansson, Changes of disjunctively closed s 1 0 9 9 2 - 0 1 1 - 9 1 7 8 - 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. [
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 Amtion 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 Proof 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