# finite_based_contraction_and_expansion_via_models__d915f495.pdf

Finite Based Contraction and Expansion via Models

Ricardo Guimar aes1, Ana Ozaki1, Jandson S. Ribeiro2

1 University of Bergen 2 University of Hagen ricardo.guimaraes@uib.no, ana.ozaki@uib.no, jandson.ribeiro@fernuni-hagen.de

We propose a new paradigm for Belief Change in which the new information is represented as sets of models, while the agent s body of knowledge is represented as a finite set of formulae, that is, a finite base. The focus on finiteness is crucial when we consider limited agents and reasoning algorithms. Moreover, having the input as arbitrary set of models is more general than the usual treatment of formulae as input. In this setting, we define new Belief Change operations akin to traditional expansion and contraction, and we identify the rationality postulates that emerge due to the finite representability requirement. We also analyse different logics concerning compatibility with our framework.

1 Introduction

The field of Belief Change (Alchourr on, G ardenfors, and Makinson 1985; Hansson 1999) studies how an agent should rationally modify its current beliefs when confronted with a new piece of information. The agent should preserve most of its original beliefs, minimising loss of information, which is known as the principle of minimal change. Traditionally, Belief Change is studied via two perspectives: (i) set of rationality postulates that conceptualise the principle of minimal change (ii) and classes of Belief Change operations characterised by such rationality postulates. These two views of Belief Change are tightly connected via representation theorems which show that these views are equivalent. The standard paradigm of Belief Change (Alchourr on, G ardenfors, and Makinson 1985), named AGM due to the initial of its founders, assumes that an agent s epistemic state is represented as a set of sentences logically closed known as theories. A main issue with theories is that they are often infinite, whilst rational agents are cognitively limited in the sense that an agent is only capable of carrying a finite amount of explicit beliefs, and all its implicit beliefs follows from such a finite body of beliefs. A theory that can be generated from a finite set of formulae is called finite based (Hansson 1996, 1993b). For this reason, we will call finite sets of formulae finite bases, as arbitrary sets of formulas simply (belief) bases. While in classical propositional logics, every theory is finite based, this

Copyright 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

is not the case for more expressive logics such as first-order logic (FOL) and several Description Logics (DLs) (Baader et al. 2017) such as ALC. Computationally, this finiteness requirement is also important as reasoners for a particular logic usually can only deal with finite sets of formulae. Therefore, it is paramount that Belief Change operations guarantee that the new epistemic state is finite based. However, the AGM postulates do not address finite representation of epistemic states. In fact, the question of finite representability has not been prioritised in Belief Change. In this work, we address this issue by devising novel classes of belief operators which ensure that the outcome is finite based. Moreover, although the AGM rationality postulates do not depend on any specific logic, classes of Belief Change operations have been devised upon strong assumptions about the underlying logics. In the last years, effort have been made in replacing some of these assumptions with weaker conditions in order to extend the AGM paradigm to more logics such as logics without classical negation (Ribeiro 2013), Horn logics (Delgrande and Wassermann 2013, 2010), temporal logics and logics without compactness (Ribeiro, Nayak, and Wassermann 2018, 2019a,b). In this work, we consider that the incoming information is represented as a set of models, which generalises the AGM paradigm and other classical Belief Change frameworks where the incoming information is represented as formulae in the same logic. Moreover, there are scenarios where it is more convenient that the incoming information is represented as models. This is the case of the Learning from Interpretations setting (De Raedt 1997), where a formula needs to be created or changed to either incorporate or block a set of models. Arias, Khardon, and Maloberti (2007) use this setting to model the construction of Horn theories from graphs. In logics displaying theories that are not finite based, the closest finite based epistemic state can be chosen instead. We present an intuitive notion of closest finite base to handle cases in which not every theory is finite based. Using this notion, we then define model change operations which correspond, in spirit, to expansion and contraction in the AGM paradigm. We also investigate the rationality consequences of the finiteness requirement and show that our operators only gain or lose models (information) when desired or necessary. Furthermore, we analyse the compatibility of logics with respect to the emerged rationality postulates, that is, we

The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)

obtain necessary and sufficient conditions for a logic to admit rational contraction and expansion operators by models. In Section 2, we briefly review basic concepts. In Section 3, we detail the new Belief Change paradigm that we propose. We discuss in Section 4 how properties of a logic (seen as a satisfaction system) affect the behaviour of model change operations. In Section 5, we analyse different logics and the ability to define model change operations following our paradigm. In Section 6, we highlight related works and conclude in Section 7. Full proofs of the results can be found in the long version (Guimar aes, Ozaki, and Ribeiro 2023).

2 Notation and Basic Notions The power set of a set A is denoted by P(A), while the set of all finite subsets of A is denote by Pf(A). We will write P (A) to refer to the non-empty subsets of A. Following Aiguier et al. (2018) and Delgrande, Peppas, and Woltran (2018), we look at a logic as a satisfaction system. A satisfaction system is a triple Λ = (L, M, |=), where L is a language, M is the set of models, also called interpretations, used to give meaning to the sentences in L, and |= is a satisfaction relation which indicates that a model M satisfies a base B (in symbols, M |= B). Looking at a logic simply as a satisfaction system allows us to explore its properties without making assumptions about the language or putting constraints upon the logic s entailment relation. Our concern is to turn a belief base into a new one that either is satisfied by a given set of models, or is not satisfied by such models. Towards this end, we do not need to constrain how models are used to define the satisfaction relation, but rather identify exactly which models satisfy a belief base B in a satisfaction system Λ = (L, M, |=) which is given by:

