# belief_update_within_propositional_fragments__243f300f.pdf

Journal of Artificial Intelligence Research 61 (2018) 807-834 Submitted 04/17; published 04/18

Belief Update within Propositional Fragments

Nadia Creignou nadia.creignou@univ-amu.fr Aix Marseille Univ, Universit e de Toulon, CNRS, LIS, Marseille, France 163 av. de Luminy, 13288, Marseille, France

Ra ıda Ktari raida.ktari@isims.usf.tn Institut Sup erieur d Informatique et de Multim edia de Sfax, Universit e de Sfax, pˆole technologique de Sfax, Sakiet Ezzit 3021, Tunisie

Odile Papini odile.papini@univ-amu.fr Aix Marseille Univ, Universit e de Toulon, CNRS, LIS, Marseille, France 163 av. de Luminy, 13288, Marseille, France

Belief change within the framework of fragments of propositional logic is one of the main and recent challenges in the knowledge representation research area. While previous research works focused on belief revision, belief merging, and belief contraction, the problem of belief update within fragments of classical logic has not been addressed so far. In the context of revision, it has been proposed to refine existing operators so that they operate within propositional fragments, and that the result of revision remains in the fragment under consideration. This approach is not restricted to the Horn fragment but also applicable to other propositional fragments like Krom and affine fragments. We generalize this notion of refinement to any belief change operator. We then focus on a specific belief change operation, namely belief update. We investigate the behavior of the refined update operators with respect to satisfaction of the KM postulates and highlight differences between revision and update in this context.

1. Introduction

Belief update consists in incorporating into an agent s beliefs new information reflecting a change in her environment. The problem of belief update first appeared in the domain of databases for updating deductive databases (Fagin, Ullman, & Vardi, 1983). Significant links quickly emerged with works developed in artificial intelligence on belief change, especially on belief revision. Keller and Winslett (1985), and later Katsuno and Mendelzon (1992) contributed to a better understanding regarding the distinction between belief revision and belief update when they proposed a common framework to represent these operations. Belief revision happens when new information is introduced in a static environment, while belief update occurs in a changing environment. From a logical point of view, when the agent s beliefs are represented by a logical formula, revision makes the models of this formula evolve as a whole towards the closest models of new information. In contrast, update makes each model of this formula locally evolve towards the closest models of new information.

c 2018 AI Access Foundation. All rights reserved.

Creignou, Ktari, & Papini

Postulates characterizing the rational behavior of update operators have been proposed by Katsuno and Mendelzon (KM) (1992) in the same spirit as the seminal AGM postulates for revision (Alchourr on, G ardenfors, & Makinson, 1985). Belief update gave rise to several studies, in most cases within the framework of propositional logic, and concrete belief update operators have been proposed mainly according to a semantic (model-based) point of view (Forbus, 1989; del Val & Shoham, 1994; Dubois & Prade, 1993; Zhang & Foo, 2000; Boutilier, 1998; Friedman & Halpern, 1999; Herzig & Rifi, 1999; Doherty, Lukaszewicz, & Madalinska-Bugaj, 2000; Lang, 2007; Delgrande, Jin, & Pelletier, 2014). Many studies focused on belief change within the framework of propositional logic fragments, particularly on belief contraction (Booth, Meyer, Varzinczak, & Wassermann, 2011; Zhuang & Pagnucco, 2014; Delgrande & Wassermann, 2013), on belief revision (Cadoli & Scarcello, 2000; Delgrande & Peppas, 2015; Zhuang, Pagnucco, & Zhang, 2013; Putte, 2013; Creignou, Papini, Pichler, & Woltran, 2014) and more recently on belief merging (Creignou, Papini, R ummele, & Woltran, 2016). However, as far as we know, the problem of belief update within fragments of propositional logic has not been addressed so far, except for complexity results in the Horn case (Eiter & Gottlob, 1992; Liberatore & Schaerf, 2001). The motivation of such a study is twofold. First, in many applications, the language is restricted a priori. For instance, a rule-based formalization of expert knowledge is much easier to handle for standard users. In the case of update they expect an outcome in the same language. Second, some fragments of propositional logic allow for efficient reasoning methods, and then an outcome of update within such a fragment can be evaluated efficiently. It seems thus natural to investigate how known update operators can be refined such that the result of update remains in the fragment under consideration. Formally, let L1 be a propositional fragment and given two formulas ψ, µ P L1, the main obstacle hereby is that there is no guarantee that the outcome of an update, denoted by ψ µ, remains in L1 as well. Let us consider the following example inspired from the one used by Katsuno and Mendelzon (1992) where the beliefs describe two objects A and B inside a room. There is a table in the room and the objects may be on the table or not. Suppose a means object A is on the table and b means object B is on the table . Assume that the agent s beliefs are represented by the formula ψ a, which expresses that object A is on the table. Suppose a robot is sent into the room with the instruction to achieve a situation in which either object A or object B is not on the table. This change is represented by the formula µ a _ b. The formulas ψ and µ are Horn formulas, however updating ψ by µ in using Forbus (1989) or Winslett s operator (1988) results in a formula equivalent to φ pa _ bq p a _ bq, which is not a Horn formula and is not equivalent to any Horn formula (because its set of models is not closed under intersection, while this property characterizes the formulas in Horn, 1951)1. In this paper, we generalize the notion of refinement, initially defined for revision (Creignou et al., 2014), to any belief change operator defined from L ˆ L to L where L denotes propositional logic. A refinement adapts a belief change operator defined in a propositional setting such that it can be applicable in a propositional fragment. The basic properties of a refinement are first to guarantee the outcome of the belief change operation to remain within the fragment and second to approximate the behavior of the original belief

1. Note that in this example, revision and update do not coincide.

Belief Update within Propositional Fragments

change operator, in particular to keep the behavior of the original operator unchanged if the result already fits in the fragment. We characterize these refined operators in a constructive way. We exploit the notion of refinement for belief update operators. We then study how refined belief update operators behave with respect to satisfaction of the KM postulates that characterize rational update operators. Indeed, we show that the basic KM postulates p U1q p U4q are preserved for any refinement in any fragment. We study the limits of the preservation of the other postulates, as well. For this we focus on the refinements of Forbus (1989) and Winslett s operators (1988) within the Horn, Krom and affine fragments. Our approach handles a natural extension that consists in investigating update when only the formula representing the initial agent s beliefs, and not necessarily the formula reflecting the new information, is in the fragment. All along this study we shed some light on subtle differences between update and revision.

The paper is organized as follows. We start with some preliminaries. In Section 2.1 we recall some basic facts about propositional logic. In Section 2.2 we define the fragments of propositional logic we are interested in. In Section 2.4 we give a short reminder of belief update. Section 3 deals with refinements in the general context of belief change. In Section 4 we focus on refinements of update operators. Finally we conclude in Section 5.

2. Preliminaries

In this section we give the relevant material on propositional logic, characterizable fragments, belief revision and belief update.

2.1 Propositional Logic

Let L be the language of propositional logic built on an infinite countable set of variables (atoms) denoted by V and equipped with standard connectives Ñ, _, , , the exclusive or connective , and constants J, K. A literal is an atom or its negation. A clause is a disjunction of literals. A clause is called Horn if at most one of its literals is positive; Krom if it consists of at most two literals. A -clause is defined like a clause but using exclusive - instead of standard - disjunction. We identify LHorn (resp., LKrom, Laffine) as the set of all formulas in L being conjunctions of Horn clauses (resp., Krom clauses, -clauses). Let U be a finite set of atoms. An interpretation over U is represented either by a set m Ď U of atoms (corresponding to the variables set to true) or by its corresponding characteristic bit-vector of length |U|, the atoms being considered in lexicographical order. For instance if we consider U tx1, . . . , x6u, the interpretation x1 x3 x6 1 and x2 x4 x5 0 will be represented either by tx1, x3, x6u or by p1, 0, 1, 0, 0, 1q. For any formula φ, let Varpφq denote the set of variables occurring in φ. As usual, if an interpretation m defined over U satisfies a formula φ such that Varpφq Ď U, we call m a model of φ. By Modpφq we denote the set of all models (over U) of φ. A formula ψ is complete over U if Varpψq Ď U and if for any µ P L such that Varpµq Ď U, we have ψ |ù µ or ψ |ù µ. In an equivalent way, a satisfiable formula ψ is complete over

Creignou, Ktari, & Papini

U 2 if it has exactly one model over U. Moreover, ψ |ù φ if Modpψq Ď Modpφq and ψ φ if Modpψq Modpφq. For fragments L1 Ď L, we use TL1pψq tφ P L1 | ψ |ù φu.

2.2 Characterizable Fragments of Propositional Logic

Let B be the set of Boolean functions β : t0, 1uk Ñ t0, 1u with k ě 1, that are symmetric (i.e., for all permutations σ, βpx1, . . . , xkq βpxσp1q, . . . , xσpkqq), and 0and 1-reproductive (i.e., for every x P t0, 1u, βpx, . . . , xq x). Examples of such functions are: The binary AND function denoted by , the ternary MAJORITY function, maj3px, y, zq 1 if at least two of the variables x, y and z are set to 1, and the ternary XOR function 3px, y, zq x y z. Recall that we consider interpretations also as bit-vectors. We thus extend Boolean functions to interpretations by applying coordinate-wise the original function. So, if m1, . . . , mk P t0, 1un, then βpm1, . . . , mkq is defined by

pβpm1r1s, . . . , mkr1sq, . . . , βpm1rns, . . . , mkrnsqq,

where mris is the i-th coordinate of the interpretation m. The next definition gives a general formal definition of closure.

Definition 1. Given a set M Ď 2U of interpretations and β P B, we define Clβp Mq, the closure of M under β, as the smallest set of interpretations that contains M and that is closed under β, i.e., if m1, . . . , mk P Clβp Mq, then βpm1, . . . , mkq P Clβp Mq.

For instance it is well-known that the set of models of any Horn formula is closed under , and actually this property characterizes Horn formulas. Closures satisfy monotonicity: if M Ď N, then Clβp Mq Ď Clβp Nq. Moreover, if |M| 1, then Clβp Mq M (because by assumption β is 0and 1-reproducing); finally, we always have Clβp Hq H. We can now use these concepts to identify fragments of propositional logic. Additionally, we want fragments to fulfill some natural properties and for technical reasons we require closure under conjunction.

Definition 2. Let β P B. A set L1 Ď L of propositional formulas is a β-fragment (or a characterizable fragment) if: (i) For all ψ P L1, Modpψq Clβp Modpψqq. (ii) For all M Ď 2U with M Clβp Mq there exists ψ P L1 with Modpψq M. (iii) If φ, ψ P L1 then φ ψ P L1.

