## A General Katsuno-Mendelzon-Style Characterization of AGMBelief Base Revision for Arbitrary Monotonic Logics
Faiq Miftakhul Falakh 1 , Sebastian Rudolph 1 , Kai Sauerwald 2
1 Computational Logic Group, TU Dresden, Germany
2 Knowledge Based Systems Group, FernUniversit¨ at in Hagen, Germany
{ faiq miftakhul.falakh, sebastian.rudolph } @tu-dresden.de, kai.sauerwald@fernuni-hagen.de
Important note: This article constitutes a preliminary report, which was found to contain inaccuracies. It is superseded by a significantly generalized, extended, and revised treatise by the same authors made available on arXiv.org under the title Semantic Characterizations of General Belief Base Revision on the 27th of December 2021 via https://arxiv.org/abs/2112.13557.
## Abstract
The AGM postulates by Alchourr´ on, G¨ ardenfors, and Makinson continue to represent a cornerstone in research related to belief change. We generalize the approach of Katsuno and Mendelzon (KM) for characterizing AGM base revision from propositional logic to the setting of (multiple) base revision in arbitrary monotonic logics. Our core result is a representation theorem using the assignment of total - yet not transitive - 'preference' relations to belief bases. We also provide a characterization of all logics for which our result can be strengthened to preorder assignments (as in KM's original work).
## 1 Introduction
The question how a rational agent should change her beliefs in the light of new information is crucial to AI systems. It gave rise to the area of belief change , which has been massively influenced by the AGM paradigm of Alchourr´ on, G¨ ardenfors, and Makinson [2]. The AGM theory assumes that an agent's beliefs are represented by a deductively closed set of formulas (aka belief set). A change operator for belief sets is required to satisfy appropriate postulates in order to qualify as a rational change operator. While the contribution of AGM is widely accepted as solid and inspiring foundation, it lacks support for certain relevant aspects: it provides no immediate solution on how to deal with multiple inputs (i.e., several formulae instead of just one), with bases (i.e., arbitrary finite collections of formulae, not necessarily deductively closed), or with the problem of iterated belief changes.
While the AGM paradigm is axiomatic, much of its success originated from operationalisations via representation theorems. Yet, most existing characterisations of AGM revision require the underlying logic to fulfil the AGM assumptions, including compactness, closure under standard connectives, deduction, and supra-classicality [18].
Leaving the safe grounds of these assumptions complicates matters; representation theorems do not easily generalize to arbitrary monotonic logics. This has sparked investigations into tailored characterisations of AGM belief change for specific logics, such as Horn logic [5], temporal logics [3], action logics [19], first-order logic [21], and description logics [15,9,7]. More general approaches to revision in non-classical logics were given by Ribeiro, Wassermann et al. [18,16,17], Delgrande et al. [6], Pardo et al. [14], or Aiguier et al. [1].
In this paper, we consider (multiple) revision of finite bases in arbitrary monotonic logics, refining and generalizing the popular approach by Katsuno and Mendelzon [12] (KM) for propositional belief base revision. KM start out from finite belief bases, assigning to each a total preorder on the interpretations, which expresses - intuitively speaking - a degree of 'modelishness'. The models of the result of any AGM revision will then coincide with the preferred (i.e., preorderminimal) models of the received information.
Our approach generalises this idea of preferences over interpretations to the general setting, which necessitates adjusting the nature of the 'modelishness-indicating' assignments: transitivity needs to be waived, whereas certain natural requirements regarding minimality need to be imposed.
The main contributions of this paper are the following:
- We extend KM's semantic approach from the setting of singular revision in propositional logic to multiple revision of finite bases in arbitrary monotone logics.
- For this setting, we provide a representation theorem characterizing AGM belief change operators via assignments.
- We characterize those logics for which every AGM operator can even be captured by preorder assignments (i.e., in the classical KM way). In particular, this condition applies to all logics supporting disjunction over sentences.
## 2 Preliminaries
We consider arbitrary logics L with monotonic modeltheoretic semantics. Syntactically, such logics are described by a (possibly infinite) set L of sentences . A belief base K
is then a finite 1 subset of L , that is K ∈ P fin ( L ) . Unlike in other belief revision frameworks, we impose no further requirements on L (such as closure under certain operators).
A model theory for L is defined in the classical way through a (potentially infinite) class Ω of interpretations (also called worlds ) and a binary relation /satisfies between Ω and L where ω /satisfies ϕ indicates that ω is a model of ϕ . Hence, a logic L is specified by the triple ( L , Ω , /satisfies ) . We let /llbracket ϕ /rrbracket = { ω ∈ Ω | ω /satisfies ϕ } denote the set of all models of ϕ ∈ L and obtain the models of a belief base K via /llbracket K /rrbracket = ⋂ ϕ ∈K /llbracket ϕ /rrbracket . A sentence or belief base is consistent if it has a model and inconsistent otherwise. Logical entailment is defined as usual (overloading the symbol ' /satisfies ') via models: for two belief bases K and K ′ we say K entails K ′ (written K /satisfies K ′ ) if /llbracket K /rrbracket ⊆ /llbracket K ′ /rrbracket . Note that this definition of the semantics enforces that L is monotonic. 2 As usual we write K ≡ K ′ to express /llbracket K /rrbracket = /llbracket K ′ /rrbracket . A multiple base change operator for L is a function ◦ : P fin ( L ) × P fin ( L ) → P fin ( L ) . For convenience, we henceforth drop 'multiple' and simply speak of base change operators instead.
We will endow the interpretation space Ω with some structure. A binary relation /precedesequal over Ω is total if, for any ω 1 , ω 2 ∈ Ω , at least one of ω 1 /precedesequal ω 2 or ω 2 /precedesequal ω 1 holds. We write ω 1 ≺ ω 2 for ω 1 /precedesequal ω 2 and ω 2 /negationslash/precedesequal ω 1 . For Ω ′ ⊆ Ω , ω ∈ Ω ′ is called /precedesequal -minimal in Ω ′ if ω /precedesequal ω ′ for all ω ′ ∈ Ω ′ . 3 We let min(Ω ′ , /precedesequal ) denote the set of /precedesequal -minimal interpretations in Ω ′ . We call /precedesequal a preorder , if it is transitive and reflexive.
## 3 Base Revision in Propositional Logic
A well-known and by now popular characterization of base revision has been described by Katsuno and Mendelzon [12] for the special case of propositional logic. KM's approach hinges on several properties of propositional logics. To start with, any propositional belief base K can be written as a single propositional formula ∧ α ∈K α . Consequently, in their approach, belief bases are represented by single formulas. They provide the following set of postulates, derived from the AGM revision postulates, where ϕ, ϕ 1 , ϕ 2 , α , and β are propositional formulae:
- (KM1) ϕ ◦ α /satisfies α .
- (KM2) If ϕ ∧ α is consistent, then ϕ ◦ α ≡ ϕ ∧ α .
- (KM3) If α is consistent, then ϕ ◦ α is consistent.
- (KM4) If ϕ 1 ≡ ϕ 2 and α ≡ β , then ϕ 1 ◦ α ≡ ϕ 2 ◦ β .
- (KM5) ( ϕ ◦ α ) ∧ β /satisfies ϕ ◦ ( α ∧ β ) .
- (KM6) If ( ϕ ◦ α ) ∧ β is consistent, then ϕ ◦ ( α ∧ β ) /satisfies ( ϕ ◦ α ) ∧ β .
One key contribution of KM is to provide an alternative characterization of those propositional base revision operators satisfying (KM1)-(KM6) by model-theoretic means, i.e. through comparisons between propositional interpretations.
1 The term base is sometimes also used for arbitrary sets [8]. We follow the mainstream in computer science and assume finite bases.
2 From here on, when simply speaking of 'logic', we always assume the classical, monotonic setting described here. From now on, we also assume a logic L = ( L , Ω , /satisfies ) as given and fixed.
3 If /precedesequal is total, this definition is equivalent to the absence of any ω ′′ ∈ Ω ′ with ω ′′ ≺ ω .
In the following, we present their results in a formulation that facilitates later generalization. One central notion for the characterization is the notion of faithful assignment.
Definition 1 (assignment, faithful) . An assignment (for L ) is a function /precedesequal ( . ) : P fin ( L ) →P (Ω × Ω) that assigns to each belief base K a total binary relation /precedesequal K over Ω . An assignment /precedesequal ( . ) is called faithful if it satisfies the following conditions:
- (F1) If ω, ω ′ /satisfies K , then ω ≺ K ω ′ does not hold.
/negationslash
- (F2) If ω /satisfies K and ω ′ /satisfies K , then ω ≺ K ω ′ .
- (F3) If K ≡ K ′ , then /precedesequal K = /precedesequal K ′ .
An assignment /precedesequal ( . ) is called a preorder assignment if /precedesequal K is a preorder for every K ∈ P fin ( L ) .
Intuitively, faithful assignments provide information which of the two interpretations is 'closer to K -modelhood'. Consequently, the actual K -models are /precedesequal K -minimal. The next definition captures the idea of an assignment adequately representing the behaviour of a revision operator.
Definition 2 (compatible) . A base change operator ◦ is called compatible with some assignment /precedesequal ( . ) if it satisfies /llbracket K◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal K ) for all belief bases K and Γ .
With these notions in place, KM's representation result can be smoothly expressed as follows:
Theorem 1 (Katsuno and Mendelzon [12]) . In propositional logic, a base change operator ◦ satisfies (KM1)-(KM6) iff it is compatible with some faithful preorder assignment.
## 4 The Approach
In this section, we prepare our main result by transferring KM's concepts from propositional logic to our general setting. As mentioned, KM's characterization hinges on features of propositional logic that do not generally hold. So far, attempts to find similarly elegant formulations for less restrictive logics have made good progress to the benefit of the understanding the nature of AGM revision, yet, none of them capture the very general case considered here (cf. Section 8).
For our presentation, we use the following straightforward reformulation of (KM1)-(KM6):
- (G1) K◦ Γ /satisfies Γ .
- (G2) If /llbracket K∪ Γ /rrbracket = ∅ then K◦ Γ ≡ K∪ Γ .
/negationslash
- (G3) If /llbracket Γ /rrbracket = ∅ then /llbracket K◦ Γ /rrbracket = ∅ .
/negationslash
/negationslash
- (G4) If K 1 ≡ K 2 and Γ 1 ≡ Γ 2 then K 1 ◦ Γ 1 ≡ K 2 ◦ Γ 2 .
- (G5) ( K◦ Γ 1 ) ∪ Γ 2 /satisfies K◦ (Γ 1 ∪ Γ 2 ) .
/negationslash
- (G6) If /llbracket ( K◦ Γ 1 ) ∪ Γ 2 /rrbracket = ∅ then K◦ (Γ 1 ∪ Γ 2 ) /satisfies ( K◦ Γ 1 ) ∪ Γ 2 .
This set of postulates was first given by Qi et al. [15] in the context of belief base revision specifically for Description Logics, yet, the formulation is generic and perfectly suitable for our general setting, too. We can see that (G1)-(G6) tightly correspond to (KM1)-(KM6), respectively. One advantage of this presentation is that it does not require L to support conjunction (while, of course, conjunction on the sentence level is still implicitly supported via set union of bases).
When switching from the setting of propositional to arbitrary logics, two obstacles become apparent.
Observation 1. Transitivity in the relation, as required in Theorem 1, is a too strict property for certain logics.
In fact, it has been observed before that the incompatibility between transitivity and KM's approach already arises for propositional Horn logic [5]. However, for our result, we need to retain totality as well as a new weaker property (which would come for free with transitivity present) defined next.
Definition 3 (min-retractive) . A binary relation /precedesequal over Ω is called min-retractive (for L ) if for every Γ ∈ P fin ( L ) and ω ′ , ω ∈ /llbracket Γ /rrbracket with ω ′ /precedesequal ω and ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ) holds ω ′ ∈ min( /llbracket Γ /rrbracket , /precedesequal ) .
In particular, min-retractivity prevents elements lying on a strict cycle being equivalent to minimal elements.
Observation 2. For arbitrary monotonic logics, the minimum from Definition 2, required in Theorem 1, might be empty.
Thus, one missing ingredient when going to the general case is that of min-completeness , defined next.
Definition 4 (min-complete) . A binary relation /precedesequal over Ω is called min-complete (for L ) if for every Γ ∈ P fin ( L ) with /llbracket Γ /rrbracket = ∅ holds min( /llbracket Γ /rrbracket , /precedesequal ) = ∅ .
/negationslash
/negationslash
In the special case of /precedesequal being transitive and total, mincompleteness trivially holds whenever Ω is finite (as, e.g., in the case of propositional logic). In the infinite case, however, it might need to be explicitly imposed, as already noted earlier [6] (cf. also the notion of limit assumption by Lewis [13]). If /precedesequal is total but not transitive, min-completeness can be violated even in the finite setting through strict cyclic relationships.
We conveniently unite the two properties into one notion.
Definition 5 (min-friendly) . A binary relation /precedesequal over Ω is called min-friendly (for L ) if it is both min-retractive and min-complete. An assignment /precedesequal ( . ) : P fin ( L ) → P (Ω × Ω) is called min-friendly if /precedesequal K is min-friendly for all K ∈ P fin ( L ) .
## 5 The Representation Theorem
We are now ready to generalize KM's representation theorem from propositional to arbitrary monotonic logics, by employing the notion of compatible min-friendly faithful assignments.
Theorem 2. A base change operator ◦ satisfies (G1)-(G6) iff it is compatible with some min-friendly faithful assignment.
We show Theorem 2 in three steps. First, we provide a canonical way of obtaining an assignment for a given revision operator. Next, we show that our construction indeed yields a min-friendly faithful assignment that is compatible with the revision operator. Finally, we show that the notion of min-friendly compatible assignment is adequate to capture the class of base revision operators satisfying (G1)-(G6).
## 5.1 From Postulates to Assignments
Unfortunately, established methods for obtaining a canonical encoding of the revision strategy of ◦ , like the elegant one by Darwiche and Pearl [4], do not generalize well beyond propositional logic. We suggest the following construction, which we consider one of this paper's core contributions.
Definition 6. Let ◦ be a base change operator and K ∈ P fin ( L ) a belief base. The relation /precedesequal ◦ K over Ω is defined by
/negationslash
<!-- formula-not-decoded -->
<!-- formula-not-decoded -->
Intuitively, according to the relation /precedesequal ◦ K , an interpretation ω 1 is 'at least as K -modelish as' an interpretation ω 2 if every change either justifies that ω 1 is more preferred than ω 2 or the change yields no information about the preference. This construction is strong enough for always obtaining a relation that is total and reflexive.
Lemma 3 (totality) . If ◦ satisfies (G5) and (G6), the relation /precedesequal ◦ K is total (and hence reflexive) for every K ∈ P fin ( L ) .
/negationslash
/negationslash
Proof. For totality assume the contrary, i.e. there are /precedesequal ◦ K -incomparable ω 1 and ω 2 . Due to Definition 6, there must exist Γ 1 , Γ 2 ∈ P fin ( L ) with ω 1 , ω 2 /satisfies Γ 1 and ω 1 , ω 2 /satisfies Γ 2 , such that ω 1 /satisfies K◦ Γ 1 and ω 2 /satisfies K◦ Γ 1 as well as ω 1 /satisfies K◦ Γ 2 and ω 2 /satisfies K ◦ Γ 2 . From (G6) follows ω 1 , ω 2 /satisfies K ◦ (Γ 1 ∪ Γ 2 ) . This is a contradiction to (G5), which demands ω 1 , ω 2 /satisfies K◦ (Γ 1 ∪ Γ 2 ) .
/negationslash
Reflexivity follows immediately from totality.
Next comes an auxiliary lemma about belief bases and /precedesequal ◦ K . Lemma 4. Let ◦ satisfy (G5) and (G6) and let K ∈ P fin ( L ) .
/negationslash
- (a) If ω 1 /negationslash/precedesequal ◦ K ω 2 , then ω 2 ≺ ◦ K ω 1 and there exists some Γ with ω 1 , ω 2 /satisfies Γ as well as ω 2 /satisfies K◦ Γ and ω 1 /satisfies K◦ Γ .
- (b) If there is a Γ with ω 1 , ω 2 /satisfies Γ such that ω 1 /satisfies K◦ Γ , then ω 1 /precedesequal ◦ K ω 2 .
/negationslash
- (c) If there is a Γ with ω 1 , ω 2 /satisfies Γ such that ω 1 /satisfies K◦ Γ and ω 2 /satisfies K◦ Γ , then ω 1 ≺ ◦ K ω 2 .
Proof. For the proofs of all statements, recall that by Lemma 3, the relation /precedesequal ◦ K is total.
/negationslash
(b) Let Γ and ω 1 , ω 2 be as assumed. For a contradiction, suppose ω 1 /negationslash/precedesequal ◦ K ω 2 . Then, by part (a) above, there is a Γ ′ with ω 1 , ω 2 /satisfies Γ ′ , ω 1 /satisfies K◦ Γ ′ and ω 2 /satisfies K◦ Γ ′ . Thus ω 1 and ω 2 ensure consistency of ( K◦ Γ) ∪ Γ ′ and ( K◦ Γ ′ ) ∪ Γ , respectively. Using (G5) and (G6) we obtain K◦ (Γ ∪ Γ ′ ) ≡ ( K◦ Γ ′ ) ∪ Γ and K ◦ (Γ ∪ Γ ′ ) ≡ ( K ◦ Γ) ∪ Γ ′ . A contradiction, because we obtained ω 1 /satisfies K◦ (Γ ∪ Γ ′ ) and ω 1 /satisfies K◦ (Γ ∪ Γ ′ ) .
/negationslash
- (c) By Definition 6, the existence of Γ implies ω 2 /negationslash/precedesequal ◦ K ω 1 . Then, totality yields ω 1 /precedesequal ◦ K ω 2 and hence ω 1 ≺ ◦ K ω 2 .
Lemma 5 (compatibility) . If ◦ satisfies (G1), (G3), (G5), and (G6), then it is compatible with /precedesequal ◦ ( . ) .
Proof. We have to show that /llbracket K ◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . For any inconsistent Γ , the statement is straightforward, since, by (G1), /llbracket K◦ Γ /rrbracket = ∅ = min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . In the following, we assume consistency of Γ , showing inclusion in both directions.
(a) By totality, we obtain ω 2 /precedesequal ◦ K ω 1 . First assume there is no Γ with ω 1 , ω 2 /satisfies Γ . Then, ω 1 /precedesequal ◦ K ω 2 by Definition 6. Contradiction. Hence, there must be a Γ with ω 1 , ω 2 /satisfies Γ . Toward a contradiction suppose that, for each Γ with ω 1 , ω 2 /satisfies Γ , we have ω 1 /satisfies K◦ Γ and ω 2 /satisfies K◦ Γ . Then by Definition 6, we would gain ω 1 /precedesequal ◦ K ω 2 ; again a contradiction.
/negationslash
/negationslash
( ⊇ ). Let ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . By consistency of Γ and (G3), there exists an ω ′ ∈ /llbracket K◦ Γ /rrbracket . From the ( ⊆ )-proof follows ω ′ ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . Then, by (G1) and Lemma 4(b), we obtain ω ′ /precedesequal ◦ K ω from ω ∈ /llbracket Γ /rrbracket and ω ′ ∈ /llbracket Γ /rrbracket and ω ′ ∈ /llbracket K◦ Γ /rrbracket . From ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) and ω ′ ∈ /llbracket Γ /rrbracket follows ω /precedesequal ◦ K ω ′ , therefore, by Definition 6, ω, ω ′ ∈ /llbracket Γ /rrbracket and ω ′ ∈ /llbracket K ◦ Γ /rrbracket enforce ω ∈ /llbracket K ◦ Γ /rrbracket . Concluding, we find that every ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) also satisfies ω ∈ /llbracket K◦ Γ /rrbracket , as desired.
( ⊆ ). From consistency of Γ and (G3), we have that /llbracket K ◦ Γ /rrbracket = ∅ . Hence, there exists some ω ∈ /llbracket K◦ Γ /rrbracket . Moreover, for any such ω , by (G1), ω ∈ /llbracket Γ /rrbracket . But then, using Lemma 4(b), we can conclude ω /precedesequal ◦ K ω ′ for any ω ′ ∈ /llbracket Γ /rrbracket . Consequently, any ω ∈ /llbracket K◦ Γ /rrbracket also satisfies ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) .
Lemma 6 (min-friendliness) . If ◦ satisfies (G1), (G3), (G5), and (G6), then /precedesequal ◦ K is min-friendly for every K ∈ P fin ( L ) .
Proof. Observe that min-completeness is a consequence of (G3) and the compatibility of /precedesequal ◦ ( . ) with ◦ from Lemma 5.
/negationslash
For min-retractivity, suppose toward a contradiction that it didn't hold. Because /precedesequal ◦ K is total, that means there is a belief base Γ and interpretations ω ′ , ω /satisfies Γ with ω ′ /precedesequal ◦ K ω and ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) but ω ′ /negationslash∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . From Lemma 5 we obtain ω /satisfies K◦ Γ and ω ′ /satisfies K◦ Γ . Now, applying Lemma 4(c) yields ω ≺ ◦ K ω ′ . A contradiction to ω ′ /precedesequal ◦ K ω .
Lemma 7 (faithfulness) . If ◦ satisfies (G2), (G4), (G5), and (G6), the assignment /precedesequal ◦ ( . ) is faithful.
Proof. We show satisfaction of the three conditions of faithfulness, (F1)-(F3).
(F1). Let ω, ω ′ ∈ /llbracket K /rrbracket . By (G2) we obtain /llbracket K◦K /rrbracket = /llbracket K /rrbracket . Using Lemma 4 we have ω ′ /precedesequal ◦ K ω . This implies ω /negationslash≺ ◦ K ω ′ .
(F3). Let K ≡ K ′ (i.e. /llbracket K /rrbracket = /llbracket K ′ /rrbracket ). From Definition 6 and (G4) follows /precedesequal ◦ K = /precedesequal ◦ K ′ , i.e., ω 1 /precedesequal ◦ K ω 2 iff ω 1 /precedesequal ◦ K ′ ω 2 .
- (F2). Let ω ∈ /llbracket K /rrbracket and ω ′ /negationslash∈ /llbracket K /rrbracket . We get /llbracket K ◦ K /rrbracket = /llbracket K /rrbracket from (G2). Then Lemma 4 implies ω /precedesequal ◦ K ω ′ and ω ′ /negationslash/precedesequal ◦ K ω .
The previous lemmas can finally be put to use to show that the construction of /precedesequal ◦ ( . ) according to Definition 6 yields an assignment with the desired properties.
Proposition 8. If ◦ satisfies (G1)-(G6), then /precedesequal ◦ ( . ) is a minfriendly faithful assignment compatible with ◦ .
Proof. Assume (G1)-(G6) are satisfied by ◦ . Then /precedesequal ◦ ( . ) is an assignment since every /precedesequal K is total by Lemma 3; it is minfriendly by Lemma 6; it is faithful by Lemma 7; and it is compatible with ◦ by Lemma 5.
## 5.2 From Assignments to Postulates
Now, it remains to show the 'if' direction of Theorem 2.
Proposition 9. If there exists a min-friendly faithful assignment /precedesequal ( . ) compatible with ◦ , then ◦ satisfies (G1)-(G6).
Proof. Let /precedesequal ( . ) : K ↦→/precedesequal K be as described. We now show that ◦ satisfies all of (G1)-(G6).
(G1). Let ω ∈ /llbracket K ◦ Γ /rrbracket . Since /llbracket K ◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal K ) , we have that ω ∈ min( /llbracket Γ /rrbracket , /precedesequal K ) . Then, we also have that ω ∈ /llbracket Γ /rrbracket . Thus, we have that /llbracket K◦ Γ /rrbracket ⊆ /llbracket Γ /rrbracket as desired.
/negationslash
/negationslash
(G2). Assume /llbracket K ∪ Γ /rrbracket = ∅ . By faithfulness, this implies /llbracket K /rrbracket = min(Ω , /precedesequal K ) . Thus /llbracket K ∪ Γ /rrbracket = min( /llbracket K ∪ Γ /rrbracket , /precedesequal K ) = min( /llbracket Γ /rrbracket , /precedesequal K ) = /llbracket K◦ Γ /rrbracket .
/negationslash
(G3). Assume /llbracket Γ /rrbracket = ∅ . By min-completeness, we have min( /llbracket Γ /rrbracket , /precedesequal K ) = ∅ . Since /llbracket K◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal K ) by compatibility, we obtain /llbracket K◦ Γ /rrbracket = ∅ .
/negationslash
(G4). Suppose there exist K 1 , K 2 , Γ 1 , Γ 2 ∈ P fin ( L ) with K 1 ≡ K 2 and Γ 1 ≡ Γ 2 . Then, /llbracket K 1 /rrbracket = /llbracket K 2 /rrbracket and /llbracket Γ 1 /rrbracket = /llbracket Γ 2 /rrbracket . From (F3), we conclude /precedesequal K 1 = /precedesequal K 2 . Now suppose that there exists ω ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K 1 ) (consequently ω ∈ /llbracket K 1 ◦ Γ 1 /rrbracket ). Then ω ∈ /llbracket Γ 1 /rrbracket and also ω ∈ /llbracket Γ 2 /rrbracket . Therefore, ω ∈ min( /llbracket Γ 2 /rrbracket , /precedesequal K 2 ) (consequently ω ∈ /llbracket K 2 ◦ Γ 2 /rrbracket ). Thus, /llbracket K 1 ◦ Γ 1 /rrbracket ⊆ /llbracket K 2 ◦ Γ 2 /rrbracket holds. Inclusion in the other direction follows by symmetry. Therefore, we have K 1 ◦ Γ 1 ≡ K 2 ◦ Γ 2 .
/negationslash
(G6). Let ( K◦ Γ 1 ) ∪ Γ 2 = ∅ , thus ω ′ ∈ /llbracket ( K◦ Γ 1 ) ∪ Γ 2 /rrbracket = /llbracket K◦ Γ 1 /rrbracket ∩ /llbracket Γ 2 /rrbracket for some ω ′ . By compatibility, we then obtain ω ′ ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) . Now consider an arbitrary ω with ω ∈ /llbracket K◦ (Γ 1 ∪ Γ 2 ) /rrbracket . By compatibility we obtain ω ∈ min( /llbracket Γ 1 ∪ Γ 2 /rrbracket , /precedesequal K ) and therefore, since ω ′ ∈ /llbracket Γ 1 /rrbracket ∩ /llbracket Γ 2 /rrbracket = /llbracket Γ 1 ∪ Γ 2 /rrbracket , we can conclude ω /precedesequal K ω ′ . This and ω ′ ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) imply ω ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) by min-retractivity. Hence every ω ∈ /llbracket K◦ (Γ 1 ∪ Γ 2 ) /rrbracket satisfies ω ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) = /llbracket K◦ Γ 1 /rrbracket but also ω ∈ /llbracket Γ 2 /rrbracket , whence /llbracket K ◦ (Γ 1 ∪ Γ 2 ) /rrbracket ⊆ /llbracket K ◦ Γ 1 /rrbracket ∩ /llbracket Γ 2 /rrbracket = /llbracket ( K◦ Γ 1 ) ∪ Γ 2 /rrbracket as desired.
(G5). If ( K◦ Γ 1 ) ∪ Γ 2 is inconsistent, the postulate follows trivially. Now assume that /llbracket K◦ Γ 1 /rrbracket ∩ /llbracket Γ 2 /rrbracket = ∅ , i.e., there is an ω with ω ∈ /llbracket K◦ Γ 1 /rrbracket ∩ /llbracket Γ 2 /rrbracket . Since /llbracket K◦ Γ 1 /rrbracket = min( /llbracket Γ 1 /rrbracket , /precedesequal K ) by compatibility, we have that ω ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) ∩ /llbracket Γ 2 /rrbracket . Suppose for a contradiction that ω /negationslash∈ /llbracket K ◦ (Γ 1 ∪ Γ 2 ) /rrbracket . Then, ω /negationslash∈ min( /llbracket Γ 1 ∪ Γ 2 /rrbracket , /precedesequal K ) . This contradicts ω ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) . Therefore ω ∈ /llbracket K ◦ (Γ 1 ∪ Γ 2 ) /rrbracket . Thus /llbracket K◦ Γ 1 /rrbracket ∩ /llbracket Γ 2 /rrbracket ⊆ /llbracket K◦ (Γ 1 ∪ Γ 2 ) /rrbracket as desired.
/negationslash
The proof of Theorem 2 follows from Proposition 8 and 9.
## 6 Abstract Representation Theorem
Theorem 2 establishes the correspondence between operators and assignments under the assumption that ◦ is known to exist. Toward a full characterization, we provide an additional condition on assignments, capturing operator existence.
A semantic base change function is a mapping R : P fin ( L ) × P fin ( L ) → P (Ω) . A base change operator ◦ is said to implement R if for all K , Γ ∈ P fin ( L ) holds /llbracket K ◦ Γ /rrbracket = R ( K , Γ) . An assignment /precedesequal ( . ) is said to represent R if min( /llbracket Γ /rrbracket , /precedesequal K ) = R ( K , Γ) for all K , Γ ∈ P fin ( L ) .
For the existence of an operator, it will turn out to be essential that any minimal model set of a belief base obtained from an assignment corresponds to some belief base, a property which is formalized by the following notion.
Definition 7 (min-expressible) . Given a logic L =( L , Ω , /satisfies ) , a binary relation /precedesequal over Ω is called min-expressible if for each Γ ∈ P fin ( L ) there exists a belief base B Γ , /precedesequal ∈ P fin ( L ) such that /llbracket B Γ , /precedesequal /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal ) . An assignment /precedesequal ( . ) will be called min-expressible, if for each K ∈ P fin ( L ) , /precedesequal K is minexpressible. Given a min-expressible assignment /precedesequal ( . ) , let ◦ /precedesequal ( . ) denote the base change operator defined by K◦ /precedesequal ( . ) Γ= B Γ , /precedesequal K .
We find the following abstract relation between expressibility, assignments and operators.
Theorem 10. Let L be a logic and let R be a semantic base change function for L . Then R is implemented by a base change operator satisfying (G1)-(G6) iff R is represented by a min-expressible and min-friendly faithful assignment.
Proof. ( ⇒ ) Let ◦ be the corresponding base change operator. Then, by Proposition 8, the assignment /precedesequal ◦ ( . ) as given in Definition 6 is min-friendly, faithful, and compatible with ◦ , thus it represents R . As for min-expressibility, recall that, by compatibility, /llbracket K ◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) for every Γ . As K◦ Γ is a belief base, min-expressibility follows immediately.
( ⇐ ) Let /precedesequal ( . ) be the corresponding min-expressible assignment and ◦ /precedesequal ( . ) as provided in Definition 7. By construction, ◦ /precedesequal ( . ) is compatible with /precedesequal ( . ) and therefore implements R . Proposition 9 implies that ◦ /precedesequal ( . ) satisfies (G1)-(G6).
Some colleagues argue that revising bases instead of belief sets calls for syntax-dependence and therefore (G4) should be discarded [8]. Without positioning ourselves in this matter, we would like to emphasize that our characterizations from Theorem 2 and Theorem 10 can be easily adjusted to a more syntax-sensitive setting: a careful inspection of the proofs shows that the results remain valid upon dropping (G4) from the postulates and (F3) from the faithfulness definition.
## 7 Total Preorder Representability
We identify those logics for which every revision operator is representable by a total preorder assignment.
Definition 8 (total preorder representable) . A base change operator ◦ is called total preorder representable if there is a min-complete faithful preorder assignment compatible with ◦ .
The following setting, describing a relationship between belief bases, will turn out to be the one and only reason to prevent total preorder representability.
Definition 9 (critical loop) . Let L = ( L , Ω , /satisfies ) be a logic. Three bases Γ 0 , Γ 1 , Γ 2 ∈P fin ( L ) form a critical loop for L if there exist K , Γ ′ 0 , Γ ′ 1 , Γ ′ 2 ∈P fin ( L ) such that
<!-- formula-not-decoded -->
<!-- formula-not-decoded -->
/negationslash
<!-- formula-not-decoded -->
We note that Definition 9 generalises a known example for non-total preorder representability in Horn logic [5,6].
Proposition 11. If L exhibits a critical loop, then there is a base change operator ◦ for L satisfying (G1)-(G6) that is not total preorder representable.
Proof. Let Γ 0 , Γ 1 , Γ 2 ∈ P fin ( L ) form a critical loop and let Γ ′ 0 , Γ ′ 1 , Γ ′ 2 and K as in Definition 9.
/negationslash
Let B denote the set of all Γ ′ guaranteed by Condition (3) from Definition 9, i.e. Γ ′ ∈ B if there is some Γ with ∅ /negationslash = /llbracket Γ ′ /rrbracket ⊆ /llbracket Γ /rrbracket \ ( /llbracket Γ 0 /rrbracket ∪ /llbracket Γ 1 /rrbracket ∪ /llbracket Γ 2 /rrbracket ) such that /llbracket Γ ′ i /rrbracket ∩ /llbracket Γ /rrbracket = ∅ for all i ∈ { 0 , 1 , 2 } . Now let B ′ = { Γ ∈ B | /llbracket Γ ∪ K /rrbracket = ∅} , i.e., all belief bases from B that are inconsistent with K . Let /lessorequalslant be an arbitrary linear order on B ′ with respect to which every non-empty subset of B ′ has a minimum. 4 We now define ◦ as follows: for every K ′ /negationslash≡ K and any Γ , let K ′ ◦ Γ = K ′ ∪ Γ if K ′ ∪ Γ is consistent, otherwise K ′ ◦ Γ = Γ . For K (and any base equivalent to it), we define:
/negationslash
<!-- formula-not-decoded -->
/negationslash
We show that ◦ satisfies (G1)-(G6) . For K ′ /negationslash≡ K we obtain a full meet revision which is known to satisfy (G1)-(G6) [11]. Consider the remaining case of K (and any equivalent base):
/negationslash where Γ B ′ min =min( { Γ ′ ∈ B ′ | /llbracket Γ ′ ∪ Γ /rrbracket = ∅} , /lessorequalslant ) . The construction exploits that Condition (2) implies /llbracket Γ ′ 0 ∪ Γ ′ 1 ∪ Γ ′ 2 /rrbracket = ∅ and by Condition (3) every base consistent with Γ ′ 0 , Γ ′ 1 and Γ ′ 2 has models outside of /llbracket Γ 0 /rrbracket ∪ /llbracket Γ 1 /rrbracket ∪ /llbracket Γ 2 /rrbracket .
Postulates (G1)-(G4) . The satisfaction of (G1)-(G3) follows direction from the construction of ◦ . For (G4) observe that the case distinction above considers only models of Γ when computing K◦ Γ . Thus, for Γ ∗ 1 ≡ Γ ∗ 2 we always obtain K◦ Γ ∗ 1 ≡ K ◦ Γ ∗ 2 .
/negationslash
Postulate (G5) and (G6) . Consider two belief bases Γ ∗ 1 and Γ ∗ 2 . If Γ ∗ 2 is inconsistent with K ◦ Γ ∗ 1 , then we obtain satisfaction of (G5) immediately. For the remaining case of (G5) and (G6) we assume K ◦ Γ ∗ 1 to be consistent with Γ ∗ 2 . The postulate (G1) implies that Γ ∗ 1 ∪ Γ ∗ 2 is consistent. If Γ ∗ 1 is consistent with K , then we obtain consistency of Γ ∗ 2 ∪ K . This implies K◦ (Γ ∗ 1 ∪ Γ ∗ 2 ) ≡ ( K◦ Γ ∗ 1 ) ∪ Γ ∗ 2 ; yielding satisfaction of (G5) and (G6). For the case of consistency of Γ ∗ 1 with some Γ ′ ∈ B ′ , the set Γ ∗ 1 ∪ Γ ∗ 2 is also consistent with Γ ′ . We obtain (Γ ∗ 1 ) B ′ min = (Γ ∗ 1 ∪ Γ ∗ 2 ) B ′ min , hence Γ ∗ 2 is consistent with Γ ′ and for every Γ ′′ ∈ B ′ with /llbracket Γ ′′ ∪ Γ ∗ 1 ∪ Γ ∗ 2 /rrbracket = ∅ we also have /llbracket Γ ′′ ∪ Γ ∗ 1 /rrbracket = ∅ . This yields K◦ (Γ ∗ 1 ∪ Γ ∗ 2 ) ≡ ( K ◦ Γ ∗ 1 ) ∪ Γ ∗ 2 , establishing (G5) and (G6) for this case. If Γ ∗ 1 is consistent with Γ ′ i and inconsistent with Γ ′ i ⊕ 2 , then likewise Γ ∗ 1 ∪ Γ ∗ 2 is consistent with Γ ′ i and inconsistent with Γ ′ i ⊕ 2 . Again we obtain K◦ (Γ ∗ 1 ∪ Γ ∗ 2 ) ≡ ( K◦ Γ ∗ 1 ) ∪ Γ ∗ 2 . If none of the conditions above applies to Γ ∗ 1 , then they also not apply to Γ ∗ 1 ∪ Γ ∗ 2 . From the construction of ◦ we obtain K◦ (Γ ∗ 1 ∪ Γ ∗ 2 ) ≡ ( K◦ Γ ∗ 1 ) ∪ Γ ∗ 2 .
/negationslash
/negationslash
It remains to show that ◦ is not total preorder representable. Towards a contradiction suppose there is a min-complete faithful preorder assignment /precedesequal ( . ) for ◦ . By construction there are ω i , ω j ∈ Ω with ω i /satisfies K ◦ Γ i and ω j /satisfies K ◦ Γ i for 0 ≤ i, j ≤ 2 and i = j . Obtain /llbracket K ◦ Γ i /rrbracket = min( /llbracket Γ i /rrbracket , /precedesequal K ) from the compatibility with ◦ . The definition of ◦ yields ω 1 ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) and ω 2 /satisfies Γ 1 and ω 2 / ∈ min( /llbracket Γ 1 /rrbracket , /precedesequal K ) . We obtain thereof the strict relation ω 1 ≺ K ω 2 . The same argument applies to every pair of interpretations ω i , ω i ⊕ 1 . In summary, we get ω 0 ≺ K ω 1 ≺ K ω 2 ≺ K ω 0 , which is impossible for a transitive relation.
/negationslash
We call pairs of interpretations detached when the base change operator gives no hint about how to order them.
/negationslash
Definition 10. A pair ( ω, ω ′ ) ∈ Ω × Ω is called detached from ◦ in K , if ω, ω ′ /satisfies K◦ Γ for all Γ ∈ P fin ( L ) .
4 Such a /lessorequalslant exists due to the well-ordering theorem, by courtesy of the axiom of choice [20].
/negationslash
Detached pairs will be helpful when proving the missing part of the correspondence between critical loop and total preorder representability. In particular, violations of transitivity in /precedesequal ◦ K from Definition 6 always contain a detached pair.
Lemma 12. Assume L does not admit a critical loop and ◦ satisfies (G1)-(G6). If ω 0 /precedesequal ◦ K ω 1 and ω 1 /precedesequal ◦ K ω 2 with ω 0 /negationslash/precedesequal ◦ K ω 2 , then ( ω 0 , ω 1 ) or ( ω 1 , ω 2 ) is detached from ◦ in K .
/negationslash
Proof. Towards a contradiction, assume a violation of transitivity, where ( ω 0 , ω 1 ) and ( ω 1 , ω 2 ) are not detached from ◦ in K . By Lemma 3 the relation ≺ ◦ K is total, and thus we have that ω 2 ≺ ◦ K ω 0 . Then, due to Lemma 4, there exist Γ 0 , Γ 1 ∈ P fin ( L ) satisfying ω 0 , ω 1 /satisfies Γ 0 and ω 0 /satisfies K ◦ Γ 0 as well as ω 1 , ω 2 /satisfies Γ 1 and ω 1 /satisfies K◦ Γ 1 . Moreover, there is a Γ 2 with ω 0 , ω 2 /satisfies Γ 2 such that ω 2 /satisfies K◦ Γ 2 and ω 0 /satisfies K◦ Γ 2 .
Consider Conditions (1) and (2) from Definition 9.
Condition (1). Assume that K is consistent with some Γ i . By faithfulness and min-retraction we also have ω i /satisfies K . By employing (G2) we obtain ω i ⊕ 2 /satisfies K from ω i ⊕ 2 /satisfies K◦ Γ i ⊕ 2 . By an analogue argumentation we obtain ω 0 , ω 1 , ω 2 /satisfies K , which yields in consequence a contradiction to ω 2 ≺ ◦ K ω 0 .
/negationslash
Condition (2). We show that K ◦ Γ i is a consistent belief base with /llbracket K ◦ Γ i /rrbracket ⊆ /llbracket Γ i ∪ Γ i ⊕ 1 /rrbracket \ /llbracket Γ i ⊕ 2 /rrbracket for each 0 ≤ i ≤ 2 . If Γ 0 ∪ Γ 1 ∪ Γ 2 is inconsistent, this is immediate. If Γ 0 ∪ Γ 1 ∪ Γ 2 is consistent, then there exists some ω 3 /satisfies Γ 0 ∪ Γ 1 ∪ Γ 2 and thus, ω i /precedesequal ◦ K ω 3 for 0 ≤ i ≤ 2 . If ω 3 /precedesequal ◦ K ω i for some 0 ≤ i ≤ 2 , then obtain the contradiction ω i /satisfies K◦ Γ 2 by employing min-retraction. Therefore, we obtain ω i ≺ ◦ K ω 3 and ω 3 /satisfies K◦ Γ i for all 0 ≤ i ≤ 2 . As consequence, K◦ Γ i is a belief base with /llbracket K◦ Γ i /rrbracket ⊆ /llbracket Γ i ∪ Γ i ⊕ 1 /rrbracket \ /llbracket Γ i ⊕ 2 /rrbracket . Consistency is given by consistency of all Γ i and (G3).
/negationslash
As Γ 0 , Γ 1 , Γ 2 form no critical loop by assumption, yet Conditions (1) and (2) hold, Condition (3) of Definition 9 must be violated by some Γ with /llbracket K◦ Γ i /rrbracket ∩ /llbracket Γ /rrbracket = ∅ for every i ∈ { 0 , 1 , 2 } such that for all Γ ′ with /llbracket Γ ′ /rrbracket ⊆ /llbracket Γ /rrbracket \ ( /llbracket Γ 0 /rrbracket ∪ /llbracket Γ 1 /rrbracket ∪ /llbracket Γ 2 /rrbracket ) we have /llbracket Γ ′ /rrbracket = ∅ . Since /llbracket K ◦ Γ /rrbracket is a consistent belief base, we obtain /llbracket K ◦ Γ /rrbracket ∩ /llbracket Γ i /rrbracket = ∅ for some i ∈ { 0 , 1 , 2 } . From min-retractivity of /precedesequal ◦ K and /llbracket K ◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) we obtain as consequence ω i ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . Employing ω i , ω i ⊕ 2 ∈ /llbracket Γ i ⊕ 2 /rrbracket , minretractivity and /llbracket Γ i ⊕ 2 /rrbracket ⊆ /llbracket Γ /rrbracket we get ω i ⊕ 2 ∈ min( /llbracket Γ /rrbracket , /precedesequal ◦ K ) . By an iterative application of the same argument we observe the contradiction ω 0 /precedesequal ◦ K ω 2 .
/negationslash
Lemma 12 allows us to complete the correspondence between critical loops and total preorder representability.
Theorem 13. A logic L = ( L , Ω , /satisfies ) does not admit a critical loop if and only if every base change operator for L satisfying (G1)-(G6) is total preorder representable.
Proof. One direction is given by Proposition 11. For the other direction, assume L does not admit a critical loop and let ◦ be a base change operator ◦ satisfying (G1)-(G6). We will obtain a min-friendly preorder assignment /precedesequal ( . ) from /precedesequal ◦ ( . ) in two steps. Let K be an arbitrary belief base K . First, let /precedesequal 1 be the relation defined by /precedesequal 1 = /precedesequal ◦ K \ D , where D denotes the set of all ( ω, ω ′ ) ∈ Ω × Ω which are detached from ◦ by K . By Lemma 12, the relation /precedesequal 1 is transitive. Since the removal of a detached pair does not influence the minimality of interpretations with respect to a belief base, we have min(Γ , /precedesequal 1 ) = min(Γ , /precedesequal ◦ K ) for all Γ ∈ P fin ( L ) . Second, the relation /precedesequal 1 can be order extended to a total preorder /precedesequal 2 such that /precedesequal 1 ⊆/precedesequal 2 and ω 1 ≺ 1 ω 2 implies ω 1 ≺ 2 ω 2 [10, Lem. 3]. 5 Choose /precedesequal K to be exactly /precedesequal 2 . The relation /precedesequal K is a total preorder where the minimality is preserved, i.e. min(Γ , /precedesequal K ) = min(Γ , /precedesequal ◦ K ) . Moreover, /precedesequal K inherits min-friendliness from /precedesequal ◦ K . Thus, ◦ is total preorder representable.
We close this section with an implication of Theorem 13. A logic L =( L , Ω , /satisfies ) is called disjunctive , if for every two bases Γ 1 , Γ 2 ∈ P fin ( L ) there is a base Γ 1 ∨ Γ 2 ∈ P fin ( L ) such that /llbracket Γ 1 ∨ Γ 2 /rrbracket = /llbracket Γ 1 /rrbracket ∪ /llbracket Γ 2 /rrbracket . This includes the case of any logic allowing for disjunction on the sentence level, i.e., when for every γ, δ ∈ L exists some γ ∨ δ ∈ L such that /llbracket γ ∨ δ /rrbracket = /llbracket γ /rrbracket ∪ /llbracket δ /rrbracket , because then Γ 1 ∨ Γ 2 can be obtained as { γ ∨ δ | γ ∈ Γ 1 , δ ∈ Γ 2 } .
Corollary 14. In a disjunctive logic, every belief change operator satisfying (G1)-(G6) is total preorder representable.
Proof. Adisjunctive logic never exhibits a critical loop; Condition (3) would be violated by picking Γ = Γ 0 ∨ Γ 1 ∨ Γ 2 .
## 8 Related Work
We are aware of two closely related approaches for revising belief bases (or sets) in settings beyond propositional logic, both proposing model-based frameworks for belief revision without fixing a particular logic or the internal structure of interpretations, and characterizing revision operators via minimal models ` a la KM with some additional assumptions.
Delgrande et al. [6] add additional restrictions both for the interpretations (aka possible worlds) as well as for the postulates. On the interpretation side, unlike us, they restrict their number to be finite. Also they impose a constraint called regularity which serves the very same purpose on their preorders as min-expressibility serves on our total relations. As for the postulates, they extend the basic AGM postulates with a new one, called (Acyc) , with the goal to exclude cyclic preference situations (our 'critical loops'). Yet, by imposing this postulate, they rule out some cases of AGM belief revision that we can cover with our framework, which works with (and characterizes) the pristine AGM postulates.
Aiguier et al. [1] consider AGM-like belief base revision with possibly infinite sets of interpretations. Moreover, like us, they argue in favor of dropping the requirement that assignments have to yield preorders. However, they rule out (KM4)/(G4) from the postulates, thus immediately restricting attention to the syntax-dependent case. Also, alike Delgrande et al.'s, their characterization imposes an additional postulate. On another note, Aiguier et al. consider some bases, that actually do have models, as inconsistent (and thus in need of revision), which in our view is at odds with the foundational assumptions of belief revision.
5 Once more, to this end, we have to assume the axiom of choice .
## 9 Conclusion
We presented a characterization of AGM belief base revision in terms of preference assignments, adapting the approach by KM.Contrary to prior work, our result requires no adjustment of the AGM postulates themselves and yet applies to arbitrary monotonic logics with possibly infinite model sets. While we need to allow for non-transitive preference relations, we also precisely identify the logics where the preference relations can be guaranteed to be preorders as in the original KM result. In particular, this holds for all logics featuring disjunction.
As one of the avenues for future work, we will consider iterated revision. To this end, our aim is to advance the line of research by Darwiche and Pearl [4] to more general logics.
Finally, we will also be working on concrete realisations of the approach presented here in popular KR formalisms such as ontology languages.
## References
- [1] M.Aiguier, J. Atif, I. Bloch, and C. Hudelot. Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics. Artificial Intelligence , 256:160 180, 2018.
- [2] C. E. Alchourr´ on, P. Gardenfors, and D. Makinson. On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic , 50(22):510-530, 1985.
- [3] G. Bonanno. Axiomatic characterization of the AGM theory of belief revision in a temporal logic. Artificial Intelligence , 171(2-3):144-160, 2007.
- [4] A. Darwiche and J. Pearl. On the logic of iterated belief revision. Artificial Intelligence , 89:1-29, 1997.
- [5] J. P. Delgrande and P. Peppas. Belief revision in Horn theories. Artificial Intelligence , 218:1-22, 2015.
- [6] J. P. Delgrande, P. Peppas, and S. Woltran. General belief revision. J. ACM , 65(5), Sept. 2018.
- [7] T. Dong, C. L. Duc, and M. Lamolle. Tableau-based revision for expressive description logics with individuals. Journal of Web Semantics , 45:63 - 79, 2017.
- [8] E. L. Ferm´ e and S. O. Hansson. Belief Change - Introduction and Overview . Springer Briefs in Intelligent Systems. Springer, 2018.
- [9] C. Halaschek-Wiener and Y. Katz. Belief base revision for expressive description logics. In B. C. Grau, P. Hitzler, C. Shankey, and E. Wallace, editors, Proceedings of the OWLED*06 Workshop on OWL: Experiences and Directions , volume 216 of CEUR Workshop Proceedings . CEUR-WS.org, 2006.
- [10] B. Hansson. Choice structures and preference relations. Synthese , 18(4):443-458, 1968.
- [11] S. O. Hansson. A Textbook of Belief Dynamics: Theory Change and Database Updating . Springer, 1999.
- [12] H. Katsuno and A. O. Mendelzon. Propositional knowledge base revision and minimal change. Artificial Intelligence , 52(3):263 - 294, 1991.
- [13] D. K. Lewis. Counterfactuals . Harvard University Press, Cambridge, Massachusetts, 1973.
- [14] P. Pardo, P. Dellunde, and L. Godo. Base belief change for finitary monotonic logics. In P. Meseguer, L. Mandow, and R. M. Gasca, editors, Current Topics in Artificial Intelligence, 13th Conference of the Spanish Association for Artificial Intelligence, CAEPIA 2009 , volume 5988 of Lecture Notes in Computer Science , pages 81-90. Springer, 2009.
- [15] G. Qi, W. Liu, and D. A. Bell. Knowledge base revision in description logics. In M. Fisher, W. van der Hoek, B. Konev, and A. Lisitsa, editors, Logics in Artificial Intelligence , pages 386-398. Springer Berlin Heidelberg, 2006.
- [16] M. M. Ribeiro. Belief Revision in Non-Classical Logics . Springer Briefs in Computer Science. Springer, 2013.
- [17] M. M. Ribeiro and R. Wassermann. Minimal change in AGM revision for non-classical logics. In C. Baral, G. D. Giacomo, and T. Eiter, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014 . AAAI Press, 2014.
- [18] M. M. Ribeiro, R. Wassermann, G. Flouris, and G. Antoniou. Minimal change: Relevance and recovery revisited. Artificial Intelligence , 201:59-80, 2013.
- [19] S. Shapiro, M. Pagnucco, Y. Lesp´ erance, and H. J. Levesque. Iterated belief change in the situation calculus. Artificial Intelligence , 175(1):165-192, 2011.
- [20] T. Vialar. Handbook of Mathematics . HDBoM, 2017.
- [21] Z. Zhuang, Z. Wang, K. Wang, and J. P. Delgrande. A generalisation of AGM contraction and revision to fragments of first-order logic. J. Artif. Intell. Res. , 64:147179, 2019.
## Supplement
In addition to our paper, we provide in the following some supplementary example and remarks for the reviewer. We start by presenting a running example.
Example 1 (based on [6]) . Let L Ex = ( L Ex , Ω Ex , /satisfies Ex ) be the logic defined by L Ex = { ψ 0 , . . . , ψ 5 , ϕ 0 , . . . , ϕ 4 } and Ω Ex = { ω 0 , . . . , ω 5 } , with the models relation /satisfies Ex implicitly given by:
<!-- formula-not-decoded -->
Since defined in the classical model-theoretic way, L Ex is a monotonic logic.
Note that logic L Ex has no connectives. However, this is just for illustrative purposes and we want to highlight that Example 1 is an extension of an example given by Delgrande et. al [6], which is known to be implementable in Horn logic [5]. As next step, we provide a base change operator for L Ex .
Example 2 (continuation of Example 1) . Let K = { ψ 0 } and let ◦ Ex be the base change operator defined as follows:
/negationslash
<!-- formula-not-decoded -->
/negationslash
For all K ′ with K ′ ≡ K we define K ′ ◦ Γ = K◦ Γ and for all K ′ with K ′ /negationslash≡ K we define
<!-- formula-not-decoded -->
For all K ′ with K ′ /negationslash≡ K , there is no violation of the postulates (G1)-(G6) since we obtain a full meet revision known to satisfy (G1)-(G6) [11]. It remains to verify satisfaction of (G1)-(G6) for the case of K ′ ≡ K . Therefore, we will provide a relation over Ω Ex and make then use of Theorem 10 to show satisfaction of (G1)-(G6). Before continuing with our running example in the next section, we give some remarks beforehand on the generic technique our paper provides for obtaining such a relation.
## On Encoding an Operator into a Preference Relation
One of the main contributions of our article is a novel way of obtaining a preference relation from an operator. The established way of encoding a revision operator is provided by Katsuno and Mendelzon [12] as follows:
<!-- formula-not-decoded -->
/negationslash
/negationslash
/negationslash where form ( ω 1 , ω 2 ) ∈ L denotes a formula with /llbracket form ( ω 1 , ω 2 ) /rrbracket = { ω 1 , ω 2 } . The problem in a general logical setting is that there might be no such formula form ( ω 1 , ω 2 ) with /llbracket form ( ω 1 , ω 2 ) /rrbracket = { ω 1 , ω 2 } in the considered logic. This generalises to the non-existence of such belief bases. In particular, this is the case in our running example (cf. Example 1).
Clearly, we are not the first to address this problem. Delgrande, Peppas and Woltran [6] solve this problem by simultaneously revising with all formulae satisfying ω 1 and ω 2 , in order to 'simulate' the revision by the desired formula form ( ω 1 , ω 2 ) . Aiguier, Atif, Block and Hudelot [1] use a similar approach by revising with all formulae at once. In summary, neither Aiguier et. al nor Delgrande et al. use a encoding approach fundamentally different to the one by Katsuno and Mendelzon.
However, in our approach, we consider the restricted setting of revision by finite bases. Therefore, the approach by Aiguier et al. and Delgrande et al. was not feasible for us. Moreover, it turns out that applying this idea to the general case would leave the order of certain pairs of elements undetermined. Depending on the shape of the logic (and its model theory) and the operator, there might be no preference between certain elements (because there is no revision which provides information on the preference). We call this pairs of interpretations detached (c.f. Definition 10). In particular, when one wants to obtain a total relation, these elements have to be ordered in a certain way, and selection of a 'preference' between these two interpretations is a 'non-local' choice (as it may have ramifications for other 'ordering choices').
As solution, we came up with Definition 6, which provides an encoding different from the approach by Katsuno and Mendelzon. This definition solves the problem with the detached pairs by treating them as equal. As a nice resulting property, we obtain that the relation given by Definition 6 is a maximal canonical representation for the preferences of an operator - a property the encoding approaches given by Equation (1) do not have.
Proposition 15. Let ◦ be a base change operator satisfying (G1)-(G6). If /precedesequal ( . ) is a min-friendly faithful assignment compatible with ◦ , then ω 1 /precedesequal K ω 2 implies ω 1 /precedesequal ◦ K ω 2 for every ω 1 , ω 2 ∈ Ω and every belief base K ∈ P fin ( L ) .
/negationslash
Proof. By Theorem 2, the relation /precedesequal K is min-friendly and total. Now assume ω 1 /precedesequal K ω 2 with ω 1 /negationslash/precedesequal ◦ K ω 2 . By Lemma 4 (a), there is a belief base Γ with ω 1 , ω 2 /satisfies Γ such that ω 2 /satisfies K ◦ Γ and ω 1 /satisfies K ◦ Γ . Therefore, by compatibility, ω 2 ∈ min( /llbracket Γ /rrbracket , /precedesequal K ) = /llbracket K◦ Γ /rrbracket and ω 1 / ∈ min( /llbracket Γ /rrbracket , /precedesequal K ) = /llbracket K◦ Γ /rrbracket , a contradiction to ω 1 /precedesequal K ω 2 due to min-retractivity.
We continue with the running example.
Example 3 (continuation of Example 2) . Applying Definition 6 to K and ◦ Ex yields the following relation /precedesequal ◦ Ex K on
Ω Ex (where ω ≺ ◦ Ex K ω ′ denotes ω /precedesequal ◦ Ex K ω ′ and ω ′ /negationslash/precedesequal ◦ Ex K ω ):
<!-- formula-not-decoded -->
Observe that /precedesequal ◦ Ex K is not transitive, since ω 1 , ω 2 , ω 3 form a circle. Yet, one can easily verify that /precedesequal ◦ Ex K is a total and min-friendly relation. In particular, as Ω Ex is finite, mincompleteness is directly given. Moreover, there is no belief base Γ ∈ P fin ( L Ex ) such that there is some ω / ∈ min(Γ , /precedesequal ◦ Ex K ) and ω ′ ∈ min(Γ , /precedesequal ◦ Ex K ) with ω /precedesequal ◦ Ex K ω ′ . Note that such a situation could appear in /precedesequal ◦ Ex K if a interpretation ω would be /precedesequal ◦ Ex K -equivalent to ω 1 , ω 2 and ω 3 and there would be a belief base Γ satisfied in all these interpretations, e.g., if ω = ω 5 would be equal to ω 1 , ω 2 and ω 3 , and /llbracket Γ /rrbracket = { ω 1 , . . . , ω 3 , ω 5 } . However, this is not the case in /precedesequal ◦ Ex K and such a belief base Γ does not exist in L Ex . Therefore, the relation /precedesequal ◦ Ex K is min-retractive.
The following Proposition summarizes what we have achieved so far by Example 1 to Example 3.
Proposition 16. There is a monotone logic L , a base change operator ◦ on L which satisfies (G1)-(G6), and a belief base K such that /precedesequal ◦ K (cf. Definition 6) is a min-friendly but not transitive relation.
We continue with some remarks on min-retractivity and transitivity.
## Remarks on Min-Retractivity and Transitivity
In belief revision literature, transitivity and the postulates (G5) and (G6) are strongly associated. Therefore, at a first glance, the introduction of the notion of min-retractivity seems to be artificial and unnatural in comparison to transitivity. However, it turns out that min-retractivity is the property of capturing the nature of the AGM postulates (G5) and (G6) very exactly.
Suppose L is a logic having a disjunction connective. It is well-known in belief revision that (G5) and (G6) are equivalent (in the light of (G1)-(G4)) to disjunctive factoring [11] (here given in a semantic formulation for belief bases):
<!-- formula-not-decoded -->
Now consider the following observation on min-retractivity.
Proposition 17. Let Γ 1 , . . . , Γ n , Γ ⊆ P fin ( L ) be belief bases with /llbracket Γ /rrbracket = /llbracket Γ 1 /rrbracket ∪ . . . ∪ /llbracket Γ n /rrbracket and let /precedesequal be a min-retractive relation on Ω . Then min(Γ , /precedesequal ) = ⋃ i ∈ I min( /llbracket Γ i /rrbracket , /precedesequal ) for some set I ⊆ { 1 , . . . , n } .
<!-- formula-not-decoded -->
If ω ∈ /llbracket Γ j /rrbracket then we have for each ω ′ ∈ min( /llbracket Γ j /rrbracket , /precedesequal ) that ω ′ /precedesequal ω holds. Since /precedesequal is min-retractive, we conclude that ω ′ ∈ min( /llbracket Γ /rrbracket , /precedesequal ) . Consequently, we obtain min( /llbracket Γ j /rrbracket , /precedesequal ) ⊆ min( /llbracket Γ /rrbracket , /precedesequal ) . For the converse direction, let I be the smallest set such that min( /llbracket Γ /rrbracket , /precedesequal ) ⊆ ⋃ i ∈ I /llbracket Γ i /rrbracket . Observe that from /llbracket Γ i /rrbracket ⊆ /llbracket Γ /rrbracket and ω ∈ min( /llbracket Γ /rrbracket , /precedesequal ) the statement ω ∈ min( /llbracket Γ i /rrbracket , /precedesequal ) follows directly. As a consequence, we obtain min( /llbracket Γ /rrbracket , /precedesequal ) = ⋃ i ∈ I min( /llbracket Γ i /rrbracket , /precedesequal ) .
By Proposition 17, when a relation ≤ on the interpretations and an operator ◦ are compatible, i.e. /llbracket K◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , ≤ ) , then min-retractivity of ≤ guarantees disjunctive factoring. This shows the strong and natural connection between the notion of min-retractivity and (G5) and (G6).
## Expressibility and Satisfaction of (G1)-(G6)
For our running example, we will now observe that /precedesequal ◦ Ex K is also a min-expressible relation.
Example 4 (continuation of Example 3) . Consider again /precedesequal ◦ Ex K , and observe that /precedesequal ◦ Ex K is compatible with ◦ Ex , i.e. /llbracket K◦ Γ /rrbracket = min( /llbracket Γ /rrbracket , /precedesequal ◦ Ex K ) .
Theorem 10 guarantees us that ◦ Ex satisfies (G1)-(G6), as we can extend /precedesequal ◦ Ex K to a faithful min-expressible and minfriendly assignment.
Thus, for every belief base Γ ∈ P fin ( L Ex ) , the minimum min(Γ , /precedesequal ◦ Ex K ) yields a set expressible by a belief base.
## Total Preorder Representability
As last step, we will now employ the novel notion of critical loop (cf. Definition 9) and our representation theorem (cf. Theorem 13) for total preorder representability, to show that there is no (total) preorder assignment for the operator ◦ Ex from our running example.
Example 5 (continuation of Example 4) . Consider again L Ex from Example 1. We will now see that L Ex exhibits a critical loop.
For this, choose Γ i = { ϕ i +1 } and Γ ′ i = { ψ i +2 } for i ∈ { 0 , 1 , 2 } . We consider each of the three conditions of Definition 9 in a separate case:
Condition (1). Observe that K from Example 2 is inconsistent with Γ 0 , Γ 1 and with Γ 2 . Thus, Condition (1) is satisfied.
Condition (2). For each i ∈ { 0 , 1 , 2 } , the belief base Γ i and 6 Γ i ⊕ 1 are consistent, but Γ i ∪ Γ i ⊕ 1 ∪ is inconsistent with Γ i ⊕ 2 , e.g. /llbracket { ϕ 1 } /rrbracket ∩ /llbracket { ϕ 2 } /rrbracket = { ω 2 } and ω 2 / ∈ /llbracket { ϕ 3 } /rrbracket . For satisfaction of Condition (2), observe that Γ ′ i is equivalent to Γ i ∪ Γ i ⊕ 1 .
Condition (3). The belief base Γ = { ϕ 4 } is the only belief base consistent with Γ ′ 0 , Γ ′ 1 , and Γ ′ 2 . For satisfaction of Condition (3) observe that Γ ′ = { ψ 4 } fulfils the required condition ∅ /negationslash = /llbracket Γ ′ /rrbracket ⊆ /llbracket Γ /rrbracket \ ( /llbracket Γ 0 /rrbracket ∪ /llbracket Γ 1 /rrbracket ∪ /llbracket Γ 2 /rrbracket ) .
In summary Γ 0 , Γ 1 , and Γ 2 form a critical loop for L Ex . Thus, by Theorem 13 ◦ Ex is not total preorder representable, i.e., there is no min-friendly min-expressible preorder assignment compatible with ◦ Ex .
Moreover, observe that the construction of ◦ Ex presented in Example 2 illustrates the construction given in the proof of
6 where ⊕ is addition mod 3 .
Proposition 11. In particular, for the example presented here one would obtain B ′ = {{ ϕ 4 }} when following the outline of the proof.
The following proposition summarizes an implication of the running example we presented here.
Proposition 18. There is a monotone logic L , a base change operator ◦ on L which satisfies (G1)-(G6) and a belief base K such that ◦ is a not total preorder representable.