ModΛ(B) := {M M | M |= B}.

We will write simply Mod(B) when the satisfaction system is clear from the context. A set of models M within Λ is finitely representable iff there is B Pf(L) such that Mod(B) = M. Also, we say that a set of formulae B L is finitely representable iff there is a B Pf(L) with Mod(B) = Mod(B ). The collection of all finitely representable sets of models in Λ is given by:

FR(Λ) := {M M | B Pf(L) : Mod(B) = M}.

3 Model Oriented Change on Finite Bases In this work, unlike the standard representation methods in Belief Change, we consider that: incoming information is represented as a (possibly infinite) set of models; while an agent s epistemic states are represented as finite (belief) bases. Differently, from most approaches in Belief Base Change, we are not concerned with the syntactical structure but, instead, with finiteness. This notion of belief bases aligns with Nebel (1990); Dixon (1994) and Dalal (1988), where a belief base is used simply as a form of finitely representing an agent s epistemic state. In our setting, we call each form of rational change in beliefs a model change operation. Formally, a model change operation is a function f : Pf(L) P(M) Pf(L). We propose two kinds of model change operations: reception (rcp(B, M)) when we

want to accept the input models; and eviction (evc(B, M)) when we want to reject them instead. Reception turns the current belief state into a new one that is satisfied by the input models; while in eviction the new epistemic state is not satisfied by any of the input models. In comparison to the Belief Change operations on formulae as input, reception resembles formula contraction, as incorporating a new model implies in removing some formulae from the original belief set. Analogously, eviction resembles formula expansion, as removal of a model implies in acquisition of information. In propositional logics, eviction and reception can be easily defined, as any set of models (over a finite signature) is finitely representable. However, in many logics, there are sets of models that are not finitely representable, even if you assume that the signature is finite. We circumvent this issue by adding or removing models from the current finite base towards the closest finite base satisfied (resp. rejected) by the input models. We show that even with an intuitive notion of closeness , there are cases where the closest solution does not exist. We also identify when a solution is uniquely determined. We introduce each operation separately in the two following subsections.

3.1 Eviction The purpose of eviction is to change the current finite base B as to forbid any interpretation in the input set M. If Mod(B)\M is not finitely representable, then we could simply remove more models until we obtain finite representability. The question at hand is how many and which models to remove to obtain a finite representation? An intuitive idea is to look at a -maximal finitely representable subset of Mod(B) \ M. Such a set is the closest we can get to the ideal result in order to keep finite representability when subtracting M. The class of eviction functions we define in this section is based on this idea. Before we present them, let us first introduce some auxiliary tools. Definition 1. Let Λ = (L, M, |=) be a satisfaction system. Also, let M M.

Max FRSubs(M, Λ) := {M FR(Λ) | M M

and M FR(Λ) with M M M}.

Given a satisfaction system Λ = (L, M, |=) and a set of models M M, the set Max FRSubs(M, Λ) contains exactly all the largest (w.r.t. set inclusion) finitely representable subsets of M. If we want to contract a set M from a finite base B, then we can simply build a finite base for one of the sets in Max FRSubs(Mod(B) \ M). It turns out that one cannot naively apply this strategy because, depending on the underlying satisfaction system, there might exist a finite base B and set of models M such that: (1) Max FRSubs(Mod(B) \ M, Λ) = ; or (2) |Max FRSubs(Mod(B) \ M, Λ)| 2. If a satisfaction system Λ displays problem (1) then we cannot subtract M. Thus, we say that a satisfaction system Λ = (L, M, |=) is eviction-compatible iff Max FRSubs(Mod(B) \ M, Λ) = for all B Pf(L) and M M. There are two possible causes for problem (1).

{p q} {p q, pq}

{ pq} { pq, pq}

{ pq, p q} { pq, p q, pq}

{ p q} { p q, pq}

{ p q, p q} { p q, p q, pq}

{ p q, pq} { p q, pq, pq}

{ p q, pq, p q} M

Figure 1: Lattice generated by the sets of valuations over the propositional atoms {p, q}. Boxed vertices correspond to sets of models in FR(Λ(Horn)). Thin arrows indicate set inclusion, the thick full arrows link sets of models to elements in their respective Max FRSubs