We will often (implicitly) use the following fact: Let µ be a formula in L and L1 be a β-fragment. Let µ be a formula in L1 such that Modp µq Clβp Modpµqq (such a formula exists according to (ii) in Definition 2). Then TL1pµq TL1p µq.

Many fragments of propositional logic allow for efficient reasoning methods. When representing knowledge, storing beliefs as a formula of a known tractable class is thus of interest. The most famous characterizable fragments, which are the largest in which satisfiability is tractable, are: LHorn which is an -fragment, LKrom which is a maj3-fragment and Laffine which is a 3-fragment (Horn, 1951; Schaefer, 1978).

2. When U is not mentioned, it implicitly means that U is the set of variables occurring in formulas under consideration

Belief Update within Propositional Fragments

An immediate generalization of our framework to fragments characterized by a closure property under a finite number of functions (and not only one), leads to infinitely many fragments, which are organized in a lattice, known as Post s (1941) lattice. The complexity of many computational tasks has been studied in these fragments (see the survey in Creignou & Vollmer, 2008). The complexity of reasoning tasks within the Krom fragment has been recently investigated (Creignou, Pichler, & Woltran, 2017).

2.3 Belief Revision

Belief revision consists in incorporating a new belief, changing as few as possible of the original beliefs while preserving consistency. More formally, a revision operator denoted by , is a function from L ˆ L to L that maps two formulas ψ (the initial agent s beliefs) and µ (new information) to a new formula ψ µ (the revised agent s beliefs). In the AGM paradigm (Alchourr on et al., 1985), postulates were proposed for belief revision when beliefs are modeled by a theory (or belief set), Katsuno and Mendelzon (1991) reformulated them when a theory is represented by a propositional formula. We recall the KM postulates for belief revision. Let ψ, ψ1, ψ2, µ, µ1, µ2 P L. (R1) ψ µ |ù µ. (R2) If ψ µ is satisfiable, then ψ µ ψ µ. (R3) If µ is satisfiable, then so is ψ µ. (R4) If ψ1 ψ2 and µ1 µ2, then ψ1 µ1 ψ2 µ2. (R5) pψ µq φ |ù ψ pµ φq. (R6) If pψ µq φ is satisfiable, then also ψ pµ φq |ù pψ µq φ. The meaning of these postulates is the following. Postulate (R1) specifies that the added formula belongs to the revised belief set. Postulate (R2) is concerned with following issue: if the added formula does not contradict the initial belief set then the revised belief set is represented by the conjunction of the added formula and the formula representing the initial belief set, in other words if the incorporation of new information does not cause problem, we just add the new belief to the existing knowledge. Postulate (R3) ensures that no inconsistency is introduced in the revised belief set. Postulate (R4) expresses the principle of irrelevance of the syntax, and (R5) and (R6) state that revising by the conjunction of two pieces of information amounts to a revision by the first one and a conjunction of the second one whenever possible (whenever the second piece of information does not contradict any belief resulting from the first revision). Katsuno and Mendelzon (1991) showed that a revision satisfying the AGM postulates is equivalent to a total preorder on interpretations, which reflects a plausibility ordering on interpretations. More formally, a faithful assignment is a function that maps any propositional formula ψ to a pre-order over interpretations ďψ such that:

1) If ω |ù ψ and ω1 |ù ϕ, then ω ψ ω1.

2) If ω |ù ψ and ω1 |ù ψ, then ω ăψ ω1.

3) If ψ1 ψ2 then ďψ1 ďψ2.

They provided the following representation theorem.

Creignou, Ktari, & Papini

Theorem 3. (Katsuno & Mendelzon, 1991) A revision operator satisfies the postulates (R1) (R6) if and only if there exists a faithful assignment that maps each formula ψ to a total preorder ďψ such that Modpψ µq Minp Modpµq, ďψq.

2.4 Belief Update

Belief update consists in incorporating into an agent s beliefs new information reflecting a change in her environment. More formally, an update operator, denoted by , is a function from L ˆ L to L that maps two formulas ψ (the initial agent s beliefs) and µ (new information) to a new formula ψ µ (the updated agent s beliefs). We recall the KM postulates for belief update (Katsuno & Mendelzon, 1991). Let ψ, ψ1, ψ2, µ, µ1, µ2 P L. (U1) ψ µ |ù µ. (U2) If ψ |ù µ, then ψ µ ψ. (U3) If ψ and µ are satisfiable then so is ψ µ. (U4) If ψ1 ψ2 and µ1 µ2, then ψ1 µ1 ψ2 µ2. (U5) pψ µq φ |ù ψ pµ φq. (U6) If pψ µ1q |ù µ2 and pψ µ2q |ù µ1, then ψ µ1 ψ µ2. (U7) If ψ is complete, then pψ µ1q pψ µ2q |ù ψ pµ1 _ µ2q. (U8) pψ1 _ ψ2q µ pψ1 µq _ pψ2 µq. (U9) If ψ is complete and pψ µq φ is satisfiable, then ψ pµ φq |ù pψ µq φ.

These postulates have been discussed in several papers (e.g., Herzig & Rifi, 1999). Postulate p U1q says that the models of the updated agent s beliefs have to be models of new information. Postulate p U4q states the irrelevance of syntax. Postulate p U5q expresses minimality of change. The three postulates p U1q, p U4q and p U5q directly correspond to the belief revision postulates p R1q, p R4q and p R5q respectively. Postulate p U2q differs from p R2q, the latter stating that if ψ µ is satisfiable then ψ µ ψ µ. A consequence of p U2q for update is that once an inconsistency is introduced in the initial beliefs there is no way to eliminate it (Katsuno & Mendelzon, 1991). Note that this is not the case for belief revision. Furthermore, p U3q is a weaker version of p R3q. The latter states that if µ is satisfiable then so is ψ µ, while in order to ensure the consistency of the result of update p U3q requires an additional condition, namely that the initial beliefs be consistent as well. Postulates p U6q, p U7q and p U8q are specific to update operators. The eighth postulate p U8q, which means that an update operator should give each of the models of the initial beliefs equal consideration, is considered as the most uncontroversial one. Finally, p U9q is a weaker version of p R6q, it is similar but restricted to complete formulas ψ. Katsuno and Mendelzon (1991)showed that an update operator corresponds to a set of preorders on interpretations. More formally, a pointwise faithful assignment is a function that maps any interpretation m to a pre-order over interpretations ďm, such that for any interpretation m1, if m1 m then m ăm m1. They provided the following representation theorem.

Theorem 4. (Katsuno & Mendelzon, 1992)

Belief Update within Propositional Fragments

An update operator satisfies the postulates (U1) (U9) if and only if there exists a pointwise faithful assignment that maps each interpretation m to a total preorder ďm such that Modpψ µq Ť m PModpψq minp Modpµq, ďmq.

An update operator satisfies the postulates (U1) (U8) if and only if there exists a pointwise faithful assignment that maps each interpretation m to a partial preorder ďm such that Modpψ µq Ť m PModpψq minp Modpµq, ďmq.

The representation theorems, Theorem 3 and Theorem 4, pinpoint the differences between revision and update. Update stems from a pointwise minimization, model by model of ψ, while revision stems from a global minimization on all the models of ψ. Update operators, for each model m of ψ, select the set of models of µ that are the closest to m, while revision operators select the set of models of µ that are the closest to the set of models of ψ. Note that when there exists only one model of ψ (which is the case when ψ is complete) revision and update coincide. The following example illustrates the difference between revision and update.

Example 5. We come back to the example given in the introduction where the beliefs describe two objects A and B inside a room. The agent s beliefs are represented by the formula ψ a, which expresses that object A is on the table. Let us recall that a robot is sent into the room with the instruction to achieve a situation in which either object A or object B is not on the table. This change is represented by the formula µ a _ b. We have ψ, µ P L with Modpψq ttau, ta, buu and Modpµq ttau, tbu, Hu. Let m, m1

be two interpretations, m m1 denotes the symmetric difference between m and m1. The global minimization of the cardinality of the symmetric difference between the models of ψ and the models of µ provides Modpψ µq ttauu. In contrast, the minimization of the cardinality of the symmetric difference between each model of ψ and the models of µ gives Modpψ µq ttau, tbuu. Note that revision selects tau as the only model of the changed beliefs. However after the robot s action, all we know is that either object A or object B is not on the table. There is no reason to conclude that only object B is not on the table as does revision, which excludes the situation where object A is not on the table.

Several update operators have been proposed. We now recall the two best known modelbased update operators on which we will focus, namely Forbus (1989) and Winslett s operators (1988). In these model-based update operators the closeness between models relies on the symmetric difference between models, that is the set of propositional variables on which they differ. Forbus (1989) operator was introduced in the context of qualitative physics. This operator is analogous to Dalal s (1988) revision operator and measures minimality of change by cardinality of model change. More formally, let ψ and µ be two propositional formulas, and m and m1 be two interpretations, m m1 denotes the symmetric difference between m and m1 and | |min m pµq denotes the minimum number of variables in which m and a model of µ differ and is defined as mint|m m1| : m1 P Modpµqu. Forbus operator is now defined as: Modpψ F µq Ť m PModpψqtm1 P Modpµq : |m m1| | |min m pµqu. This operator satisfies (U1)-(U8) (Katsuno & Mendelzon, 1991) and (U9) (Herzig & Rifi, 1999). This update operator is illustrated in the following example.

Creignou, Ktari, & Papini

Modpψq Modpµq {b,c} {c,d} {a,b,d} {c} {d} {b} H {a,b,c} 1 3 2 2 4 2 3 {a,b,c,d,e} 3 3 2 4 4 4 5

Table 1: Example for F

Modpψq Modpµq {b,c} {c,d} {a,b,d} {c} {d} {b} H {a,b,c} {a} {a,b,d} {c,d} {a,b} {a,b,c,d} {a,c} {a,b,c} {a,b,c,d,e} {a,d,e} {a,b,e} {c,e} {a,b,d,e} {a,b,c,e} {a,c,d,e} {a,b,c,d,e}

Table 2: Example for W

Example 6. Let ψ, µ P L such that Modpψq tta, b, cu, ta, b, c, d, euu and Modpµq ttb, cu, tc, du, ta, b, du, tcu, tdu, tbu, Hu. The result of update could be read in Table 1. Each line of the table gives the cardinalities of the symmetric differences between the corresponding model of ψ and the models of µ. The minimal cardinalities are written in bold. Hence Modpψ F µq ttb, cu, ta, b, duu.