First, when a set of models M has no finitely representable subset, that is, FR(Λ). Second, when there is no - maximal among infinitely many subsets of M: for any such subset, there is another subset of M in FR(Λ) that contains it. Figure 1 illustrates the satisfaction system for propositional Horn logic (Λ(Horn)), a case in which Max FRSubs is always non-empty. Note that bases in Horn logic can represent only sets of models that are closed under conjunction, which explains why { pq, pq} is selected but { pq, p q} is not. As we will prove in Section 5, the usual satisfaction systems for propositional logic and propositional Horn logic are eviction-compatible. However, we will also show that some important satisfaction systems (for instance for the Description Logic ALC) do not have this property. There are two alternatives to deal with problem (1). One is to apply an approach similar to semi-revision (Hansson 1997) and reject the change, keeping the finite base intact. Another alternative, if FR(Λ), is to impose another constraint over the plausible candidates. Problem (2) is related to epistemic choices. Intuitively Max FRSubs(Mod(B)\M, Λ) presents the best solutions to remove M. If multiple solutions exist, then the agent needs to choose among them. Traditionally, it is assumed that such choices are based on an agent s epistemic preference over its beliefs, and such choices are realised by a selection function:

Definition 2. A FR selection function on a satisfaction system Λ is a map sel : P (FR(Λ)) FR(Λ) such that sel(X) X.

Thus, each FR selection function determines an eviction function as follows.

Definition 3. Let Λ be an eviction-compatible satisfaction system and sel a FR selection function on Λ. The maxichoice eviction function on Λ defined by sel is a map evcsel : Pf(L) P(M) Pf(L) such that:

Mod(evcsel(B, M)) = sel(Max FRSubs(Mod(B)\M, Λ)).

The operation evcsel chooses exactly one set in Max FRSubs. Eviction functions that use this strategy are called maxichoice because by choosing only one element

they keep as much information as possible from the original finite base. Another approach is to allow the selection function to choose multiple elements, and then intersect all of them to build the eviction result. However, Proposition 4 shows that this strategy cannot be applied in our setting.

Proposition 4. Given a satisfaction system Λ = (L, M, |=) and set of models M M, if M Max FRSubs(M, Λ) and |M| 2 then not necessarily (T M M M) FR(Λ).

Theorem 5 states a characterisation of the finitely representable eviction functions based on FR selection functions.

Theorem 5. A model change operation evc, defined on an eviction-compatible satisfaction system Λ, is a maxichoice eviction function iff it satisfies the following postulates:

(success) M Mod(evc(B, M)) = . (inclusion) Mod(evc(B, M)) Mod(B). (vacuity) If M Mod(B) = , then Mod(evc(B, M)) = Mod(B). (finite retainment) If Mod(evc(B, M)) M Mod(B) \ M then M FR(Λ). (uniformity) If Max FRSubs(Mod(B) \ M, Λ) = Max FRSubs(Mod(B ) \ M , Λ) then Mod(evc(B, M)) = Mod(evc(B , M )).

The postulate of success ensures that no input model will satisfy the resulting base, while inclusion states that no models will be introduced. Vacuity guarantees that models are removed only when the input set has some models in common with the base. Finite retainment expresses the notion of minimality: we only lose models (other than the input) if there is no other way of ensuring success, inclusion and vacuity while keeping the base finite. Uniformity states that the result depends only on Max FRSubs. Vacuity is redundant in the presence of inclusion and finite retainment.

Proposition 6. If a model change operation evc satisfies inclusion and finite retainment, then it satisfies vacuity.

An analogous to the classical recovery postulate would be desirable: if a set of models M is evicted from a finite base B, then putting M back should restore all the models of B. This model-recovery postulate, however, cannot be satisfied: in order to evict M, some extra models might be purged in order to reach a finite base, and they cannot be restored by simply putting M back. Although the roles of the postulates conjunction and intersection are well-known within classical logics, understanding their behaviours within nonclassical settings are still a challenge (Ribeiro, Nayak, and Wassermann 2018, 2019a). While intersection follows directly from finite-retainment, we cannot characterise conjunction since our framework goes beyond the classical case.

3.2 Reception

Reception alters a finite base B to incorporate all models in M. In some satisfaction systems, Mod(B) M is not finitely representable. Analogous to the strategy employed in the previous subsection, reception can be defined using the smallest supersets of Mod(B) M.

Definition 7. Let Λ = (L, M, |=) be a satisfaction system. Also, let M M.

Min FRSups(M, Λ) := {M FR(Λ) | M M

and M FR(Λ) with M M M }.

There are also satisfaction systems Λ = (L, M, |=) with Min FRSups(M, Λ) = for some M M. The causes are dual to the eviction case: either M FR(Λ) or there is a M M without a -minimal superset in FR(Λ). We say that a satisfaction system Λ = (L, M, |=) is receptioncompatible iff Min FRSups(Mod(B) M, Λ) = for all B Pf(L) and M M. Figure 1 also shows a situation in which the satisfaction system is reception-compatible. In such systems, we can design reception as follows.

Definition 8. Let Λ = (L, M, |=) be a reception-compatible satisfaction system and sel a FR selection function on Λ. The maxichoice model reception function on Λ defined by sel is a map rcpsel : Pf(L) P(M) Pf(L) such that:

Mod(rcpsel(B, M)) = sel(Min FRSups(Mod(B) M, Λ)).

An analogous of Proposition 4 also holds for reception, as stated in Proposition 9.

Proposition 9. Given a satisfaction system Λ = (L, M, |=) and set of models M M, if M Min FRSups(M, Λ) and |M| 2 then not necessarily (S M M M) FR(Λ).

In Section 5, we will show that the usual satisfaction systems for propositional logic and proposition Horn logic are also reception-compatible.We will also introduce a satisfaction system that is reception-compatible but not eviction, thus, showing that reception-compatibility and evictioncompatibility are not always co-occurrent. A satisfaction system Λ = (L, M, |=) can be such that FR(Λ) but M FR(Λ), and vice-versa. We identify the set of rationality postulates that characterise the reception function from Definition 8.

Theorem 10. A model change operation rcp, defined on a reception-compatible satisfaction system Λ, is a maxichoice reception function iff it satisfies the following postulates:

(success) M Mod(rcp(B, M)). (persistence) Mod(B) Mod(rcp(B, M)). (vacuity) Mod(rcp(B, M)) = Mod(B), if M Mod(B). (finite temperance) If Mod(B) M M Mod(rcp(B, M)) then M FR(Λ). (uniformity) If Min FRSups(Mod(B) M, Λ) = Min FRSups(Mod(B ) M , Λ) then Mod(rcp(B, M)) = Mod(rcp(B , M )).

The postulates presented in Theorem 10 are straightforward translations of the classical framework of Belief Change expansion, being finite temperance the only which deviates w.r.t. its classical correspondent. Success guarantees that the input models will satisfy the resulting base, while persistence determines that no model will be lost. Vacuity ensures that models will be added only when the input set brings new models. Finite temperance expresses the notion of minimality: we only gain models (other than the

input) if there is no other way of ensuring success and persistence while keeping the base finitely representable. Uniformity states that the result depends only on Min FRSups. Vacuity is redundant in the presence of finite temperance and persistence.

Proposition 11. If a model change operation rcp satisfies persistence and finite temperance, then it satisfies vacuity.

We can also translate the postulate monotony from classical expansion to our setting as follows: if Mod(B) Mod(B ) then Mod(rcp(B, M)) Mod(rcp(B , M)). However, rcp does not satisfy this postulate and enforcing it means imposing monotonicity on the operation rcp similar to what happens to the update operations of Katsuno and Mendelzon (1991). We would have to constrain FR selection function to only pick certain elements of Min FRSups. A third operation of Belief Change on formulae is belief revision whose purpose is to incorporate a new piece of information and guarantee that the new theory is consistent. In terms of models as input, we could define the model revision operation whose purpose would be to remove models but avoiding that the inconsistent state is reached. To avoid the inconsistent state, the agent would need to select a closest finitely representable set of models according to its underlying epistemic preference relation. We leave such investigation as future work.

4 Uniqueness and Characterisation

In some satisfaction systems, the result of any eviction is uniquely determined by the input models and initial base, regardless of the underlying FR selection function. The same holds for reception in some systems. Many well-known satisfaction systems such as the traditional ones for propositional logic and propositional Horn logic have the reverse monotonic bijection property (RMBP).

Definition 12. A satisfaction system Λ = (L, M, |=) has the RMBP if for every B1, B2 L and every M M: M Mod(B1) and M Mod(B2) iff M Mod(B1 B2).

Proposition 13 states the RMBP is a sufficient condition for this determinism.

Proposition 13. Let Λ = (L, M, |=) be a satisfaction system with the RMBP. Then |Min FRSups(M, Λ)| 1 and |Max FRSubs(M, Λ)| 1 for all M M.

Due to Proposition 13, if Λ = (L, M, |=) has the RBMP then every FR selection function will yield the same result when applied over Min FRSups(M, Λ) for any M M, and the same holds for Max FRSubs(M, Λ). We devote the rest of this section to prove a characterization of evictionand reception-compatibility based on the notion of partial orders. The intuitive idea is that evictioncompatibility of a satisfaction system Λ depends on the ability of finding at least one subset which can be seen as the immediate predecessor when adding a set of models to the partially ordered set (poset) (FR(Λ), ).

Definition 14. Let (P, ), x, y, z P and the strict version of . We say that x is an immediate predecessor of y