Winslett s (1988) operator, also called PMA (Possible Models Approach) was introduced for reasoning about actions and change. This operator is analogous to Satoh s (1988) revision operator and interprets minimal change in terms of set inclusion instead of cardinality on model difference. More formally, min m pµq denotes the minimal difference between m and a model of µ and is defined as minĎptm m1 : m1 P Modpµquq. Winslett s operator is now defined as: Modpψ W µq Ť m PModpψqtm1 P Modpµq : m m1 P min m pµqu. This operator satisfies p U1q p U8q (Katsuno & Mendelzon, 1991) but does not satisfy p U9q (Ktari, 2016). Winslett s operator W behaves differently from Forbus operator F (1989) as illustrated in the following example.

Example 7. Let ψ, µ P L from Example 6. The result of update could be read in Table 2. Each line of the table gives the symmetric differences between the corresponding model of ψ and the models of µ. The minimal subsets with respect to set inclusion are written in bold. Hence Modpψ W µq ttb, cu, tc, du, ta, b, duu Modpψ F µq.

In this paper, we are interested in update operators which are tailored for certain fragments. We say that satisfies the postulates (Ui) pi P t1, . . . , 9uq in a fragment L1 Ď L if these postulates hold when restricted to formulas from L1.

3. Refinements of Belief Change Operators

Refinements have been defined within the context of belief revision (Creignou et al., 2014) and may be naturally considered for any belief change operation. The idea is to use well-established belief change operators in order to define rational belief change operators that are well-suited for characterizable fragments of propositional

Belief Update within Propositional Fragments

logic. Given a propositional fragment L1 and a propositional belief change operator , a refinement of consists of a new operator , which is built from and not too different from , that operates within L1 and is such that the result of change remains in L1. Roughly speaking the goal is that the difference of behavior between and obeys a kind of principle of minimal change in the sense that if the original operator gives a result that is already in the fragment, then the refined operator should do nothing more, and in any case it should not increase the logical consequences of the original result. In the following we first define formally a few natural basic properties for refinements, then we show how such refinements can be explicitly obtained.

Definition 8. Let L1 be a propositional fragment and : L ˆ L Ñ L a belief change operator. We call an operator : L1 ˆ L1 Ñ L1 a -refinement for L1 if it satisfies the following properties, for each ψ, ψ1, µ, µ1 P L1.

consistency: ψ µ is satisfiable if and only if ψ µ is satisfiable.

equivalence: If ψ µ ψ1 µ1 then, ψ µ ψ1 µ1.

containment: TL1pψ µq Ď TL1pψ µq.

invariance: If ψ µ P L1, then TL1pψ µq TL1pψ µq.

Let us briefly discuss these properties. The first two conditions are rather independent from L1, but relate the refined operator to the original belief change in certain ways. To be more precise, consistency states that the refined operator should yield a consistent belief change exactly if the original operator does so. Equivalence means that the definition of the -operator should not be syntax-dependent, belief changes which are equivalent w.r.t are also equivalent w.r.t. . Containment ensures that can be seen as a form of approximation of when applied in the L1 fragment, while invariance states that in case behaves as expected (i.e., the belief change is contained in L1) there is no need for to do something additional.

When considering a model-based operator it seems that such a refinement can be obtained as follows. Let L1 be a β-fragment and ψ and µ two formulas in L1. Let be a model-based belief change operator. In order to set a refinement, we first compute the set of models of ψ µ, denoted by M, we then apply a mapping to M in order to obtain a set of models N that is a set of models of a formula in L1. We call such a mapping a β-mapping since N has to be closed under β. In the following we prove that indeed all possible refinements can be obtained that way. This characterization of all possible refinements requires the definition of the notion of β-mapping.

Definition 9. Given β P B, we define a β-mapping, fβ, as an application from sets of models into sets of models, fβ : 22U ÝÑ 22U, such that for every M Ď 2U:

1. Clβpfβp Mqq fβp Mq, i.e., fβp Mq is closed under β.

2. fβp Mq Ď Clβp Mq.

Creignou, Ktari, & Papini

3. if M Clβp Mq, then fβp Mq M.

4. If M H, then fβp Mq H.

As explained above the underlying idea of functions fβ is to take a set of models Modpψ µq and to return a set of models fβp Modpψ µqq, thus defining a refinement of the operator . The outcome has to be closed under β (1) since we want to get a belief change into formulas from the β-fragment, and should not add any further interpretations (2) in order to satisfy containment, cf. Definition 8. Since we want to capture refinements of operators there is no need to change the behavior of the original operator as long as it provides a result in the desired fragment (3). Property (4) takes care of consistency, cf. Definition 8. Thus, the concept of β-mapping allows us to define a family of refined operators for the fragments of propositional logic as follows.

Definition 10. Let : LˆL ÝÑ L be a belief change operator and L1 Ď L be a β-fragment of propositional logic with β P B. For a β-mapping fβ, we denote with fβ : L1 ˆ L1 ÝÑ L1

the belief change operator for L1 defined as Modpψ fβµq : fβp Modpψ µqq. The class r , L1s contains all operators fβ where fβ is a β-mapping.

The next proposition is central in reflecting that the above class captures all refined operators we had in mind. A similar result was obtained in Creignou et al. (2014) for basic (revision) operators, i.e., operators satisfying J µ µ. This assumption was used to prove that any -refinement can be defined through a β-mapping. We give here an alternative proof that does not rely on this assumption.

Proposition 11. Let : L ˆ L ÝÑ L be a belief change operator and L1 Ď L be a characterizable fragment of propositional logic. Then, r , L1s is the set of all -refinements for L1.

Proof. Since L1 is a characterizable fragment it is also a β-fragment for some β P B. We first show that any operator from the class r , L1s is a -refinement of L1. Let fβ P r , L1s. We have to show that it satisfies the properties of Definition 8. Consistency for fβ: Let ψ, µ P L1. If Modpψ µq H then Modpψ fβµq fβp Modpψ µqq H by Property 4 in Definition 9. In case, Modpψ µq H, we make use of the fact that Clβp Hq H holds for all β P B. By Property 2 in Definition 9, we get Modpψ fβµq fβp Modpψ µqq Ď Clβp Modpψ µqq H. Equivalence for fβ is clear by definition and since fβ is defined on sets of models. To show containment for fβ, let φ P TL1pψ µq, i.e., φ P L1 and Modpψ µq Ď Modpφq. We have Clβp Modpψ µqq Ď Clβp Modpφqq by monotonicity of Clβ. By Property 2 of Definition 9, Modpψ fβµq Ď Clβp Modpψ µqq. Since φ P L1 we have Clβp Modpφqq Modpφq. Thus, Modpψ fβµq Ď Modpφq, i.e., φ P TL1pψ fβµq. Finally, we require invariance for fβ: In case ψ µ P L1, we have Clβp Modpψ µqq Modpψ µq since L1 is a β-fragment. By Property 3 in Definition 9, we have Modpψ fβµq fβp Modpψ µqq Modpψ µq. Thus TL1pψ fβµq TL1pψ µq as required. For the converse, let be a -refinement for L1. We show that P r , L1s. Let f be defined as follows for any set M of interpretations: fp Hq H and for M H, if there

Belief Update within Propositional Fragments

exists a pair pψM, µMq of formulas from L1 such that ModpψM µMq M, then we define fp Mq ModpψM µMq, otherwise fp Mq Clβp Mq. Thus the refined operator behaves like the operator f. We show that such a mapping f is a β-mapping. Note that since is a β-refinement, it satisfies the property of equivalence, thus the actual choice of the pair pψM, µMq is not relevant, i.e., given M, and pairs pψM, µMq, pψ1 M, µ1 Mq such that ModpψM µMq Modpψ1 M µ1 Mq M, we have that ψM µM is equivalent to ψ1 M µ1 M. Thus, f is welldefined. We continue to show that the four properties in Definition 9 hold for f. Property 1 is ensured since for every M, fp Mq is closed under β. Indeed, either fp Mq ModpψM µMq and since ψM µM P L1 its set of models is closed under β, or fp Mq Clβp Mq. Let us show Property 2 , i.e., fp Mq Ď Clβp Mq for any set of interpretations M. It is obvious when M H (then fp Mq H), as well as when fp Mq Clβp Mq. Otherwise fp Mq ModpψM µMq and since satisfies containment ModpψM µMq Ď Clβp ModpψM µMq. Therefore in any case we have fp Mq Ď Clβp Mq. For showing Property 3 let us consider M H such that M Clβp Mq. If fp Mq Clβp Mq, then fp Mq M. Otherwise, fp Mq ModpψM µMq where ψM, µM P L1 such that ModpψM µMq M. Since satisfies invariance ModpψM µMq M. Thus, in any case, fp Mq M. Property 4 is ensured by consistency of .

Hence, β-mappings allow us to define refined belief change operators. We give some examples of β-mappings in the next section (see Section 4.2) and study how they perform to refine update operators.

4. Update Operators within Fragments

The previous section presented refinements for any belief change operation. We now focus on refinements for belief update. We recall that a belief update operator is a function : L ˆ L to L that maps a formula ψ representing the initial agent s beliefs and a formula µ encoding a change in her environment to a new formula ψ µ representing the updated agent s beliefs. In this section we first present some update operators that are well-suited for any characterizable fragment (Section 4.1). Then we turn to update operators that require refinements. We first propose some β-mappings (Section 4.2) and then study the logical properties of the refined operators they define (Section 4.3). Finally we address the question of refining update operators so that they can handle the case where only the formula representing the agent s beliefs is in the fragment (Section 4.4).

4.1 Dependence-Based Update Operators

There exists a family of update operators that is well-suited for any characterizable fragment, i.e., that provides a result in the fragment, namely dependence-based update operators (Herzig & Rifi, 1999). More formally, a dependence is a function that assigns each atom a a set of atoms deppaq. This dependence function is extended to formulas by deppµq Ť a PVarpµq deppaq.

Creignou, Ktari, & Papini

Herzig s update operator (Herzig & Rifi, 1999) is a dependence-based update operator denoted by HZ and defined by

Modpψ HZ µq tm1 P Modpµq|Dm P Modpψq : m m1 Ď deppµqu.

Hegner s (1987) operator, denoted by H, is a special case of Herzig s operator where deppµq Varpµq, and thus is defined by

Modpψ H µq tm1 P Modpµq|Dm P Modpψq : m m1 Ď Varpµqu.

The following proposition shows that these two update operators are well-suited for any characterizable fragments.

Proposition 12. Let L1 be a characterizable fragment of propositional logic. Given two formulas ψ, µ P L1, then ψ HZ µ P L1 (in particular, ψ H µ P L1).

Proof. Let L1 be a β-fragment, ψ and µ two formulas of L1. Let n1, ..., nk P Modpψ HZ µq. According to the definition of Herzig s operator (Herzig & Rifi, 1999), there exist models m1, ..., mk P Modpψq, such that for each i 1, ..., k, we have ni mi Ď deppµq. Consider βpn1, ..., nkq βpm1, ..., mkq. If x R deppµq then for each i, we have nipxq mipxq, and thus, βpn1pxq, ..., nkpxqq βpm1pxq, ..., mkpxqq. Therefore, βpn1, ..., nkq βpm1, ..., mkq Ď deppµq. Moreover, we have µ P L1, thus βpn1, ..., nkq P Modpµq. Similarly, ψ P L1, thus βpm1, ..., mkq P Modpψq. Hence, βpn1, ..., nkq P Modpψ HZ µq. Therefore, Modpψ HZ µq is closed under β, hence ψ HZ µ P L1.

The following example illustrates the behavior of these dependence-based update operators.

Example 13. Let ψ a b and µ a be Horn formulas. We have Modpψq t Hu, Modpµq ttau, ta, buu and Varpµq tau. Suppose deppµq ta, bu, we have Modpψ HZµq ttau, ta, buu and Modpψ H µq ttauu. Therefore, the result of update is also in LHorn.

All update operators considered in this paper proceed as follows to compute the update of ψ by µ: A model m1 of µ is a model of the updated beliefs if there is a model m of ψ such that the distance between m and m1, measured by their symmetric difference m m1, satisfies some property. An important feature of the dependence-based update operators, not shared by Forbus (1989) and Winslett s operators (1988), is that the property m m1

has to satisfy depends on µ, and not on m.

We now turn to update operators that are not directly suited for fragments of propositional logic and for which refinements make sense. Thanks to Proposition 11, given an update operator, the family of all its possible update refinements, [ , L1], is the set of operators fβ where fβ is a β-mapping. For this reason we first present different β-mappings and next study the logical properties of the refined operators they define.

Belief Update within Propositional Fragments

4.2 Examples of Refined Belief Update Operators

We now give some examples of β-mappings. In the following, let : L ˆ L Ñ L be a belief change operator, and L1 Ď L be a fragment of propositional logic such that L1 is a β-fragment for some β P B. A natural β-mapping is the Clβ function that leads to the definition of a closedbased refined belief change operator denoted by Clβ and given by Modpψ Clβµq Clβp Modpψ µqq. In the following all refined belief change operators are illustrated in the particular case of belief update operators. The following examples illustrate the closed-based refinement for several propositional fragments.

Example 14. Let ψ and µ be Horn formulas such that Modpψq tta, b, cu, ta, b, c, d, euu and Modpµq ttb, cu, tc, du, ta, b, du, tcu, tdu, tbu, Hu as in Example 6. Such formulas exist since their sets of models are closed under intersection. We have Modpψ F µq ttb, cu, ta, b, duu and Modpψ W µq ttb, cu, tc, du, ta, b, duu that are not closed under intersection. So, neither ψ F µ nor ψ W µ is in LHorn. The refined operators Cl F and Cl W are defined as Modpψ Cl F µq Cl p Modpψ F µqq ttb, cu, ta, b, du, tbuu and Modpψ Cl W µq Cl p Modpψ W µqq ttb, cu, tc, du, ta, b, du, tbu, tcu, tdu, Hu.

We give now an example that holds both in the Horn and the Krom fragments.

Example 15. Consider ψ a b c and µ p a _ bq p b _ cq p a _ cq. These two formulas are both Horn and Krom. Their respective set of models Modpψq tta, b, cuu and Modpµq ttau, tbu, tcu, Hu are closed under intersection and under majority. We have Modpψ F µq Modpψ W µq ttau, tbu, tcuu, which is closed neither under intersection nor under majority. So ψ F µ is neither in LHorn nor in LKrom. The refined operators Cl F and Cl W are defined as Modpψ Cl F µq Modpψ Cl W µq ttau, tbu, tcu, Hu. The refined

operators Clmaj3 F and Clmaj3 W operate similarly.

We now give an example in the affine fragment.

Example 16. Let ψ and µ be affine formulas such that Modpψq tta, b, cu, ta, duu and Modpµq ttau, tb, cu, ta, bu, tcuu. Such formulas exist since these sets of models are closed under the ternary XOR function. We have Modpψ F µq Modpψ W µq ttau, ta, bu, tb, cuu, which is not closed under the ternary XOR function. So ψ F µ is not in Laffine. The refined operators Cl 3 F and Cl 3 W for Laffine are defined as Modpψ Cl 3 F µq

Modpψ Cl 3 W µq ttau, ta, bu, tb, cu, tcuu.

Given a total order over interpretations, another β-mapping is the Minβ function that selects the minimal model in this order when the set of models is not closed.

Definition 17. Let β P B and ď be a fixed total order on the set 2U of interpretations. We define the function Minβ as

Minβp Mq " M if Clβp Mq M tminďp Mqu otherwise

Creignou, Ktari, & Papini

The Minβ function allows us to define a min-based refined belief change operator, denoted by Minβ and given by Modpψ Minβµq Minβp Modpψ µqq.

Example 18. Let ψ, µ P LHorn from Example 14. Recall that Modpψ F µq ttb, cu, ta, b, duu and Modpψ W µq ttb, cu, tc, du, ta, b, duu. Consider the following order over interpretations: tc, du ă tb, cu ă ta, b, du. We thus have Modpψ Min F µq Min p Modpψ F µqq ttb, cuu and Modpψ Min W µq Min p Modpψ W µqq ttc, duu.

The two β-mappings Clβ and Minβ represent two extreme functions, the former selecting the closure of the set of interpretations M, the latter selecting only one interpretation of M. In between these extremes there is a variety of possible β-mappings. As an example we define an intermediary function, denoted by Proxβ, which selects a closed subset of interpretations of Clβp Mq that is the closest to M. For M H, let Fp Mq be the set of nonempty subsets of Clβp Mq which are closed under β. This set is defined more formally as follows.

Fp Mq t N | H Ă N Ď Clβp Mq and N Clβp Nqu.

Let Fpp Mq be the set of elements of Fp Mq that are the closest to M (in terms of cardinality of the symmetric difference). This set is defined more formally as follows, for all M H.

Fpp Mq t N P Fp Mq | @ N 1 P Fp Mq, |M N| ď |M N 1|u

We assign to any fixed total order over interpretations a lexicographic order over subsets of interpretations, denoted by ďlex. The following example illustrates this assignment.

Example 19. Let m1, m2 and m3 be models such that m1 ď m2 ď m3. Consider the two sets of models M1 tm1, m3u and M2 tm2u. These sets are respectively represented by their characteristic vector, 101 and 010, therefore, M2 ďlex M1.

We now formally define the Proxβ function as follows.

Definition 20. Let β P B, let ď be a fixed total preorder over interpretations, ďlex its corresponding lexicographic order over subsets of interpretations and M Ď 2U a set of interpretations. The function Proxβ is defined as follows:

M if Clβp Mq M Clβp Mq if Clβp Mq M and Clβp Mq P Fpp Mq tminďlexp Fpp Mqqu otherwise

Indeed, Proxβ is a β-mapping and the refined belief change operator denoted by Proxβ is given by Modpψ Proxβµq Proxβp Modpψ µqq.

Example 21. We come back to Example 14 in the Horn fragment, where Modpψq tta, b, cu, ta, b, c, d, euu and Modpµq ttb, cu, tc, du, ta, b, du, tcu, tdu, tbu, Hu. We consider the following order over interpretations : H ă tbu ă tcu ă tdu ă tb, cu ă tc, du ă ta, b, du.

Belief Update within Propositional Fragments

H tbu tcu tdu tb, cu tc, du ta, b, du ttb, cuu 0 0 0 0 1 0 0 ttc, du 0 0 0 0 0 1 0 tta, b, duu 0 0 0 0 0 0 1 ttb, cu, tc, du, tcuu 0 0 1 0 1 1 0 ttb, cu, ta, b, du, tbuu 0 1 0 0 1 0 1 ttc, du, ta, b, du, tduu 0 0 0 1 0 1 1

Table 3: Lexicographic order on subsets of models

We remind that M Modpψ F µq ttb, cu, ta, b, duu. There are three subsets of Cl p Mq that are -closed and at distance 1 from M, and Cl p Mq is one of them. Therefore, Modpψ Proxβ F µq ttb, cu, ta, b, du, tbuu. Now let us consider M Modpψ W µq ttb, cu, tc, du, ta, b, duu. Observe that Cl p Mq ttb, cu, tc, du, ta, b, du, tbu, tcu, tdu, Hu. There is no closed subset of Cl p Mq which is at distance 1 from M, and six of them are at distance 2, therefore Fpp Mq is made of these six subsets. Since Cl p Mq R Fpp Mq we have to determine which of its element is the lexicographically minimal one. For this we focus on Table 3 where we can read the lexicographic order assigned to the different elements of Fpp Mq. Hence, Modpψ Proxβ W µq t M3u tta, b, duu. Observe that in this example the three refinements we have considered give different results, Modpψ Proxβ W µq Modpψ Clβ W µq Modpψ Minβ W µq.

4.3 Logical Properties of Refined Belief Update Operators

In this section we investigate how our refined update operators behave with respect to satisfaction of the KM postulates. We first show that our update refinements preserve the first four KM postulates.

Proposition 22. Let be an update operator and L1 Ď L a characterizable fragment. For i 1, . . . , 4, if satisfies postulate p Uiq, then so does any refinement of this operator in L1, P r , L1s.

Proof. Suppose L1 is a β-fragment. Thus we can assume that P r , L1s is an operator of the form fβ where fβ is a suitable β-mapping. Since postulates (U1) and (U4) are exactly the same postulates as (R1) and (R4), and since satisfaction of (U3) follows from satisfaction of (R3), according to Creignou et al. (2014, Prop. 6) we only have to deal with (U2). By definition Modpψ µq fβp Modpψ µqq. Since satisfies postulate (U2), if ψ |ù µ, then ψ µ ψ, i.e., Modpψ µq Modpψq. Therefore, fβp Modpψ µqq fβp Modpψqq. Since ψ P L1, fβp Modpψqq Modpψq. Thus, ψ µ ψ.

A natural question is whether there exist refined update operators that satisfy more postulates. We focus on Forbus (1989) and Winslett s operators (1988) (that satisfy respectively all KM postulates and the first eight ones) refined by Clβ, Minβ and Proxβ (other update operators as well as other refinements have been studied in Ktari, 2016). We discuss the postulates that are expressible in our fragments, namely (U5), (U6) and (U9).