if x y and there is no x P with x x y. Analogously, we say that z is an immediate successor of y if y z and there is no z P with y z z. If a satisfaction system Λ = (L, M, |=) guarantees that for any B Pf(B) and M M, Mod(B) \ M will have a finitely representable immediate predecessor regarding set inclusion ( ), then it is eviction-compatible. Some satisfaction systems, do not guarantee this because the empty set of models is not representable (there is no inconsistent base). That would be case for propositional Horn logic if we removed the constant . On the other hand, some satisfaction system (as we will see in Section 5) have non-finitely representable sets of models for which there are arbitrarily close approximations. Hence, none of the infinitely many candidates is an immediate predecessor w.r.t. set inclusion. The analogous notions and observations hold for receptioncompatibility. Example 15 illustrates one such satisfaction system. Example 15. Let Λq = (Lq, Mq, |=q) be such that Lq = {[x, y] | x, y Q and x y}, Mq = Q and Q |=q B (with Q Q) iff for all z Q, x z y for every [x, y] B. Intuitively, every finite base either has no models, or corresponds to a closed interval on the rationals. However, the target set of models produced by an eviction or reception can correspond to an open interval. For eviction, take the base {[0, 1]} and the set of models {1} and for reception, take the base {[0.5, 1]} and the set of models (0, 1]. In both cases, one can find arbitrarily close approximations, thus there might be no maximal subset for eviction nor a minimal superset for reception. Given a satisfaction system Λ = (L, M, |=), it is not only the density of (FR(Λ), ) that determines compatibility. Even when the poset is dense, if every set of models is finitely representable (that is, FR(Λ) = 2M) then Λ is clearly evictionand reception-compatible. Using Definition 14 we can finally characterise evictionand receptioncompatibility with the following theorem. Theorem 16. A satisfaction system Λ = (L, M, |=) is eviction-compatible iff for every M M either (i) M FR(Λ), (ii) M has an immediate predecessor in (FR(Λ) {M}, ), or (iii) there is no M FR(Λ) with M M ; and reception-compatible iff for every M M either (i) M FR(Λ), (ii) M has an immediate successor in (FR(Λ) {M}, ), or (iii) there is no M FR(Λ) with M M. While verifying compatibility can be very cumbersome in general, Corollary 17 displays a simpler sufficient condition when FR(Λ) is finite. Corollary 17. Let Λ = (L, M, |=) be satisfaction system in which FR(Λ) is finite. Then: Λ is eviction-compatible iff FR(Λ). Λ is reception-compatible iff M FR(Λ).

5 Compatibility: Use Cases In this section, we analyse some satisfaction systems and establish whether they are (or not) evictionand receptioncompatible. The framework we presented in Section 3 is

Satisfaction System Compatible

Eviction Reception

Λ(Prop) Yes Yes Λ(Horn) Yes Yes Λ(K3) Yes Yes Λ(P3) No Yes Λ(G odel, θ) Yes Yes Λ(LTLX) No Yes Λ(ABox) Yes No Λ(DL-Lite R) Yes Yes Λ(ALC) No No

Table 1: Evictionand reception-compatibility of different satisfaction systems. : only with finite signature

general enough to cover several satisfaction systems without imposing much constraints upon the logics being used to represent an agent s beliefs. In particular, it covers propositional logic (Theorem 18). However, there are interesting fragments of first-order logic used for knowledge representation that are neither eviction nor reception-compatible, as it is the case of some DLs (Theorem 25). Table 1 summarises the results of compatibility proved in this section.

5.1 The Case of Propositional Logic We start by analysing the simplest case: that of propositional classical logic. We denote by Λ(Prop) the satisfaction system with the entailment relation given by the standard semantics of propositional logic with finite signature. As one can express inconsistency with a finite base, tautologies, and there is only a finite number of valuations, we obtain the following result for Λ(Prop). Theorem 18. Λ(Prop) is reception-compatible and eviction-compatible. Proposition 19 demonstrates how to formulate eviction and reception in propositional logic. Proposition 19. The functions evc Prop and rcp Prop defined next are, respectively, maxichoice eviction and reception functions on Λ(Prop).

evc Prop(B, M) = _

rcp Prop(B, M) = _

As usual, F stands for false and T stands for true . Horn logic limits the language of propositional logic to only facts and implications. Let At be a set of propositional atoms containing (falsum), the language of Horn logic, denoted LH, is given by the following BNF grammar.

φ := φ φ | H | T H T := T T | H H := p

where p At. The universe of models and satisfaction system in (propositional) Horn logic coincide with those of classical propositional logic. The compatibilities of the resulting satisfying system with our setting is given in Theorem 20, which can be proved in a similar way as Theorem 18. Theorem 20. Λ(Horn) = (LH, MProp, |=Prop) Λ(Horn), is both evictionand reception-compatible.

5.2 The Case of Kleene and Priest 3-valued Logics Now, we look at examples of 3-valued logics which are only slightly more complex than propositional logic. The 3-valued logics of Kleene (Kleene 1952) and Priest (Priest 1979) consist of the classical propositional logic in which the formulae might be assigned one of the following three truth values: true (T), false (F) and unknown (U). Consider the following total order on the three values: F < U < T. The satisfaction system for Kleene s 3-valued logics is Λ(K3) = (LProp, M3, |=K3), and for Priest s 3-valued logics is Λ(P3) = (LProp, M3, |=P 3) where LProp is the language of the classical propositional logic, and M3 is the set of all functions v : L {F, U, T} s.t v( φ) = T, if v(φ) = F; v( φ) = U, if v(φ) = U; v( φ) = F, if v(φ) = T. v(φ ψ) = min<({v(φ), v(ψ)}). v(φ ψ) = max<({v(φ), v(ψ)}). The main difference between Kleene s and Priest s 3valued logics lies on the satisfaction relation: for Kleene, v |=K3 φ iff v(φ) = T; while for Priest, v |=P 3 φ iff v(φ) = T or v(φ) = U. Theorem 21 states the compatibility results for these systems. Theorem 21. Λ(K3) and Λ(P3) are reception-compatible but Λ(K3) is reception-compatible, while Λ(P3) is not.