Creignou, Ktari, & Papini

In the following, within a characterizable fragment, it is implicit that any β-mapping we refer to, uses the Boolean function β which characterizes the fragment. This means that within LHorn (resp. LKrom, Laffine) a β-mapping is an -mapping (resp., maj3-mapping, 3-mapping).

We first show that Proposition 22 cannot be extended to postulate (U5). Indeed we get the following negative result for (U5).

Proposition 23. Let P t F , W u. The refined update operators Clβ, Minβ and Proxβ violate postulate (U5) in any L1 P t LHorn, LKrom, Laffineu.

Proof. The proof is in the appendix.

Observation 1. Let us emphasize that this result shows a difference between revision and update. Indeed, let us recall that Forbus operator F (1989) can be considered as the update counterpart of Dalal s (1988) revision operator, D. The refinements of these two operators by the function Minβ show a different behavior. While Creignou et al. (2014) proved that Minβ D satisfies (R5), the above proposition shows that Minβ F violates (U5). Interestingly the proof that Minβ D satisfies (R5) relies on the fact that Dalal s operator D satisfies both (R5) and (R6). In the context of update (U9) is a weaker version of (R6), that applies only to complete formulas. While Forbus operator F satisfies (U9) it can be proved that it does not satisfy (R6) (see the example given in the proof of Proposition 23 for the min refinement in the Horn fragment). This explains the difference of behavior of the two operators, Dalal and Forbus, with respect to the preservation of the fifth postulate, resp. (R5) and (U5).

For the ninth postulate (U9), we obtain a rather general negative result, which is similar to the result obtained for (R6) in the context of revision (Creignou et al., 2014), but which nevertheless requires new examples to be proven, since in the case of update we need complete formulas.

Proposition 24. Let P t F , W u and L1 P t LHorn, LKrom, Laffineu. Then any refined operator P r , L1s violates postulate (U9) in L1.

Observe that in order to prove this proposition the examples proposed in Creignou et al. (2014) cannot be used since they do not involve complete formulas and we have to provide new ones.

Proof. The proof is in the appendix.

The status of the sixth postulate (U6) is less clear than the ones we have investigated so far. Indeed, the two following propositions show that the satisfaction of (U6) depends on the β-mapping that is used to define the refinement.

Proposition 25. Let be an update operator and L1 a β-fragment. If satisfies (U6), then so does the refined operator Clβ in L1.

Proof. Suppose that pψ Clβ µ1q |ù µ2 and pψ Clβ µ2q |ù µ1. Thus, Clβp Modpψ µ1qq Ď Modpµ2q and Clβp Modpψ µ2qq Ď Modpµ1q. Moreover, Modpψ µ1q Ď Clβp Modpψ µ1qq and also Modpψ µ2q Ď Clβp Modpψ µ2qq. Therefore, Modpψ µ1q Ď Modpµ2q and Modpψ µ2q Ď Modpµ1q. Since satisfies (U6), we get ψ µ1 ψ µ2. According to the equivalence property cited in Definition 8, we have finally ψ Clβ µ1 ψ Clβ µ2.

Belief Update within Propositional Fragments

Refined operators Postulates (U5) (U6) (U9) Clβ F ˆ ˆ Clβ W ˆ ˆ

Minβ F ˆ ˆ ˆ Minβ W ˆ ˆ ˆ

Proxβ F ˆ ˆLHorn ˆ Proxβ W ˆ ˆLHorn ˆ

Table 4: An overview of the satisfied postulates by the refined operators.

Proposition 26. Let P t F , W u. The refined operator Minβ violates postulate (U6) in any L1 P t LHorn, LKrom, Laffineu.

Proof. The proof is in the appendix.

The refinement by Proxβ of Forbus (1989) and Winslett s operators (1988) does not seem to behave better than the refinements by Clβ and Minβ. It is rather difficult to find counterexamples in all fragments and we obtain only a partial result in LHorn.

Proposition 27. Let P t F , W u. The refined operator Proxβ violates postulate (U6) in LHorn.

Proof. The proof is in the appendix.

Let us briefly summarize and discuss the results obtained in this section so far. Proposition 22 is positive: Given an update operator satisfying the four basic postulates (U1)-(U4), any refinement of it (in any fragment) satisfies them as well. The other results, obtained for refinements of Forbus (1989) and Winslett s operators (1988), look less promising. Nevertheless they raise interesting issues. On the one hand one might ask whether postulates (U5), (U6) and (U9) should be adapted to refinements, which correspond to a specific way of building update operators. On the other hand one has to bear in mind that Forbus operator is not the only one satisfying all postulates. Indeed representation theorems (in terms of preorders as discussed in Section 4) characterize operators satisfying all postulates. Some of these operators might lead to refinements satisfying more postulates. A classification of operators that satisfy all postulates and can be refined in such a way to preserve (U5), (U6) and (U9) in some fragment is beyond the scope of this paper and left as future work. Table 4 gives a general overview of the properties of our refined update operators in terms of satisfaction of the postulates (U5), (U6) and (U9). We put if the refined operator satisfies the considered postulate, ˆ if it violates it in all fragments, and ˆLHorn it is only known that the refined operator violates the postulate in LHorn.

Finally observe that (U7) and (U8) are not applicable in our study since they use disjunction of formulas while our fragments are not closed under disjunction (given µ1 and µ2 in L1, µ1 _ µ2 does not necessarily belong to L1). These postulates would require to

Creignou, Ktari, & Papini

be reformulated in order to fit into fragments while still characterizing rational behavior of update operators. This is an interesting issue, which is beyond the scope of this paper. An adapted formulation of these postulates would ideally be validated by a representation theorem.

Let us nevertheless discuss postulate (U8), which is the most uncontroversial postulate for belief update in the context of full propositional logic. It reflects the central fact that a rational update operator should give each model of the original beliefs equal consideration (a property that distinguishes update from revision). Unfortunately (U8) fails playing this role in fragments of propositional logic that are not closed under disjunction. Indeed, the union of closed sets of models obtained after having considered independently each model of the formula representing the belief set, has no reason to be a closed set of models. However, note that by construction our refined operators first compute the result obtained through an original operator, and then, as a post-processing step, apply a β-mapping to it. Therefore, starting from an update operator that satisfies (U8) the models of the formula will equally contribute to the update in the first step. So at least the spirit is preserved, even if of course one has to perform a post-processing in order to remain in the fragment. Observe that for the refinement by the closure Clβ, since for for all formulas ψ and µ in L1, Modpψ Clβ µq Clβp Modpψ µqq, we have TL1pψ Clβ µq TL1pψ µq. Therefore, roughly speaking Clβ is the best approximation of in L1, and if can be considered as a rational update operator, then so can Clβ in L1.

4.4 When Only the Formula Representing the Agent s Beliefs is in the Fragment

When working within fragments a very natural situation is that the formula representing the initial agent s beliefs is indeed in the fragment, while the formula reflecting new information, which potentially comes from an external source, is not. In order to iterate the process one is interested in a result that still belongs to the fragment. An interesting issue is thus to decide whether our approach allows us to refine well-established belief update operators which starting from a formula ψ in the fragment and a formula µ not necessarily in the fragment, give a result in the fragment. This is what we address in this section (for sake of completeness, the symmetric case, which is much less natural, and in which only new information is required to be in the fragment is addressed in Ktari, 2016).

Given an update operator , we call : L1 ˆ L Ñ L1 a -left-refinement (for L1) if it satisfies all properties given in Definition 8 with ψ P L1 and µ P L. It is then easy to check that the characterization given in Proposition 11 still holds, that is that any -left-refinement can be defined as fβ for some β-mapping fβ. So, we are in a position to study the logical properties of such refined operators in terms of satisfaction of postulates. On the one hand note that the negative results obtained in the initial framework a fortiori hold in this generalized case. On the other hand, the seventh postulate (U7), which did not apply in the previous section, makes sense in this context. For these reasons, we shall examine postulates (U1)-(U4), (U6) and (U7). We first give a general positive result for three of the four basic postulates.

Belief Update within Propositional Fragments

Proposition 28. Let be an update operator and L1 Ď L a β-fragment. For i 2, 3, 4, if satisfies p Uiq, then each -left-refinement for L1, : L1 ˆL Ñ L1, satisfies postulate p Uiq.

Proof. The proof is similar to the one used in Proposition 22, since ψ P L1 is not used for the preservation of (U2)-(U4).

Contrary to (U2), (U3) and (U4), the first postulate (U1) could be violated. The success postulate (U1) says that the models of the updated beliefs have to be models of new information, i.e., ψ µ |ù µ. In the case of a refined operator fβ, since Modpψ fβ µq fβp Modpµqq, the problem is that the application of fβ can generate new models that are not necessarily models of µ, and thus the postulate (U1) is not necessarily preserved. We show that this is indeed the case, and actually we prove that the preservation of (U1) depends on the β-mapping that is used for the refinement.

Proposition 29. Let P t F , W u be an update operator and L1 Ď L a β-fragment. The -left-refinement Clβ violates postulate (U1) in any L1 P t LHorn, LKrom, Laffineu.

Proof. Let P t F , W u. Consider ψ P L1 such that Modpψq t Hu. This set is closed under , maj3 and 3. Let µ P L such that Modpµq ttau, tbu, tcuu, we get Modpψ µq ttau, tbu, tcuu. Thus, Modpψ Clβ µq ttau, tbu, tcu, Hu. Observe that Modpψ Clβ µq Ę Modpµq, hence Clβ violates (U1).

However, some β-mappings behave better, in particular the β-mappings f we call contracting, which are characterized by the property fp Mq Ď M for any set of interpretations M. Observe that Minβ is such a contracting mapping.

Proposition 30. Let be an update operator and L1 Ď L be a β-fragment. If satisfies (U1) and if fβ is a contracting β-mapping, then the -left-refinement, fβ : L1 ˆ L Ñ L1, satisfies postulate (U1).

Proof. Since satisfies (U1), we have ψ µ |ù µ. Thus, Modpψ µq Ď Modpµq. Besides, fβ is contracting, thus fβp Modpψ µqq Ď Modpψ µq Ď Modpµq. Therefore, Modpψ fβ µq Ď Modpµq, i.e., ψ fβ µ |ù µ. Hence fβ satisfies (U1).