5.3 The Case of Propositional G odel Logic All satisfaction systems studied earlier in this section had only finitely many models. This is not the case in (propositional) G odel logic, one of the most important fuzzy logics (H ajek 1998; Bergmann 2008). We will analyse the compatibilities for G odel logic s satisfaction system next. Let θ (0, 1] and Λ(G odel, θ) = (LG, MG, |=θ G) be a satisfaction system in which LG consists of propositional formulae defined over a nonempty finite set of propositional atoms At; MG is the set of all functions v : L [0, 1] respecting the standard G odel semantics for the boolean connectives (see (Bergmann 2008, page 20)); and v|=θ GB iff v(V φ B { ( a a)} φ) θ, where a At.

We say that Λ(G odel, θ) is the satisfaction system for propositional G odel logic with threshold θ. Theorem 22 states a positive result for Λ(G odel, θ). Despite MG being infinite, the models can be grouped into finitely many equivalence classes w.r.t. satisfaction of bases. Theorem 22. The satisfaction system Λ(G odel, θ) is evictionand reception-compatible.

5.4 The LTL Ne Xt Fragment In the previous subsections, we focused on languages which had only boolean connectives and whose models were valuations on propositional atoms. Here, we consider the LTL logic (Clarke et al. 2018) with the language confined only to the operator X (Ne Xt) as an example of satisfaction system which differs considerably in language and in semantics from the other systems presented before. For clarity, the language of this logic LX is given by the following grammar in BNF φ := p | Xφ, where p At for some fixed non empty set of propositional symbols At. We write Xmp as a shorthand for the nesting of X m times. The formula X0p stands for p. A model of this logic is a pair (M, s) where M is a Kripke structure (see definition at (Clarke et al. 2018)), and s is a initial state of M, called the initial state. Let MX be the set of all such models. A model (M, s) satisfies a formula Xip iff p is labelled at the i-th state of all paths from M starting from s (see (Clarke et al. 2018), for a detailed definition). Let |=X be the satisfaction relation between models and formulae as just defined. The satisfaction system of this logic is the system Λ(LTLX) = (LX, MX, |=X). Within this section, we will write A |=X φ as a shorthand for (M, s)|=Xφ, for all (M, s) A. For reception-compatibility we define the function rcp X and prove its relation to the reception construction in Proposition 23.

Proposition 23. Let B Pf(LX), M MX and rcp X : Pf(LX) P(MX) Pf(LX) defined as

rcp X(B, M) = {φ B | M |= φ}.

It holds that rcp X(B, M) Min FRSups(Mod(B) M).

Even though this logic is reception-compatible, it is not eviction-compatible.

Theorem 24. Λ(LTLX) is reception-compatible but it is not eviction-compatible.

5.5 The Case of Description Logic To analyse the case of Description Logic (DL), we study ALC, which is a prototypical DL that shares many similarities with other expressive logics in the DL family. Here we use the term ontology to refer to a finite set of formulae a finite base. Let NC, NR and NI be countably infinite and pairwise disjoint sets of concept, role, and individual names, respectively. ALC concepts are built according to the rule:

C ::= A | C | (C C) | r.C,

where A NC. An ALC ontology is a set of expressions of the form C(a) | r(a, b) | C D,

where C, D are ALC concepts, a, b NI, and r NR. The semantics of the DLs considered here is standard (Baader et al. 2017).

Theorem 25. Λ(ALC) is neither reception-compatible nor eviction-compatible.

Not being reception-compatible is essentially due to having an infinite signature. Indeed, this is already the case

for the satisfaction system where the language allows only (positive and negative) assertions, which are expressions of the form A(a), r(a, b), A(a), r(a, b), where A NC, r NR, and a, b NI. We denote it by Λ(ABox).

Theorem 26. Λ(ABox) is not reception-compatible but it is eviction-compatible.

Finally, we consider the case in which the signature is finite, that is, the sets NC, NR, NI are disjoint, non-empty, and finite (but models can still be infinite). Our result that Λ(ALC) is not eviction-compatible already holds is this case. So we consider a simpler but popular DL called DLLite R. DL-Lite R role and concept inclusions are expressions of the form S T and B C, respectively, where S, T are role expressions and B, C are concept expressions built through the rules

S ::= r | r , T ::= S | S, B ::= A | S, C ::= B | B,

with r NR and A NC. A DL-Lite R ontology is a set of role and concept inclusions and (positive) assertions, as defined above. We denote by Λ(DL-Lite R) the satisfaction system with the entailment relation given by the standard semantics of DL-Lite R (Baader et al. 2017).

Theorem 27. Λ(DL-Lite R) (with finite signature) is reception-compatible and eviction-compatible.

6 Related Work Finite representation of epistemic states have been addressed in Belief Change literature by representing an agent s knowledge via a finite set of formulae known as a finite belief base (Nebel 1991; Dixon and Wobcke 1993). Belief change operations on belief bases, however, are syntax sensitive: they preserve the syntactic form of the original belief base as much as possible. This syntax sensitivity also appears in traditional approaches for Ontology Repair and Ontology Evolution (Kalyanpur 2006; Suntisrivaraporn 2009). Although finite bases trivially guarantee finite representability, syntax sensitivity might compel drastic loss of information as noticed by Hansson (1993a). The main reason is that applying an operation in the finite base is not equivalent to applying an operation on the epistemic state generated by the same base, in general. The new paradigm we defined performs eviction and reception on the epistemic state generate from the finite base, that is, it is not sensitive to syntax. The problem of loss of information due to syntax sensitivity has been studied in Belief Change pseudo-contraction (Santos et al. 2018). Thus, our paradigm approaches the concept of pseudo-contraction with the extra condition of finite representability. To minimize the drastic loss of syntax sensitive operations, Troquard et al. (2018) proposed to repair DL ontologies by weakening axioms using refinement operators. Building on this study, Baader et al. (2018) devised the theory of gentle repairs, which also aims at keeping most of the information within the ontology upon repair. In fact, gentle repairs are type of pseudo-contractions (Matos et al. 2019). In this same category, we include the Belief Change operations based on concept relaxation (Aiguier et al. 2018).

These studies, however, do not answer the question of finding an optimal solution. Meanwhile, we give conditions that guarantee that our operations perform minimal changes on epistemic states. Baader et al. (2022) propose to repair EL ontologies by modifying only their ABox, preserving as many entailments as possible. Still, in this approach, one cannot contract all necessary kinds of information, as the TBox cannot be modified. Other works in Belief Change that consider finite representability are: (i) revision by Katsuno and Mendelzon (1991) and (ii) base-generated operations by Hansson (1996). In the former, Katsuno and Mendelzon (1991) assumes an agent s epistemic state is represented as a single formula. This is possible because they only consider finitary propositional languages. Hansson (1996) provides a characterisation of Belief Change operations over finite bases but restricted for logics which satisfy all the AGM assumptions (such as classical propositional logic), while we have shown that our approach works in other logics as well. As for Belief Change operation on models, Guerra and Wassermann (2019) consider modifying a single Kripke model into a new one that satisfies a given formula in Linear Temporal Logics (LTL) (Clarke et al. 2018). While they provide an AGM-style characterisation, there is no guarantee of finite representability. Hieke, Kriegel, and Nuradiansyah (2021) devise an approach for contraction by formula in DL EL ontologies that employs the notion of counter-models. Even so, while a model is employed to derive the final outcome of the contraction, the input is still a single formula. Hence, despite using finite bases, our framework is more general because we accept arbitrary sets of models as input.

7 Conclusion and Future Work We introduced a new paradigm of Belief Change: an agent s epistemic state is represented as a finite base, while incoming information are represented as a set of models. The agent can either incorporate the incoming models (via reception) or remove them (via eviction). In either case, the resulting belief base must be finitely representable. The standard rationality postulates of Belief Change do not guarantee finite representability. Hence, we proposed new postulates that capture a notion of minimal change in this setting for both eviction and reception. We also presented two constructive classes of model change operations that are precisely characterised by such sets of rationality postulates. As a case study, we investigated how this new paradigm works in various logics. Eviction can lead to an inconsistent belief base, in the case that all models are removed. If consistency is required, then a more sophisticated model operation could be defined with the caveat that, in behalf of consistency, other models can be assimilated during the removal of an input model. This third model operation is similar in spirit to formula revision. We leave model revision as a future work. We envisage that the results we obtain for eviction and reception shall shed light towards this other operation. Another line of research concerns the effects of partially constraining the structure of the resulting base, in the spirit of pseudo-contractions.

Acknowledgements

Part of this work has been done in the context of CEDAS (Center for Data Science, University of Bergen, Norway). The first author is supported by the ERC project Lossy Preprocessing (LOPRE), grant number 819416, led by Prof Saket Saurabh. The second author is supported by the NFR project Learning Description Logic Ontologies , grant number 316022. The third author is supported by the German Research Association (DFG), project number 424710479.

Aiguier, M.; Atif, J.; Bloch, I.; and Hudelot, C. 2018. Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics. Artificial Intelligence, 256: 160 180. Alchourr on, C. E.; G ardenfors, P.; and Makinson, D. 1985. On the Logic of Theory Change: Partial Meet Contraction and Revision Functions. Journal of Symbolic Logic, 50(2): 510 530. Arias, M.; Khardon, R.; and Maloberti, J. 2007. Learning Horn Expressions with LOGAN-H. J. Mach. Learn. Res., 8: 549 587. Baader, F.; Horrocks, I.; Lutz, C.; and Sattler, U. 2017. An Introduction to Description Logic. Cambridge University Press. Baader, F.; Koopmann, P.; Kriegel, F.; and Nuradiansyah, A. 2022. Optimal ABox Repair w.r.t. Static EL TBoxes: From Quantified ABoxes Back to ABoxes. In The Semantic Web. Springer International Publishing. Baader, F.; Kriegel, F.; Nuradiansyah, A.; and Pe naloza, R. 2018. Making Repairs in Description Logics More Gentle. In KR 2018. AAAI Press. Bergmann, M. 2008. An Introduction to Many-Valued and Fuzzy Logic. Cambridge University Press. Clarke, E. M.; Grumberg, O.; Kroening, D.; Peled, D. A.; and Veith, H. 2018. Model checking, 2nd Edition. MIT Press. ISBN 978-0-262-03883-6. Dalal, M. 1988. Investigations into a Theory of Knowledge Base Revision. In Proceedings of the 7th National Conference on Artificial Intelligence, 475 479. AAAI Press / The MIT Press. De Raedt, L. 1997. Logical settings for concept-learning. Artificial Intelligence, 95(1): 187 201. Delgrande, J. P.; Peppas, P.; and Woltran, S. 2018. General Belief Revision. J. ACM, 65(5): 29:1 29:34. Delgrande, J. P.; and Wassermann, R. 2010. Horn Clause Contraction Functions: Belief Set and Belief Base Approaches. In Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010, Toronto, Ontario, Canada, May 9-13, 2010. AAAI Press. Delgrande, J. P.; and Wassermann, R. 2013. Horn Clause Contraction Functions. J. Artif. Intell. Res., 48: 475 511.