So interestingly contracting β-mappings allow us to refine rational update operators in order to obtain update operators defined from L1 ˆ L to L1 that satisfy the four basic postulates. Observe that this is in sharp contrast with belief revision. No refinement of a rational revision operator provides a revision operator defined from L1 ˆ L to L1 that satisfies the first four basic postulates. Indeed, the second postulate for revision (R2) (if pψ µq is satisfiable then ψ µ ψ µ) is not compatible with an operator from L1 ˆ L to L1. For instance let us consider ψ J and µ a satisfiable formula which is not equivalent to any formula in L1. The formula ψ µ is satisfiable since ψ µ µ, whereas ψ µ ı ψ µ by assumption on the choice of µ.

Another way to deal with (U1) is to consider a weaker version of this postulate that would be more appropriate to fragments in this particular case, where new information does not necessarily belong to the fragment. In full propositional logic (U1) means that TLpµq Ď TLpψ µq. In a fragment L1 it would be reasonable to require only that TL1pµq Ď TL1pψ µq.

Creignou, Ktari, & Papini

Since for any β-fragment L1 and any formula µ, TL1pµq TL1p µq where µ P L1 is such that Modp µq Clβp Modpµqq, we propose the following weaker version of (U1):

Let L1 be a β-fragment, ψ P L1, and µ P L. ( U1) ψ µ |ù µ, where µ P L1 is such that Modp µq Clβp Modpµqq.

Interestingly, with this more adequate formulation the success postulate is preserved by left-refinements.

Proposition 31. Let be an update operator and L1 Ď L a β-fragment. If satisfies p U1q, then each -left-refinement for L1, : L1 ˆ L Ñ L1, satisfies postulate p U1q.

Proof. Since satisfies (U1), we have ψ µ |ù µ. Thus, Modpψ µq Ď Modpµq. According to Definition 9, for any β-mapping fβ we have fβp Modpψ µqq Ď Clβp Modpψ µqq, and since Clβ is monotone Clβp Modpψ µqq Ď Clβp Modpµqq, thus proving that ( U1) holds.

The status of postulate (U6) seems to be unchanged in this generalized framework compared to the original one.

Proposition 32. Let be an update operator and L1 Ď L be a β-fragment. If satisfies (U6), then the -left-refinement, Clβ: L1 ˆ L Ñ L1, satisfies postulate (U6).

Proof. The proof is similar to the one used in Proposition 25, since µ P L1 is not used.

In the previous section, the seventh postulate (U7) was not applicable since the considered fragments are not closed under disjunction, however for -left-refinements, there is no constraint on new information µ anymore and this postulate makes sense. We get a negative result for this postulate.

Proposition 33. Let P t F , W u. The -left-refinement Minβ violates postulate (U7) in LHorn.

Proof. Let ψ be a formula in LHorn such that Modpψq ttb, c, duu and let µ1 and µ2 be two formulas in L such that Modpµ1q tta, b, cu, tcuu and Modpµ2q tta, b, cu, tduu. Observe that Modpµ1q Y Modpµ2q is not closed under and thus µ1 _ µ2 is not equivalent to any formula in LHorn. Consider the following order: tcu ă ta, b, cu ă tdu. We get Modpψ µ1q tta, b, cu, tcuu, which is closed under , thus Modpψ Min µ1q tta, b, cu, tcuu. Moreover we have Modpψ µ2q tta, b, cu, tduu which is not closed under , this leads to Modpψ Min µ2q tta, b, cuu. Therefore Modpψ Min µ1q X Modpψ Min µ2q tta, b, cuu. Besides, we get Modpψ pµ1 _ µ2qq tta, b, cu, tcu, tduu, which is not closed under thus Modpψ Min pµ1_µ2qq ttcuu. Consequently we have Modpψ Min µ1q XModpψ Min µ2q Ę Modpψ Min pµ1 _ µ2qq. Hence, Minβ violates (U7) in LHorn.

To conclude this section let us recall that Herzig s update operators HZ (Herzig & Rifi, 1999), and in particular Hegner s (1987) operator H, are well-suited for update in any characterizable fragment when both the formula representing the agent s beliefs and the formula reflecting new information are in the fragment (see Proposition12). However, this is not the case anymore when new information is not required to be in the fragment, as illustrated in the following example.

Belief Update within Propositional Fragments

Example 34. Let two formulas ψ and µ such that ψ a b c and µ a _ b. We have Modpψq ttcuu, Modpµq ttau, tbu, ta, bu, ta, cu, tb, cu, ta, b, cuu and Varpµq ta, bu. Clearly, ψ is in LHorn but µ is not equivalent to any Horn formula. Assume deppµq ta, bu, we get Modpψ HZ µq tta, cu, tb, cu, ta, b, cuu, which is not closed under intersection. Therefore, within this more general framework ( -left-refinement), Herzig s update operators HZ (Herzig & Rifi, 1999), and in particular Hegner s (1987) operator H, would deserve to be refined.

5. Conclusion

We have investigated to which extent well-established model-based belief change operators can be refined to work within propositional fragments. We have first defined desired properties any refined belief change operator should satisfy and provided a characterization of all such refined operators. Then, we focused on the belief update operation, which has been neglected so far. We showed that any refinement of an update operator preserves the basic KM update postulates p U1q p U4q (Katsuno & Mendelzon, 1992) for any fragment. We then focused on Forbus (1989) and Winslett s update operators (1988) within Horn, Krom and affine fragments. We showed that all the proposed refinements violate the fifth postulate p U5q. This result is very interesting since it highlights a difference between revision and update. An interesting issue is whether this postulate is indeed violated by any refined update operator. Regarding the sixth postulate p U6q the situation is less clear since the refinement by the closure preserves this postulate, while the other studied refinements do not. It would be interesting to characterize the refined operators that preserve it. We also showed that none of the refinements of Forbus (1989) and Winslett s operators (1988) satisfies the ninth postulate p U9q. We also studied a natural extension, when only the formula representing the agent s beliefs is in the fragment, and not necessarily new information, that is operators from L1ˆL to L1. Our approach can handle this extension. Using β-mappings that are contracting allows us to define refined update operators, which contrary to revision satisfy the first four basic postulates. There are several interesting issues for future work. The first one concerns the postulates. The KM postulates (Katsuno & Mendelzon, 1992) that are meaningful in propositional fragment, namely p U5q, p U6q and p U9q, are not all satisfied by refined operators. An interesting issue is how to weaken them in such a way that some refinements, notably the closure-based refinement, satisfy them. Other KM postulates are not expressible in fragments, namely p U7q and p U8q. For them, an additional difficulty is to modify them so that they are expressible in fragments, regardless of refinement operators. A challenging task would be to find an appropriate formulation of these postulates that leads to a representation theorem for update in fragments, as it was already done for revision (Delgrande & Peppas, 2015) and merging (Haret, R ummele, & Woltran, 2017) within the Horn fragment. Besides, we plan to continue our study in exploring other belief change operations, such as belief erasure and belief forget, which are defined by means of update operators. Finally, an ambitious issue is the study of the computational complexity of the refined update operators.

Creignou, Ktari, & Papini

Acknowledgments

This work received support from the french Agence Nationale de la Recherche, ASPIQ project reference ANR-12-BS02-0003. The authors thank the anonymous referees of JAIR for their comments, which helped to improve this article.

Appendix A.

Proposition 35. Let P t F , W u. The refined update operators Clβ, Minβ and Proxβ violate postulate (U5) in any L1 P t LHorn, LKrom, Laffineu.