Dixon, S.; and Wobcke, W. 1993. The Implementation of a First-Order Logic AGM Belief Revision System. In ICTAI 1993, 40 47. IEEE Computer Society. Dixon, S. E. 1994. Belief revision: A computational approach. Ph.D. thesis, University of Sydney. Guerra, P. T.; and Wassermann, R. 2019. Two AGM-style characterizations of model repair. Ann. Math. Artif. Intell., 87(3): 233 257. Guimar aes, R.; Ozaki, A.; and Ribeiro, J. S. 2023. Finite Based Contraction and Expansion via Models. ar Xiv preprint ar Xiv:2303.03034. Hansson, S. 1997. Semi-revision. Journal of Applied Non Classical Logics, 7(1-2): 151 175. Hansson, S. O. 1993a. Changes of disjunctively closed bases. Journal of Logic, Language and Information, 2(4): 255 284. Hansson, S. O. 1993b. Reversing the Levi identity. J. Philos. Log., 22(6): 637 669. Hansson, S. O. 1996. Knowledge-Level Analysis of Belief Base Operations. Artificial Intelligence, 82(1-2): 215 235. Hansson, S. O. 1999. A Textbook of Belief Dynamics: Theory Change and Database Updating. Applied Logic Series. Kluwer Academic Publishers. Hieke, W.; Kriegel, F.; and Nuradiansyah, A. 2021. Repairing EL TBoxes by Means of Countermodels Obtained by Model Transformation. In Homola, M.; Ryzhikov, V.; and Schmidt, R. A., eds., Proceedings of the 34th International Workshop on Description Logics (DL 2021), Bratislava, Slovakia, September 19-22, 2021, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org. H ajek, P. 1998. Metamathematics of Fuzzy Logic. Springer Netherlands. ISBN 9789401153003. Kalyanpur, A. 2006. Debugging and repair of OWL ontologies. Ph.D. thesis, University of Maryland. Katsuno, H.; and Mendelzon, A. O. 1991. Propositional knowledge base revision and minimal change. Artificial Intelligence, 52(3): 263 294. Kleene, S. 1952. Introduction to Metamathematics. Princeton, NJ, USA: North Holland. Matos, V. B.; Guimar aes, R.; Santos, Y. D.; and Wassermann, R. 2019. Pseudo-contractions as Gentle Repairs. In Lecture Notes in Computer Science, 385 403. Springer International Publishing. Nebel, B. 1990. Reasoning and Revision in Hybrid Representation Systems, volume 422 of Lecture Notes in Computer Science. Springer. Nebel, B. 1991. Belief Revision and Default Reasoning: Syntax-Based Approaches. In KR 1991, 417 428. Morgan Kaufmann. Priest, G. 1979. The Logic of Paradox. Journal of Philosophical Logic, 8(1): 219 241. Ribeiro, J. S.; Nayak, A.; and Wassermann, R. 2018. Towards Belief Contraction without Compactness. In KR 2018, 287 296. AAAI Press.

Ribeiro, J. S.; Nayak, A.; and Wassermann, R. 2019a. Belief Change and Non-Monotonic Reasoning Sans Compactness. In AAAI 2019, 3019 3026. AAAI Press. Ribeiro, J. S.; Nayak, A.; and Wassermann, R. 2019b. Belief Update without Compactness in Non-finitary Languages. In IJCAI 2019, 1858 1864. ijcai.org. Ribeiro, M. M. 2013. Belief Revision in Non-Classical Logics. Springer London. Santos, Y. D.; Matos, V. B.; Ribeiro, M. M.; and Wassermann, R. 2018. Partial meet pseudo-contractions. International Journal of Approximate Reasoning, 103: 11 27. Suntisrivaraporn, B. 2009. Polynomial time reasoning support for design and maintenance of large-scale biomedical ontologies. Ph.D. thesis, Dresden University of Technology, Germany. Troquard, N.; Confalonieri, R.; Galliani, P.; Pe naloza, R.; Porello, D.; and Kutz, O. 2018. Repairing Ontologies via Axiom Weakening. In AAAI 2018, 1981 1988. AAAI Press.