Proof. We give first the proof for the refinement by Clβ. For LHorn and LKrom, consider ψ, µ, φ in LHorn (resp. LKrom) such that Modpψq tta, b, cuu, Modpµq ttau, tbu, tcu, Hu and Modpφq ttcu, Hu. Such formulas exists since these sets of models are closed under and maj3. For P t F , W u, we have Modpψ µq ttau, tbu, tcuu which is not closed under nor under maj3. We get Modpψ Clβ µq ttau, tbu, tcu, Huu and Modppψ Clβ µq φq ttcu, Huu. Besides, Modpψ Clβ pµ φqq ttcuu, therefore Modppψ Clβ µq φq |ù Modpψ Clβ pµ φqq. Hence, Clβ violates (U5) in LHorn and LKrom. For L1 Laffine, consider ψ, µ, φ in Laffine such that Modpψq ttau, ta, b, cuu, Modpµq t H, ta, bu, ta, cu, ta, du, ta, eu, tb, cu, tb, du, tb, eu, tc, du, tc, eu, td, eu, ta, b, c, du, ta, b, c, eu, ta, b, d, eu, ta, c, d, eu, tb, c, d, euu and Modpφq ttd, eu, Hu. Note that ψ, φ P Laffine since the corresponding sets of models are closed under 3 and the set of models of µ is the set of solutions of the equation a b c d e 0. We have Modpψ µq t H, ta, bu, ta, cu, ta, du, ta, eu, tb, cu, ta, b, c, du, ta, b, c, euu. The closure of this set under 3 is exactly Modpµq. Hence, Modpψ Clβ µq Modpµq. We now use φ P Laffine with Modpφq ttd, eu, Hu. We obtain Modppψ Clβ µq φq t H, td, euu. But, Modpψ Clβ pµ φqq t Hu. Thus, pψ Clβ µq φ |ù ψ Clβ pµ φq, hence Clβ F and Clβ W violate postulate (U5) in Laffine. Let us now turn to the refinement by Minβ. We give first the proof for LHorn and LKrom. Let P t F , W u. Let ψ, µ and φ in LHorn (resp. LKromq such that Modpψq tta, b, c, d, e, fu, tb, c, d, e, fuu, Modpµq t H, tcu, ta, bu, tc, du, te, fu, ta, b, cuu and Modpφq tta, bu, tc, du, te, fu, Hu. Observe that since these sets of models are closed under (resp. under maj3) such formulas exist. Consider the following order ta, bu ă tc, du ă te, fu ă ta, b, cu. On the one hand we obtain Modpψ µq ttc, du, te, fu, ta, b, cuu, and thus Modpψ Minβ µq ttc, duu. Therefore, Modppψ Minβ µq φq ttc, duu. On the other hand, Modpψ pµ φqq tta, bu, tc, du, te, fuu, thus Modpψ Minβ pµ φqq tta, buu. It is then clear pψ Minβ µq φ |ù ψ Minβ pµ φq, hence Minβ F and Minβ W violate postulate (U5) in LHorn and LKrom. For L1 Laffine, we can consider the formulas ψ, µ in Laffine with the same set of models as in the case of the refinement by Clβ and let φ P Laffine such that Modpφq ttb, cu, tb, du, tb, eu, tb, c, d, euu. Note that φ P Laffine exists since the corresponding set of models is closed under 3. Let us suppose that tb, du and tb, cu are the two smallest interpretations with respect to ď with tb, du ă tb, cu. We have on the one hand Modpψ µq t H, ta, bu, ta, cu, ta, du, ta, eu, tb, cu, ta, b, c, du, ta, b, c, euu which is not closed under 3 and so Modpψ Minβ µq ttb, cuu. Hence, Modppψ Minβ µq φq ttb, cuu. On the other hand, we have Modpψ pµ φqq ttb, cu, tb, du, tb, euu, which is not closed under 3, and thus

Belief Update within Propositional Fragments

Modpψ Minβ pµ φqq ttb, duu. It is obvious that pψ Minβ µq φ |ù ψ Minβ pµ φq. Therefore, Minβ F and Minβ W violate postulate (U5) in Laffine. We now consider the refinement by Proxβ. We give first the proof for LHorn and LKrom. Let ψ, µ and φ in LHorn (resp. LKrom) such that Modpψq tta, b, cuu, Modpµq ttau, tbu, tcu, Hu and Modpφq ttcu, Hu. For P t F , W u, we have Modpψ µq ttau, tbu, tcuu, which is not closed under (resp. maj3). Since Fpp Modpψ µqq consists in a single set ttau, tbu, tcu, Hu, which is equal to Clβp Modpψ µqq, we have Modpψ Proxβ µq ttau, tbu, tcu, Hu and Modppψ Proxβ µq φq ttcu, Hu. On the other hand, Modpψ pµ φqq ttcuu, which is closed under (resp. maj3). Therefore Modpψ Proxβ pµ φqq ttcuu. It is then clear pψ Proxβ µq φ |ù ψ Proxβ pµ φq, thus proving that Proxβ F and Proxβ W violate postulate (U5) in LHorn and LKrom. For L1 Laffine consider ψ, µ and φ in Laffine such that Modpψq tta, b, cuu, Modpµq t H, ta, bu, tc, du, tc, eu, td, eu, ta, b, c, du, ta, b, c, eu, ta, b, d, euu and Modpφq ttc, du, tc, eu, ta, bu, ta, b, d, euu. Note that such formulas exists in Laffine since the corresponding sets of models are closed under 3. For P t F , W u, we have Modpψ µq tta, bu, ta, b, c, du, ta, b, c, euu which is not closed under 3. On the one hand Modpψ Prox

µq Clβptta, bu, ta, b, c, du, ta, b, c, euuq tta, bu, ta, b, c, du, ta, b, c, eu, ta, b, d, euu, because Clβp Modpψ µqq is at distance 1 from Modpψ µq and hence in Fpp Modpψ µqq. Therefore Modppψ Prox µq φq tta, bu, ta, b, d, euu. On the other hand we have Modpψ pµ φqq tta, buu. This set of models is closed under 3. Thus, Modpψ Prox pµ φqq tta, buu. Therefore, pψ Prox µq φ |ù ψ Prox pµ φq. Hence, Proxβ F and Proxβ W violate postulate (U5) in Laffine.

Proposition 36. Let P t F , W u and L1 P t LHorn, LKrom, Laffineu. Then any refined operator P r , L1s violates postulate (U9) in L1.

Proof. First, let us treat the case L1 LHorn. Consider f where f is a -mapping. Let ψ and µ in LHorn such Modpψq tta, b, c, duu and Modpµq tta, bu, ta, cu, tau, ta, b, eu, ta, b, c, euu. We obtain M Modpψ µq tta, bu, ta, cu, ta, b, c, euu. Consider the possibilities for Modpψ µq fp Mq. Recall that fp Mq Ď Cl p Mq tta, bu, ta, cu, ta, b, c, eu, tauu. We consider two cases: First assume that tau P fp Mq. Let φ be such that Modpφq ttau, ta, b, euu N. Clearly, such a φ exists in LHorn. Also note that Modpφq Ď Modpµq. We get Modpψ pµ φqq Modpψ φq fp Modpψ φqq fpttau, ta, b, euuq N (N is closed under , fp Nq N holds by definition of refined operators), but Modppψ µq φq fp Mq XModpφq ttauu. Otherwise tau R fp Mq. Since fp Mq H and fp Mq is closed under , by symmetry of the role played by the variables b and c, it is sufficient to examine three possibilities for fp Mq: either fp Mq tta, buu or fp Mq tta, b, c, euu or fp Mq tta, bu, ta, b, c, euu.

If fp Mq tta, buu or fp Mq tta, b, c, euu, let us consider the formula φ such that Modpφq tta, bu, ta, b, c, euu. Clearly, such a φ exists in LHorn. We obtain Modpψ pµ φqq tta, bu, ta, b, c, euu, whereas Modppψ µq φq fp Mq XModpφq fp Mq.

Creignou, Ktari, & Papini

If fp Mq tta, bu, tta, b, c, euu. Consider φ in LHorn such that Modpφq tta, cu, ta, b, c, euu. Observe that Modpψ pµ φqq tta, cu, ta, b, c, euu, but Modppψ µq φq fp Mq X Modpφq tta, b, c, euu.

Therefore, in any case Modppψ µq φq H and Modpψ pµ φqq Ę Modppψ µq φq, thus proving that pψ µq φ is satisfiable, whereas ψ pµ φq |ù pψ µq φ in LHorn. For L1 LKrom, the formulas ψ, µ P LKrom with Modpψq tta, b, c, d, euu, Modpµq tta, b, cu, tb, c, du, tb, c, eu, tb, cu, ta, buu can be employed. For P t F , W u, we have M Modpψ µq tta, b, cu, tb, c, du, tb, c, euu. Observe that Clmaj3p Mq tta, b, cu, tb, c, du, tb, c, eu, tb, cuu. Let us consider the possibilities for Modpψ µq fp Mq. By definition of refined operators, we know that ta, bu R fp Mq since ta, bu R Clmaj3p Mq. We consider two cases: First assume tb, cu P fp Mq: Let φ be such that Modpφq ttb, cu, ta, buu N. Clearly such a φ exists in LKrom. Besides note that Modpφq Ď Modpµq. We get Modpψ pµ φqq Modpψ φq fp Modpψ φqq ttb, cu, ta, buu N, whereas Modppψ µq φq ttb, cuu. Otherwise, we have tb, cu R fp Mq. Since fp Mq H and fp Mq is already closed under maj3, by symmetry of the role played by the variables a, d and e, it is sufficient to consider two cases for fp Mq : either fp Mq tta, b, cu, tb, c, duu or fp Mq tta, b, cuu.

If fp Mq tta, b, cu, tb, c, duu, let us consider the formula φ such that Modpφq tta, b, cu, tb, c, euu. Clearly, such a φ exists in LKrom. We obtain thus Modpψ pµ φqq tta, b, cu, tb, c, euu. Nevertheles, Modppψ µq φq fp Mq XModpφq tta, b, cuu.

If fp Mq tta, b, cuu. We select φ in LKrom with Modpφq tta, b, cu, tb, c, duu. Then, Modpψ pµ φqq tta, b, cu, tb, c, duu, whereas Modppψ µq φq fp Mq XModpφq fp Mq tta, b, cuu.

It is then clear that in any case Modppψ µq φq H and Modpψ pµ φqq Ę Modppψ µq φq, thus showing eventually that pψ µq φ is satisfiable, whereas ψ pµ φq |ù pψ µq φ in LKrom. For L1 Laffine, we use formulas ψ, µ P Laffine with Modpψq tta, b, cuu and Modpµq t H, ta, bu, tc, du, tc, eu, td, eu, ta, b, c, du, ta, b, c, eu, ta, b, d, euu. Observe that the set of models of µ is the set of solutions of the following equations system: (a b 0, c d e 0). We have M Modpψ µq tta, bu, ta, b, c, du, ta, b, c, euu. For P t F , W u, we have Cl 3p Mq Modpψ Cl 3 µq tta, bu, ta, b, c, du, ta, b, c, eu, ta, b, d, euu. Let us consider the possibilities for Modpψ µq fp Mq. We distiguish two cases. First, assume ta, b, d, eu P fp Mq: let φ be such that Modpφq tta, b, d, eu, ta, buu. Clearly, such a φ exists in Laffine. Also note that Modpφq Ď Modpµq. We obtain on the one hand Modpψ pµ φqq Modpψ φq fp Modpψ φqq tta, buu and on the other hand Modppψ µq φq contains tta, b, d, euu. Otherwise, we have ta, b, d, eu R fp Mq. Since

fp Mq H and fp Mq is closed under 3, by symmetry of the role played by the variables d and e, it is sufficient to distinguish four cases for fp Mq: either fp Mq tta, buu or fp Mq tta, b, c, euu or fp Mq tta, bu, ta, b, c, euu or fp Mq tta, b, c, du, ta, b, c, euu:

If fp Mq tta, buu or fp Mq tta, b, c, euu, we consider the formula φ such that Modpφq tta, bu, ta, b, c, euu. Clearly, such a φ exists in Laffine. We obtain Modpψ pµ φqq tta, bu, ta, b, c, euu, whereas Modppψ µq φq fp Mq X Modpφq fp Mq.

Belief Update within Propositional Fragments

If fp Mq tta, bu, ta, b, c, euu. In this case, let consider φ in Laffine such that Modpφq tta, bu, ta, b, c, duuu. Observe that while Modpψ pµ φqq tta, bu, ta, b, c, duu, Modppψ µq φq fp Mq X Modpφq tta, buu.

If fp Mq tta, b, c, du, ta, b, c, euu, we use φ P Laffine with Modpφq tta, bu, ta, b, c, duu. While Modpψ pµ φqq tta, bu, ta, b, c, duu, we get Modppψ µq φq fp Mq X Modpφq tta, b, c, duu.

Obviously, Modppψ µq φq H and Modpψ pµ φqq Ę Modppψ µq φq in all cases, thus proving that pψ µq φ is satisfiable, whereass ψ pµ φq |ù pψ µq φ in Laffine.

Proposition 37. Let P t F , W u. The refined operator Minβ violates postulate (U6) in any L1 P t LHorn, LKrom, Laffineu.

Proof. Let P t F , W u. We give first the proof for LHorn. Let ψ, µ1, µ2 P LHorn with Modpψq ttbu, ta, b, c, duu, Modpµ1q ttau, ta, bu, ta, cu, ta, b, c, euu and Modpµ2q tta, bu, ta, b, c, euu. Suppose that ta, bu ă ta, cu ă ta, b, c, eu. On the one hand, we have Modpψ µ1q tta, bu, ta, cu, ta, b, c, euu which is not closed under . Thus, Modpψ Min µ1q Min ptta, bu, ta, cu, ta, b, c, euuq tta, buu Ď Modpµ2q. On the other hand, we have Modpψ µ2q tta, bu, ta, b, c, euu, a set of models closed under . Therefore, Modpψ Min µ2q tta, bu, ta, b, c, euu Ď Modpµ1q. But, ψ Min µ1 ı ψ Min µ2, hence Minβ violates (U6) in LHorn. For L1 LKrom, we use ψ, µ1, µ2 P LKrom with Modpψq tta, b, cu, ta, buu, Modpµ1q ttau, tbu, tcu, Hu and Modpµ2q ttau, tcuu and we suppose that tau ă tbu ă tcu. We have on the one hand Modpψ µ1q ttau, tbu, tcuu, this set is not closed maj3. Consequently, Modpψ Minmaj3 µ1q Minmaj3pttau, tbu, tcuuq ttauu Ď Modpµ2q. On the other hand, Modpψ µ2q ttau, tcuu is closed under maj3. Hence, Modpψ Minmaj3 µ2q ttau, tcuu Ď Modpµ1q. Let us notice that Modpψ Minmaj3 µ1q Modpψ Minmaj3 µ2q, hence Minβ violates (U6) in LKrom. Finally, for L1 Laffine, the formulas ψ, µ1 and µ2 P Laffine with Modpψq tta, b, c, d, eu, ta, b, cuu, Modpµ1q t H, ta, bu, tc, du, te, fu, ta, b, c, du, ta, b, e, fu, tc, d, e, fu, ta, b, c, d, e, fuu and Modpµ2q tta, bu, tc, du, ta, b, e, fu, tc, d, e, fuu can be used to show the assertion. Indeed, the set of models of µ is the set of solutions of the following equation system: (a b 0, c d 0, e f 0). Let us suppose that ta, bu is the smallest interpretation with respect to ď. On the one hand, we have Modpψ µ1q tta, bu, ta, b, c, du, ta, b, c, d, e, fuu, a set not closed under 3. We obtain thus Modpψ min 3 µ1q tta, buu Ď Modpµ2q. On the other hand, Modpψ µ2q tta, bu, tc, du, ta, b, e, fu, tc, d, e, fuu which is already closed under 3. Therefore, Modpψ min 3 µ2q tta, bu, tc, du, ta, b, e, fu, tc, d, e, fuu. Hence, Modpψ min 3 µ2q Ď Modpµ1q. Nevertheless, Modpψ min 3 µ1q Modpψ min 3 µ2q, hence Minβ violates (U6) in Laffine.

Proposition 38. Let P t F , W u. The refined operator Proxβ violates postulate (U6) in LHorn.

Creignou, Ktari, & Papini

Proof. Consider ψ and µ1 two formulas in LHorn such that Modpψq tta, b, c, duu and Modpµ1q tta, bu, ta, cu, tau, ta, b, eu, ta, b, c, euu. Note that these sets of models are closed under . We get Modpψ µ1q tta, bu, ta, cu, ta, b, c, euu, which is not closed by intersection. Observe that Clβp Modpψ µ1qq is at distance 1 from Modpψ µ1q, and hence Cl p Modpψ µ1qq P Fpp Modpψ µ1qq. Thus, Modpψ Prox

µ1q Cl ptta, bu, ta, cu, ta, b, c, euuq tta, bu, ta, cu, ta, b, c, eu, tauu. Let µ2 be a formula in LHorn such that Modpµ2q tta, bu, ta, cu, ta, b, c, eu, tau, tb, cu, tbu, tcu, Hu, we observe that Modpψ Prox µ1q Ď Modpµ2q. Besides, Modpψ µ2q tta, bu, ta, cu, ta, b, c, eu, tb, cuu is not closed by intersection. We have Fpp Modpψ µ2qq ttta, bu, ta, b, c, euu, tta, bu, ta, cu, ta, b, c, eu, tauu, tta, bu, tb, cu, ta, b, c, eu, tbuu, tta, cu, t b, cu, ta, b, c, eu, tcuuu, it does not contain Clβp Modpψ µ2qq. Consider the following order on models of µ2:

ta, bu ă ta, b, c, eu ă tau ă ta, cu ă tb, cu ă tbu ă tcu.

It induces the following lexicographical order on the sets of models of Fpp Modpψ µ2qq: tta, bu, ta, b, c, euu ă tta, bu, ta, b, c, eu, tau, ta, cuu ă tta, bu, ta, b, c, eu, tb, cu, tbuu ă tta, b, c, eu, ta, cuu ă tta, cu, tb, cu, ta, b, c, eu, tcuu. Thus, Modpψ Prox µ2q tta, bu, ta, b, c, euu Ď Modpµ1q. We observe that Modpψ Prox µ1q Modpψ Prox µ2q, thus proving that Proxβ violates (U6) in LHorn.

Alchourr on, C., G ardenfors, P., & Makinson, D. (1985). On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic, 50, 510 530.

Booth, R., Meyer, T., Varzinczak, I., & Wassermann, R. (2011). On the link between partial meet, kernel, and infra contraction and its application to Horn logic. Journal of Artificial Intelligence Research, 42, 31 53.

Boutilier, C. (1998). A unified model of qualitative belief change: A dynamical systems perspective. Artificial Intelligence, 98(1-2), 281 316.

Cadoli, M., & Scarcello, F. (2000). Semantical and computational aspects of Horn approximations. Artificial Intelligence, 119(1-2), 1 17.

Creignou, N., Papini, O., Pichler, R., & Woltran, S. (2014). Belief revision within fragments of propositional logic. Journal of Computer and System Sciences, 80(2), 427 449. A preliminary version appeared in Proc. of KR 2012.

Creignou, N., Papini, O., R ummele, S., & Woltran, S. (2016). Belief merging within fragments of propositional logic. ACM Transactions on Computational Logic, 17(3), 20. A preliminary version appeared in Proc. of ECAI 2014.

Creignou, N., Pichler, R., & Woltran, S. (2017). Do hard SAT-related reasoning tasks become easier in the Krom fragment?. Co RR, abs/1711.07786.

Belief Update within Propositional Fragments

Creignou, N., & Vollmer, H. (2008). Boolean constraint satisfaction problems: When does Post s lattice help?. In Complexity of Constraints - An Overview of Current Research Themes [Result of a Dagstuhl Seminar], Vol. 5250 of Lecture Notes in Computer Science, pp. 3 37. Springer.

Dalal, M. (1988). Investigations into theory of knowledge base revision. In Proc. AAAI, pp. 449 479.

del Val, A., & Shoham, Y. (1994). A unified view of belief revision and update. Journal of Logic and Computation, 4(5), 797 810.

Delgrande, J., Jin, Y., & Pelletier, F. (2014). Compositional belief update. Journal of Artificial Intelligence Research, 32, 757 791.

Delgrande, J., & Peppas, P. (2015). Belief revision in Horn theories. Artificial Intelligence, 218, 1 22.

Delgrande, J., & Wassermann, R. (2013). Horn clause contraction functions. Journal of Artificial Intelligence Research, 48, 457 511.

Doherty, P., Lukaszewicz, W., & Madalinska-Bugaj, E. (2000). The PMA and relativizing minimal change for action update. Fundamenta Informaticae, 44(1-2), 95 131.

Dubois, D., & Prade, H. (1993). Belief revision and updates in numerical formalisms: An overview, with new results for the possibilistic framework. In Proc. IJCAI, pp. 620 625.

Eiter, T., & Gottlob, G. (1992). On the complexity of propositional knowledge base revision, updates, and counterfactuals. Artificial Intelligence, 57(2-3), 227 270.

Fagin, R., Ullman, J., & Vardi, M. (1983). On the semantic of updates in databases. In Proc. ACM SIGACT SIGMOD, pp. 352 365.

Forbus, K. (1989). Introducing actions into qualitative simulation. In Proc. IJCAI, pp. 1273 1278.

Friedman, N., & Halpern, J. (1999). Modeling belief in dynamic systems, part II: Revision and update. Journal of Artificial Intelligence Research, 10, 117 167.

Haret, A., R ummele, S., & Woltran, S. (2017). Merging in the Horn fragment. ACM Transactions on Computational Logic, 18(1), 6:1 6:32.

Hegner, S. (1987). Specification and implementation of programs for updating incomplete information databases. In Proc. ACM SIGACT-SIGMOD-SIGART, pp. 146 158.

Herzig, A., & Rifi, O. (1999). Propositional belief base update and minimal change. Artificial Intelligence, 115(1), 107 138.

Horn, A. (1951). On sentences which are true of direct unions of algebras. Journal of Symbolic Logic, 16, 14 21.

Katsuno, H., & Mendelzon, A. (1991). Propositional knowledge base revision and minimal change. Artificial Intelligence, 52(3), 263 294.

Katsuno, H., & Mendelzon, A. (1992). On the difference between updating a knowledge base and revising it. In G ardenfors, P. (Ed.), Belief revision, pp. 183 203. Cambridge University Press.

Creignou, Ktari, & Papini

Keller, A., & Winslett, M. (1985). On the use of an extended relational model to handle changing incomplete information. IEEE Transactions of Software Engineering, 11(7), 620 633.

Ktari, R. (2016). Changement de croyances dans des fragments de la logique propositionnelle. Ph.D. thesis, Aix-Marseille Universit e.

Lang, J. (2007). Belief update revisited. In Proc. IJCAI, pp. 2517 2522.

Liberatore, P., & Schaerf, M. (2001). Belief revision and update: Complexity of model checking. Journal of Computer and System Sciences, 62(1), 43 72.

Post, E. L. (1941). The two-valued iterative systems of mathematical logic. Annals of Mathematical Studies, 5, 1 122.

Putte, F. V. D. (2013). Prime implicates and relevant belief revision. Journal of Logic and Computation, 23(1), 109 119.

Satoh, K. (1988). Nonmonotonic reasoning by minimal belief revision. In Proc. FGCS, pp. 455 462, Tokyo.

Schaefer, T. J. (1978). The complexity of satisfiability problems. In Proc. STOC, pp. 216 226. ACM Press.

Winslett, M. (1988). Reasoning about action using a possible models approach. In Proc. AAAI, pp. 89 93.

Zhang, Y., & Foo, N. (2000). Updates with disjunctive information: From syntactical and semantical perspectives. Computational Intelligence, 16(1), 29 52.

Zhuang, Z., & Pagnucco, M. (2014). Entrenchment-based Horn contraction. Journal of Artificial Intelligence Research, 51, 227 254.

Zhuang, Z., Pagnucco, M., & Zhang, Y. (2013). Definability of Horn revision from Horn contraction. In Proc. IJCAI, pp. 1205 1212.