Andreas Herzig

Jerome Lang

Propositional Update Operators Based on Formula/Literal Dependence

Keywords: Algorithms, Languages, Theory Knowledge representation, update, computational complexity

We present and study a general family of belief update operators in a propositional setting. Its operators are based on formula/literal dependence, which is more fine-grained than the notion of formula/variable dependence that was proposed in the literature: formula/variable dependence is a particular case of formula/literal dependence. Our update operators are defined according to the "forget-then-conjoin" scheme: updating a belief base by an input formula consists in first forgetting in the base every literal on which the input formula has a negative influence, and then conjoining the resulting base with the input formula. The operators of our family differ by the underlying notion of formula/literal dependence, which may be defined syntactically or semantically, and which may or may not exploit further information like known persistent literals and pre-set dependencies. We argue that this allows to handle the frame problem and the ramification problem in a more appropriate way. We evaluate the update operators of our family w.r.t. two important dimensions: the logical dimension, by checking the status of the Katsuno-Mendelzon postulates for update, and the computational dimension, by identifying the complexity of a number of decision problems (including model checking, consistency and inference), both in the general case and in some restricted cases, as well as by studying compactability issues. It follows that several operators of our family are interesting alternatives to previous belief update operators.

INTRODUCTION

Belief update mainly focuses on determining how a belief state (typically represented by a belief base) should evolve in order to take into account a new piece of information reflecting an explicit evolution of the world, typically the effect of an agent's action, or an event the occurrence of which the agent is aware of. In other words, updating by some piece of information µ roughly corresponds to projecting the consequences of the action "make µ true."

Many belief update operators in a propositional setting have been proposed in the literature. In this setting, a belief base is a propositional formula (or a finite set of such formulas that is interpreted conjunctively). The first works were mostly based on principles of minimization of change. While this principle is attractive for many belief change operators, including belief revision1 , using it to define update operators has been criticized in many places (see e.g., [START_REF] Herzig | Propositional belief update and minimal change[END_REF]), and it is now more or less a common belief that an explicit minimization of change should not be the core principle for belief update. A more suitable principle for building update operators is the notion of dependence. The first dependence-based update operators were proposed by [START_REF] Winslett | Updating Logical Databases[END_REF], [START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Doherty | The PMA and relativizing change for action update[END_REF], [START_REF] Herzig | The PMA revisited[END_REF], [START_REF] Herzig | The PMA revisited[END_REF]Rifi [1998, 1999]. In a nutshell, a belief base is updated by first forgetting every piece of belief whose variables depend on those of the input formula, and then conjoining ("expanding") the resulting base with the input formula itself. For example take the propositional belief base a ∧ b and the input formula ¬a. If we consider that the propositional variable a depends on a and b does not, then forgetting a from a ∧ b results in b, and expanding the latter with ¬a results in ¬a ∧ b. Another example is the belief base a ∧ b and the input formula a ∨ b. If the propositional variable a depends on a and b depends on b then forgetting a ∨ b from a ∧ b results in the empty belief base ⊤, and expanding the latter with a ∨ b results in a ∨ b. Depending on the notion of dependence under consideration, many operators following such a "forget-then-conjoin" scheme can be defined.

However, some severe problems with these dependence-based operators were pointed out by [START_REF] Herzig | Updates, actions, and planning[END_REF]. They stem from the fact that dependence is not directed: as we shall explain below, in many cases this makes us forget too much. In this article we show how dependence-based update operators can be generalized to take into account the truth value of fluents (here, the propositional variables) on which the update formula depends (and not only the variables themselves). This leads to a better handling of the frame problem and is specifically important when persistent literals are considered: literals that remain true once they become true. The idea is that in order to update by µ one should forget the negations of all those literals µ depends on. Let us take up the second above example where forgetting the variables a and b in a∧b resulted in the trivial belief base ⊤. It is natural to consider that a (positively) depends on the truth of a, but that ¬a does not (positively) depend on the truth of a. Therefore in order to update by a ∨ b we should forget ¬a and ¬b from a ∧ b. As both a and b "survive" the forgetting of ¬a and of ¬b, updating a ∧ b by a ∨ b should result in a ∧ b.

In order to overcome these problems we introduce a family of update operators that is based on formula/literal dependence. We explore several possible definitions of dependence functions: they may be defined syntactically or semantically, and they may exploit further information such as knowledge about persistent literals and pre-set dependencies. Different notions of formula/literal dependence will lead to different update operators. We show that these belief update operators allow to grasp the effects of actions in a way better than the previous dependence-based operators, while avoiding a complexity shift. We also evaluate the operators with respect to their logical and computational properties: as to the former, we check the status of the Katsuno-Mendelzon (KM) postulates for update; as to the latter, we identify the complexity of a number of decision problems (including model checking, consistency, and inference), as well as compactability issues. We identify some operators from the family that provide interesting trade-offs, compared to previous belief update operators.

The rest of the article is as follows. Some formal preliminaries are given in Section 2. Our family of dependence-based update operators is presented in Section 3. Logical properties are discussed in Section 4 and computational properties are studied in Section 5. Dependence-based update is positioned with respect to action languages in Section 6. Connections to related work are given in Section 7. Finally, Section 8 concludes the article.

FORMAL PRELIMINARIES

In this section, we recall the necessary background definitions from propositional logic and complexity theory.

Propositional logic

We consider a propositional language FML Var built up from a finite (but arbitrarily large) set of propositional variables Var = {a, b, . . .}, the Boolean constants ⊤ and ⊥, and the connectives ¬, ∧, ∨, ⇒. Propositional formulas are denoted by Greek letters, typically α, β, µ, ϕ, ψ, etc. Var(ψ) denotes the set of propositional variables occurring in formula ψ, and |ψ| denotes the size of ψ, i.e., the number of symbols used to write it.

Interpretations over Var (or worlds) are denoted by ω, ω ′ , etc. We represent them as (maximal consistent) sets or conjunctions of literals over Var. For instance, if Var = {a, b, c}, then the world assigning variables a and c to true and variable b to false is denoted by {a, ¬b, c}. Formulas are interpreted in the classical way. The set of models of a formula ϕ is the set of interpretations ω such that ω |= ϕ; this set is denoted by Mod(ϕ). |= denotes classical entailment and ≡ denotes logical equivalence.

A literal is a propositional variable (a positive literal) or the negation of a propositional variable (a negative literal). For every literal l, l is the complementary literal of l, defined by l = ¬x when l = x ∈ Var is a positive literal, and l = x when l = ¬x (with x ∈ Var) is a negative literal. For a set of literals L we note L = {l | l ∈ L}. Lit Var is the set of literals of the language, i.e., Lit Var = x∈Var {x, ¬x} = Var ∪ Var.

If ω is a world and L a consistent set of literals from Lit Var , then (ω \ L) ∪ L is the world that gives the same truth value as ω to all variables except the variables of literals of L and such that every literal of L is true, that is, (ω \ L) ∪ L |= ( L). For instance, if ω = {a, ¬b, c, d} and L = {b, c, ¬d} then (ω \ L) ∪ L = {a, b, c, ¬d}.

The set of literals of a formula is inductively defined as follows:

Lit(⊤) = ∅ Lit(⊥) = ∅ Lit(x) = {x} for x ∈ Var Lit(¬ϕ) = Lit(ϕ) Lit(ϕ ∧ ψ) = Lit(ϕ) ∪ Lit(ψ) Lit(ϕ ∨ ψ) = Lit(ϕ) ∪ Lit(ψ) Lit(ϕ ⇒ ψ) = Lit(ϕ) ∪ Lit(ψ) For instance, for ϕ = ¬((¬a ∧ b) ∨ (a ∧ c)) we have Lit(ϕ) = {a, ¬a, ¬b, ¬c}.
Equivalently, Lit(ϕ) is the set of literals occurring in the Negation Normal Form of ϕ, noted NNF(ϕ), that is obtained by "pushing down" every occurrence of ¬ in ϕ (including the implicit negations conveyed by ⇒), then removing double negations (over variables). Formally, NNF(ϕ) is inductively defined as follows:

-if ϕ ∈ Var ∪ {⊤, ⊥}, then NNF(ϕ) = ϕ; -if ϕ = α ∧ β then NNF(ϕ) = NNF(α) ∧ NNF(β); -if ϕ = α ∨ β then NNF(ϕ) = NNF(α) ∨ NNF(β); -if ϕ = α ⇒ β then NNF(ϕ) = ¬NNF(α) ∨ NNF(β); -if ϕ = ¬α with α ∈ Var ∪ {⊤, ⊥} then NNF(ϕ) = ¬α; -if ϕ = ¬(¬α) then NNF(ϕ) = NNF(α); -if ϕ = ¬(α ∧ β) then NNF(ϕ) = NNF(¬α) ∨ NNF(¬β); -if ϕ = ¬(α ∨ β) then NNF(ϕ) = NNF(¬α) ∧ NNF(¬β); -if ϕ = ¬(α ⇒ β) then NNF(ϕ) = NNF(α) ∧ NNF(¬β).
When the morphology of the language is limited to the connectives ¬, ∧, ∨, ⇒, and the Boolean constants-as it is the case here-, then Lit(ϕ) can be computed in time linear in the size of ϕ.

The standard definition of uniform substitution stipulates that ϕ[x ← ψ] is the formula obtained by uniformly replacing in ϕ every occurrence of propositional variable x by the formula ψ. It will be convenient to extend this to literals; we identify

ϕ[¬x ← ψ] with ϕ[x ← ¬ψ]. For the example formula ϕ = ¬((¬a ∧ b) ∨ (a ∧ c)) we get ϕ[¬a ← ⊤] = ¬((¬¬⊤ ∧ b) ∨ (¬⊤ ∧ c)).

Computational Complexity

We assume that the reader is familiar with some basic notions of computational complexity, especially the complexity classes P, NP, and coNP, as well as with the basic decision problems SAT and UNSAT (and their restrictions to 3CNF formulas) and with the classes An advice-taking Turing machine is a Turing machine that has associated with it a special "advice oracle" A, which can be any function (which does not have to be computable). On input s, a special "advice tape" is automatically loaded with A(|s|) and from then on the computation proceeds as normal, based on the two inputs, s and A(|s|).

An advice-taking Turing machine uses polynomial advice if its advice oracle A satisfies |A(n)| ≤ p(n) for some fixed polynomial p and all non-negative integers n; finally, P/poly is the class of all languages that can be decided in polynomial time by deterministic Turing machines augmented by polynomial advice. It is known that if NP ⊆ P/poly, then PH collapses at the second level [START_REF] Karp | Some connections between non-uniform and uniform complexity classes[END_REF].

A GENERAL FAMILY OF DEPENDENCE-BASED UPDATE OPERATORS

Belief update operators [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF]] map a belief base ψ representing the initial beliefs of a given agent and an input formula µ reflecting the effect of some action or event to a new belief base ψ ⋄ µ, which corresponds to the beliefs held by the agent after the action or event took place. In this article we consider propositional belief bases, that we identify with formulas. We typically use ϕ, ψ, ψ ′ , etc. for belief bases and µ, µ ′ etc. for input formulas. To define ψ ⋄ µ as the conjunction of the input formula µ with ψ-called an expansion in the belief revision literature-would not be a good idea because ψ ∧ µ is inconsistent as soon as the input formula µ contradicts ψ. Similarly, belief revision operations [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF][START_REF] Katsuno | Propositional knowledge base revision and minimal change[END_REF] are not appropriate for updating belief bases; especially, the belief revision postulate (R2) [START_REF] Katsuno | Propositional knowledge base revision and minimal change[END_REF], stating that revision must reduce to expansion whenever µ is consistent with ψ, is not expected to hold. As a matter of illustration, consider the well-known example ψ = d ∨ w where d means "the door is open" and w means "the window is open." If ψ is revised by the more reliable formula µ = ¬d, it makes sense to assume after the revision step that "the door is closed and the window is open" since no action occurred. However, this conclusion cannot reasonably be drawn if the change formula µ = ¬d reflects the effect of the action of closing the door; indeed, assume that in the actual state of the world the door is open and the window is closed (which is a model of ψ); for sure, opening the window is not an expected effect of closing the door! [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF] proposed a general semantics for update operations. The most prominent feature of KM updates (distinguishing update from revision) is that they are performed modelwise:

Mod(ψ ⋄ µ) = ω|=ψ Mod(ω ⋄ µ).
(This is a consequence of the KM postulate (U8).) The literature contains many proposals for update operators. Several authors showed that there are good reasons for building an update operator from a dependence function [START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Herzig | Propositional belief update and minimal change[END_REF].

The dependence-based update of a belief base ψ by an input formula µ consists in first forgetting in ψ all information "related" to µ (leaving unchanged the variables that are not related to the update), and then expanding the result with µ. It remains to define the notion of "being related to" and the operation of forgetting.

Formula/Variable Dependence

A formula/variable dependence function is modeled as a mapping Dep v from FML Var to 2 Var . (The mapping has to be computable, although this is typically left implicit in the definitions.)

Many choices for Dep v are possible. Common examples of formula/variable dependence functions are the following.

(1) Syntactical Dependence. Dep v (µ) = Var(µ) is the set of propositional variables occurring in µ.

(2) Semantical Dependence. Dep v (µ) = RelVar(µ) ⊆ Var(µ) is the set of relevant variables of µ, defined by: x ∈ RelVar(µ) if and only if x occurs in every formula that is logically equivalent to µ; or, equivalently, x ∈ RelVar(µ) if and only if µ [START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Herzig | The PMA revisited[END_REF]Rifi 1998, 1999;[START_REF] Lang | Two forms of dependence in propositional logic: Controllability and definability[END_REF]];

[x ← ⊤] is not equivalent to µ[x ← ⊥] [
(3) Dependence Induced by Dependencies between Variables [START_REF] Herzig | Propositional belief update and minimal change[END_REF].

Let δ v be a primitive variable dependence function, i.e., a mapping from 2 Var to 2 Var such that for every X ⊆ Var we have X ⊆ δ v (X). (When X is a singleton {x}, we write δ v (x) instead of δ v (X) in order to alleviate notation.) Often δ v can by built from a more basic reflexive relation r v on Var × Var:

δ v (X) = x∈X {x ′ | (x, x ′ ) ∈ r v }.
We extend the mapping δ v to formulas by stipulating that Var δ v (ϕ) = δ v (Var(ϕ)), and RelVar δ v (ϕ) = δ v (RelVar(ϕ)). Dep v (ϕ) can be defined as any of these two sets, leading thus to two families of update operators.

Whatever the choice, given a dependence function Dep v , the set of models of the dependence-based update of a world ω by a formula µ w.r.t. Dep v , denoted by ω ⋄ Dep v µ, is the set of all worlds ω ′ such that ω ′ |= µ, and such that ω and ω ′ assign the same truth value to every propositional variable x such that x ∈ Dep v (µ): Equivalently, ω ′ ∈ Mod(ω ⋄ Dep v µ) if and only if the following two conditions are met:

Mod(ω ⋄ Dep v µ) = {ω ′ | ω ′ |= µ and Var(ω ′ \ ω) ⊆ Dep v (µ)}. 2
(1) ω ′ |= µ;

(2) ω and ω ′ agree on all propositional variables in Var \ Dep v (µ). (c,c),(c,d),(d,d)}. We have: b, c, d}, {¬a, ¬b, ¬c, d}, {a, b, c, d}, {a, ¬b, ¬c, d}}; Mod(ω b, c, d}, {¬a, ¬b, ¬c, d}, {¬a, b, c, ¬d}, {¬a, ¬b, ¬c, ¬d}}. Finally, the dependence-based update of a belief base ψ ∈ FML Var by the input formula µ w.r.t. Dep v is defined as follows:

Var(µ) = {a, b, c}; RelVar(µ) = {b, c}; Var δ v (µ) = {a, b, c, d}; RelVar δ v (µ) = {b, c, d}; Mod(ω ⋄ Var µ) = {{¬a,
⋄ RelVar µ) = {{¬a, b, c, d}, {¬a, ¬b, ¬c, d}}; Mod(ω ⋄ RelVar δv µ) = {{¬a,
Mod(ψ ⋄ Dep v µ) = ω|=ψ Mod(ω ⋄ Dep v µ).
Figure 1 sums up the various dependence functions Dep v and the associated update operators. In the last line the set P is some (fixed) subset of Var.

Interestingly, ⋄ Dep v operators can be characterized through the notion of variable forgetting [Lang et al. 2003a;[START_REF] Lin | How to progress a database (and why) I: Logical foundations[END_REF]. Indeed, let us define quantification over propositional variables as ∃x.ψ = ψ[x ← ⊤] ∨ ψ[x ← ⊥]; and let us define quantification over a finite set of variables X = {x 1 , . . . , x n } ⊆ Var as ∃X.ψ = ∃x 1 . . . ∃x n .ψ. Then the following holds: ψ ⋄ Dep v µ ≡ (∃Dep v (µ).ψ) ∧ µ [START_REF] Doherty | The PMA and relativizing change for action update[END_REF]].

Note that there exist other closely related belief update operators that are explicitly based on a dependence function [START_REF] Delgrande | Gricean belief change[END_REF][START_REF] Vo | A syntax-based approach to reasoning about action and belief update[END_REF]]; they will be discussed in the related work section.

Formula/Literal Dependence

Unfortunately, forgetting everything about the variables involved in the update often leads to forgetting too much. Let us consider the following scenario.

Example 3.2. Let us consider a mobile robot whose internal state is described by the truth values given to a number of fluents, like powerOn, engineReady, batteryOK, etc. Assume that we know at start that the robot satisfies ψ = powerOn ∧ engineReady ∧ ¬batteryOK; if the action of making µ = (powerOn ∨ engineReady) ∧ batteryOK true is performed, then under any formula/variable dependence function Dep v such that {powerOn, engineReady, batteryOK} ⊆ Dep v (µ), we get ψ ⋄ Dep v µ ≡ µ. We thus forgot that initially power was on and the engine ready.

This is not what we expected: the input formula does not convey any evidence that our belief that power is on and the engine is ready should be changed; intuitively, we should not forget the initial information, because updating by µ has negative influence neither on powerOn nor on engineReady. Hence, only negative occurrences of powerOn and engineReady should be forgotten before expanding by the input formula, but not positive occurrences.

Another problem with the previous update operators based on formula/variable dependence is that they cannot handle persistent literals: literals that remain true once they become true.

Example 3.3. Suppose now that an additional fluent engineDead is added to the description of the internal state of the robot, and suppose that that the engine cannot be fixed. Assume that we know at start that ψ = powerOn ∧ engineReady ∧ engineDead. When the world evolves so that µ = ¬powerOn ∨ ¬engineReady ∨ ¬engineDead holds, then using any formula/variable dependence function Dep v such that {powerOn, engineReady, engineDead} ⊆ Dep v (µ), we obtain ψ ⋄ Dep v µ ≡ µ. Once again, this is not what we expected. Although ¬engineDead has a negative influence on engineDead, engineDead should not be forgotten because it is a persistent fluent, while ¬engineDead is not.

In the last example the truth value of the fluent is essential: formula/variable dependence is too coarse-grained to handle the problem. This calls for the following more fine-grained notion of dependence. Definition 3.4 (formula/literal dependence function). A formula/literal dependence function is a computable mapping Dep : FML Var → 2 Lit Var .

Intuitively, Dep(µ) is the set of literals that potentially become true when µ becomes true. The other way round, when l is absent from Dep(µ) then we know that under no circumstances an update by µ may make l true: if l is false before the update then it will remain false.

Many meaningful functions Dep can be considered. Similarly to formula/variable dependence functions, Dep(µ) can be basically defined as Lit(µ) or as RelLit(µ), where the latter is defined as follows.

Definition 3.5 (formula/literal independence [Lang et al. 2003a]). Let ψ be a formula from FML Var . ψ is Lit-independent of x iff ψ[x ← ⊤] |= ψ, and ψ is Litindependent of ¬x iff ψ[x ← ⊥] |= ψ. Finally, for l ∈ Lit Var , ψ is Lit-dependent on l if and only if it is not Lit-independent of l. We denote by RelLit(ψ) the set of literals ψ depends on.

Example 3.6. The formula ¬a ∨ (a ∧ b) is Lit-dependent on ¬a, and Lit-independent of a. The latter is the case because

(¬a ∨ (a ∧ b))[a ← ⊤] = ¬⊤ ∨ (⊤ ∧ b) ≡ b, and b |= ¬a ∨ (a ∧ b). The formula ψ = (a ∨ b) ∧ (¬a ∨ c) ∧ (a ∨ b ∨ ¬c) is Lit-dependent on a, ¬a, b and c; but not on ¬c. The latter is the case because ψ[c ← ⊥] = (a ∨ b) ∧ (¬a ∨ ⊥) ∧ (a ∨ b ∨ ¬⊥), which is equivalent to (a ∨ b) ∧ ¬a, and (a ∨ b) ∧ ¬a |= (a ∨ b) ∧ (¬a ∨ c) ∧ (a ∨ b ∨ ¬c).
We have RelLit(ψ) = {a, ¬a, b, c}.

An alternative, equivalent definition [Lang et al. 2003a] is: ψ is Lit-independent of l if and only if there is an equivalent formula ϕ such that l ∈ Lit(ϕ).

Here are some observations. First, RelLit(µ) is a subset of Lit(µ), while the converse is false. Second, µ is Lit-independent of x if and only if µ More sophisticated dependence functions can be designed by presupposing the existence of a primitive literal dependence function, i.e., a mapping δ l : 2 Lit Var -→ 2 Lit Var , such that for every L ⊆ Lit Var , L ⊆ δ l (L). Some natural constraints may be imposed on δ l ; for example, monotonicity: if

[x ← ⊤] |= µ[x ← ⊥],
L 1 ⊆ L 2 then δ l (L 1 ) ⊆ δ l (L 2 ). We can then define Lit δ l (µ) = δ l (Lit(µ)), RelLit δ l (µ) = δ l (RelLit(µ)).
When l ∈ δ l ({l 1 , . . . , l n }) then the truth of l 1 ,. . . , l n releases the truth of l. This turns out to be particularly useful to solve the ramification problem: whenever a literal l is caused by the truth of some set of literals L then it is natural to have l ∈ δ l (L). This can be ensured by defining

Dep = Lit δ l (resp. Dep = RelLit δ l ), provided that L ⊆ Lit(µ) (resp. L ⊆ RelLit(µ)) with δ l monotone.
The truth values of such derived fluents can then be updated through the use of some integrity constraints (reflecting static laws), which have to be conjoined with the input formula.

Example 3.7. Suppose now that an additional fluent readyToMove is added to the description of the internal state of the robot. It is a derived fluent and its connections with the previous three primitive fluents are given by the static law

ϕ = ((¬engineDead ∧ powerOn ∧ engineReady) ⇒ readyToMove) ∧ (readyToMove ⇒ (¬engineDead ∧ powerOn ∧ engineReady)).
Assume that initially ψ = powerOn ∧ engineReady ∧ ¬engineDead ∧ readyToMove.

Assume also that µ = ¬powerOn ∨ ¬engineReady ∨ engineDead.

Suppose Dep = Lit δ l where δ l is such that ¬readyToMove ∈ δ l ({¬powerOn, ¬engineReady, engineDead}).

If the world evolves so that µ holds then readyToMove is forgotten, as expected.

Using our formula/literal dependence functions, one can also easily take into account persistent literals, i.e., literals remaining true whatever happens, such as engineDead (contrarily to ¬engineDead). For example, a possible dependence function is

Dep(µ) = RelLit(µ) \ PersLit, where PersLit is a given set of persistent literals. Example 3.8. Let ψ = powerOn ∧ engineReady ∧ engineDead and let µ = ¬powerOn ∨ ¬engineReady ∨ ¬engineDead. If PersLit = {engineDead}, then Dep(µ) = RelLit(µ) \ PersLit = {¬powerOn, ¬engineReady},
and engineDead will not be forgotten in ψ.

Update Based on Formula/Literal Dependence

We are now ready to define our update operators based on formula/literal dependence: Definition 3.9 (update based on formula/literal dependence). Let Dep be a formula/ literal dependence function. Let ϕ be a formula representing integrity constraints. The set of models of the update based on formula/literal dependence ω ⋄ ϕ Dep µ of the world ω by the formula µ w.r.t. Dep and ϕ is the set of all worlds ω ′ such that ω ′ |= µ ∧ ϕ and ω ′ \ ω ⊆ Dep(µ). In symbols: Definition 3.11 (literal forgetting [Lang et al. 2003a]). Let ψ be a formula and let L ⊆ Lit Var . Then ∃ l L.ψ is the formula inductively defined by:

Mod(ω ⋄ ϕ Dep µ) = {ω ′ |= µ ∧ ϕ | ω ′ \ ω ⊆ Dep(µ)}. Last, if ψ is a formula from FML Var , then Mod(ψ ⋄ ϕ Dep µ) = ω|=ψ Mod(ω ⋄ ϕ Dep µ). An equivalent formulation of Mod(ω ⋄ ϕ Dep µ) is: Mod(ω ⋄ ϕ Dep µ) = L⊆Dep(µ) {ω ′ |= µ ∧ ϕ | ω = (ω ′ \ L) ∪ L}.
∃ l ∅.ψ = ψ ∃ l {l}.ψ = ψ[l ← ⊤] ∨(¬l ∧ ψ) ∃ l ({l} ∪ L).ψ = ∃ l L.(∃ l {l}.ψ)
∃ l L.ψ is (up to logical equivalence) the logically strongest consequence of ψ that is Lit-independent of L, i.e., it is Lit-independent of each l ∈ L (see Proposition 16 from Lang et al. [2003a]).

On this ground, the following characterization of ψ ⋄ ϕ Dep µ follows. PROPOSITION 3.12. Let Dep be a formula/literal dependence function. Let ϕ be a formula representing integrity constraints. Let ψ and µ be two formulas. We have: Lang et al. [2003a], we get that

ψ ⋄ ϕ Dep µ ≡ µ ∧ ϕ ∧ ∃ l Dep(µ).ψ PROOF. From Proposition 15 of
Mod(µ ∧ ϕ ∧ ∃ l Dep(µ).ψ) = {ω ′ |= µ ∧ ϕ | (ω ′ \ L) ∪ L |= ψ where L ⊆ Dep(µ)} = ω|=ψ {ω ′ |= µ ∧ ϕ | ω = (ω ′ \ L) ∪ L where L ⊆ Dep(µ)} = ω|=ψ {ω ′ |= µ ∧ ϕ | ω = (ω ′ \ L) ∪ L where L ⊆ Dep(µ)} = Mod(ψ ⋄ ϕ Dep µ) Example 3.13. Let ψ = (¬a ∨ ¬d) ∧ (a ∨ b) ∧ (a ∨ c ∨ d), µ = d and let Dep = RelLit and ϕ = ⊤. We have Dep(µ) = {d} and ∃ l {¬d}.ψ ≡ (a ∨ b) ∧ (a ∨ c ∨ d); hence ψ ⋄ ϕ Dep µ ≡ d ∧ (a ∨ b).
A direct consequence of Proposition 3.12 is that we also have ψ ⋄

ϕ Dep µ ≡ µ ∧ ϕ ∧ ∃ l (Dep(µ) ∩ Lit(ψ)).ψ. Indeed, if l ∈ Dep(µ) and l ∈ Lit(ψ), then ∃ l Dep(µ).ψ is equivalent to ∃ l (Dep(µ) \ {l})
.ψ: forgetting literals not occurring in a formula does not change anything.

Clearly enough, our family of operators contains all previous operators based on formula/variable dependence. PROPOSITION 3.14. Every update operator based on formula/variable dependence is an update operator based on formula/literal dependence.

PROOF. Given that ∃{x}.ψ ≡ ∃ l {x, ¬x}.ψ for every formula ψ and variable x (see Proposition 20 from Lang et al. [2003a]), any operator ⋄ Dep v based on formula/variable dependence is the same as the update operator ⋄ ⊤ Dep based on formula/literal dependence, where Dep is defined by Dep(α) = x∈Dep v (α) {x, ¬x} for any formula α.

ψ ⋄ ⊤ Dep e µ = ψ ∧ µ ψ ⋄ ⊤ Dep f µ = µ if ψ is consistent ⊥ otherwise PROOF.
For the case of the empty dependence function we use that ∃ l ∅.ψ is equivalent to ψ. For the case of the full dependence function, we use that ∃ l Lit Var .ψ ≡ ⊥ if ψ is inconsistent and ∃ l Lit Var .ψ ≡ ⊤ otherwise.

In the literature, ⋄ ⊤ Dep e is called the expansion operator.

RATIONALITY POSTULATES

We now examine the status of the KM postulates. We do so both in the general case and for specific formula/literal dependence functions. [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF] proposed the following eight postulates for characterizing rational update operators.

(U1) ψ ⋄ µ |= µ. (U2) If ψ |= µ then ψ ⋄ µ ≡ ψ. (U3) If ψ and µ are consistent then ψ ⋄ µ is consistent. (U4) If ψ 1 ≡ ψ 2 and µ 1 ≡ µ 2 then ψ 1 ⋄ µ 1 ≡ ψ 2 ⋄ µ 2 . (U5) (ψ ⋄ µ 1 ) ∧ µ 2 |= ψ ⋄ (µ 1 ∧ µ 2 ). (U6) If ψ ⋄ µ 1 |= µ 2 and ψ ⋄ µ 2 |= µ 1 then ψ ⋄ µ 1 ≡ ψ ⋄ µ 2 . (U7) If ψ is complete then (ψ ⋄ µ 1 ) ∧ (ψ ⋄ µ 2 ) |= ψ ⋄ (µ 1 ∨ µ 2 ). (U8) (ψ 1 ∨ ψ 2 ) ⋄ µ is equivalent to (ψ 1 ⋄ µ) ∨ (ψ 2 ⋄ µ).
These postulates are designed for updates without integrity constraints. For this reason, we assume in this section (and in this section only) that ϕ = ⊤. Note also that is possible to extend such postulates in order to account for integrity constraints (see [START_REF] Herzig | Propositional belief update and minimal change[END_REF] for such a contribution).

General Results

The relationships between the family of KM update operators and the family of update operators based on formula/literal dependence are made precise by the following propositions. First, Proposition 4.1 shows that the two families are disjoint because no update operator ⋄ ⊤ Dep based on formula/literal dependence satisfies both (U2) and (U3). Furthermore, giving up any of those two postulates is enough to overcome this impossibility: (2) There exists an update operator based on formula/literal dependence that satisfies all KM postulates but (U2).

(3) There exists an update operator based on formula/literal dependence that satisfies all KM postulates but (U3).

PROOF.

(1) Let ⋄ ⊤ Dep be an update operator based on formula/literal dependence. If ⋄ ⊤ Dep satisfies (U2), then for any formulas ψ and µ such that ψ |= µ holds, it must be the case that ψ ⋄ ⊤ Dep µ ≡ ψ. Equivalenty, if ψ |= µ holds, then we must have µ ∧ ∃ l Dep(µ).ψ ≡ ψ, which implies that ∃ l Dep(µ).ψ |= ¬µ ∨ ψ must be satisfied. Now, let Var = {a, b}, µ = a ∨ ¬b, and let us consider the following formulas: ¬(a ∨ ¬b) ∨ (¬a ∧ ¬b) is equivalent to ¬a, hence this entailment can be the case

(a) ψ 1 = a ∧ b. Since ψ 1 |= µ holds, we must have ∃ l Dep(a ∨ ¬b).(a ∧ b) |= ¬(a ∨ ¬b) ∨ (a ∧ b). ¬(a ∨ ¬b) ∨ (a ∧ b) is equivalent to b,
only if a ∈ Dep(a ∨ ¬b). (c) ψ 3 = ¬a ∧ b. By definition, ψ 3 ⋄ ⊤ Dep µ is equivalent to (a ∨ ¬b) ∧ ∃ l Dep(a ∨ ¬b).(¬a ∧ b).
From items (a) and (b) above, neither a nor ¬b belongs to Dep(a ∨ ¬b). As a consequence, we have [START_REF] Doherty | The PMA and relativizing change for action update[END_REF]]. (U6) Not satisfied by MPMA [START_REF] Doherty | The PMA and relativizing change for action update[END_REF]]. (U7) Not satisfied by MPMA [START_REF] Doherty | The PMA and relativizing change for action update[END_REF]]. (U8) Obvious from the definition of update operators based on formula/literal dependence.

∃ l Dep(a ∨ ¬b).(¬a ∧ b) ≡ ¬a ∧ b. Accordingly, ψ 3 ⋄ ⊤ Dep µ is inconsistent. Since neither ψ 3 nor µ is inconsistent, this contradicts the fact that ⋄ ⊤ Dep satisfies (U3). (
consistent but ψ ⋄ ⊤ Dep µ is not. (U4) Let ψ 1 = ψ 2 = a, µ 1 = ⊤, µ 2 = a ∨ ¬a and Dep = Lit; we have ψ 1 ≡ ψ 2 and µ 1 ≡ µ 2 , but ψ 1 ⋄ ⊤ Dep µ 1 ≡ a is not equivalent to ψ 2 ⋄ ⊤ Dep µ 2 ≡ ⊤. (U5) Not satisfied by MPMA
Finally, while Proposition 4.1 shows that the KM update operators and the update operators based on formula/literal dependence form two disjoint families, every operator from their union bounds in the same way the belief base ψ ⋄ µ resulting from the update of ψ by µ. Furthermore, these bounds are reached for both families of operators. Formally, we have the following. PROPOSITION 4.3. Let ⋄ be a KM update operator or an update operator based on formula/literal dependence, of the form ⋄ ⊤ Dep . Then for every formulas ψ and µ we have: Dep(µ).ψ. By definition of literal forgetting, ∃ l Dep(µ).ψ is a logical consequence of ψ. Then the result follows trivially.

ψ ∧ µ |= ψ ⋄ µ |= µ. PROOF. -If ⋄ is a KM update operator then it satisfies (U1), therefore ψ ⋄ µ |= µ. It remains to show that ψ ∧ µ |= ψ ⋄ µ. Consider the instance (ψ ⋄ ⊤) ∧ µ |= ψ ⋄ (⊤ ∧ µ) of (U5). By (U2), ψ ⋄ ⊤ ≡ ψ, and by (U4), ψ ⋄ (⊤ ∧ µ) ≡ ψ ⋄ µ. It follows from all this that ψ ∧ µ |= ψ ⋄ µ. -If ⋄ is an update operator based on formula/literal dependence, of the form ⋄ ⊤ Dep , then ψ ⋄ µ ≡ µ ∧ ∃ l

The Cases of Specific Dependence Functions

We now study some specific formula/literal dependence functions that are obtained by imposing some requirements on Dep. Proposition 3.15 already characterized the update operators that are based on empty and on full dependence functions. 3 We note that logically equivalent bases ψ 1 and ψ 2 are however updated equivalently: if

ψ 1 ≡ ψ 2 then ψ 1 ⋄ ϕ Dep µ ≡ ψ 2 ⋄ ϕ Dep µ.
Definition 4.4. Let Dep be a formula/literal dependence function.

-

Dep is standard iff RelLit(µ) ⊆ Dep(µ) for every µ. -Dep is syntax-independent iff µ 1 ≡ µ 2 implies Dep(µ 1 ) = Dep(µ 2 ) for every µ 1 , µ 2 . -Dep is monotone iff µ 1 |= µ 2 implies Dep(µ 1 ) ⊇ Dep(µ 2 ) for every µ 1 , µ 2 . -Dep is antimonotone iff µ 1 |= µ 2 implies Dep(µ 1 ) ⊆ Dep(µ 2 ) for every µ 1 , µ 2 . -Dep is confined iff Dep(µ) ⊆ Lit(µ) for every µ. -Dep is constant iff Dep(µ 1 ) = Dep(µ 2 ) for every µ 1 , µ 2 .
The mappings Lit and RelLit are neither monotone nor antimonotone: to see the former take µ 1 = a and µ 2 = a ∨ b; to see the latter take µ 1 = a ∧ b and µ 2 = a. They are also not constant. RelLit is syntax-independent while Lit is not. Finally, both mappings are standard and confined.

Clearly enough, since ⊥ |= µ and µ |= ⊤ for every formula µ, dependence functions that are both monotone and antimonotone are constant (and therefore syntaxindependent). Furthermore, for the same reason, given that Lit(⊥) = Lit(⊤) = ∅, there is a unique function that is both monotone and confined, or both antimonotone and confined, viz. the empty dependence function leading to the expansion operator (cf. Proposition 3.15. Moreover, there is exactly one dependence function that is both standard and monotone, viz. the full dependence function (because µ |= µ ∨ l for every l ∈ Lit), and there is exactly one dependence function that is both standard and antimonotone, viz. the full dependence function (because µ ∧ l |= µ for every l ∈ Lit).

These restrictions lead to operators satisfying more KM postulates as follows. Before proceeding to the proof of Proposition 4.5, we first state a lemma that will be used in the proof of Proposition 4.5 and then used again in Section 5. It relates Levesque's notion of separability [1998] and the following notion of Lit-separability: Definition 4.6 (Lit-separability). Two formulas α and β are said to be Lit-separable if and only if there is no l ∈ Lit Var such that l ∈ RelLit(α) and l ∈ RelLit(β).

Since ∃ l Dep(µ).ψ is Lit-independent of Dep(µ) (see Proposition 16 from Lang et al. [2003a]), we have that if Dep is a standard function then µ and ∃ l Dep(µ).ψ are Litseparable. This implies that they are also separable in Levesque's sense. LEMMA 4.7. If α and β are Lit-separable formulas, then they are separable in Levesque's sense [1998], that is, for every clause γ , we have α ∧ β |= γ if and only if α |= β or α |= γ . PROOF. From Theorem 5 of Lang et al. [2003a], there exist α ′ and β ′ such that α ≡ α ′ and β ≡ β ′ and α ′ and β ′ are Lit-simplified, that is, such that RelLit(α ′ ) = Lit(α ′ ) and RelLit(β ′ ) = Lit(β ′ ). Since α ≡ α ′ and β ≡ β ′ , we have RelLit(α ′ ) = RelLit(α) and RelLit(β ′ ) = RelLit(β); hence, α ′ and β ′ are two Lit-separable formulas and we have for every literal l ∈ Lit Var , if l ∈ Lit(α ′ ) then l ∈ Lit(β ′ ). We can assume w.l.o.g. that α ′ and β ′ are CNF formulas, so that α ′ ∧ β ′ is also a CNF formula. Now, let l be any literal occurring in α ′ ∧ β ′ and let x l be the corresponding variable; we know that for every literal l ′ , if l ′ ∈ Lit(α ′ ) then l ′ ∈ Lit(β ′ ) ; as a consequence, x l is pure in α ′ ∧ β ′ (i.e., l does not occur in α ′ ∧ β ′ ) or x l occurs either in α or in β, but not in both. Subsequently, there is no possible resolution step in α ′ ∧ β ′ between a clause from α and a clause from β: any resolvent γ of two clauses of α ′ ∧ β ′ is such that the two clauses are in α or the two clauses are in β. Assume that γ is the resolvent of two clauses of α (the other case is similar); then we still have that every variable occurring in (α ∧ γ ) ∧ β is pure or such that it occurs either in α ∧γ or in β, but not in both. A straightforward induction on the length of resolution proofs is enough to conclude that every clause that can be derived by (general) resolution from α ∧ β can be derived from α alone or from β alone. Since (general) resolution is complete in consequence-finding, we conclude that every prime implicate of α ∧β is a prime implicate of α or a prime implicate of β (see [START_REF] Marquis | Consequence finding algorithms[END_REF]] for details). Finally, Corollary 3 of [START_REF] Lang | Conditional independence in propositional logic[END_REF] shows that α and β are separable in Levesque's sense if and only if every prime implicate of α ∧ β is a prime implicate of α or a prime implicate of β, and this concludes the proof.

It is easy to check that Lit-separability alone is a sufficient condition for Levesque's separability. For instance, α = a ∨ b and β = ¬a ∨ ¬b are separable in Levesque's sense but are not Lit-separable. Now we proceed to the proof of Proposition 4.5.

PROOF.

(1) This is a direct consequence of Proposition 4.

1 , µ 2 ∈ FML Var , Dep(µ 1 ) = Dep(µ 2 ) = P. Hence ψ ⋄ ⊤ Dep µ 1 ≡ µ 1 ∧ ∃ l P.ψ and ψ ⋄ ⊤ Dep µ 2 ≡ µ 2 ∧ ∃ l P.ψ. If µ 1 ∧ ∃ l P.ψ |= µ 2 , then µ 1 ∧ ∃ l P.ψ |= µ 2 ∧ ∃ l P.ψ. Similarly, if µ 2 ∧ ∃ l P.ψ |= µ 1 , then µ 2 ∧ ∃ l P.ψ |= µ 1 ∧ ∃ l P.ψ. Accordingly, if ψ ⋄ ⊤ Dep µ 1 |= µ 2 and ψ ⋄ ⊤ Dep µ 2 |= µ 1 , then we have ψ ⋄ ⊤ Dep µ 1 ≡ ψ ⋄ ⊤ Dep µ 2 .
(5) Similarly, the result for (U7) comes from the fact that

∃ l Dep(µ).ψ |= ∃ l Dep(µ ∧ ϕ).ψ
when Dep is antimonotone.

COROLLARY 4.8. Let δ l be a primitive literal dependence function.

-The update operator ⋄ RelLit δ l satisfies (U1), (U3), (U4) and (U8). -The update operator ⋄ Lit δ l satisfies (U1), (U3) and (U8).

Taking δ l (L) = L for any L, we obtain, in particular, that ⋄ RelLit satisfies (U1), (U3), (U4) and (U8) and that ⋄ Lit satisfies (U1), (U3) and (U8).

A further property of decomposability has been proposed in [START_REF] Hoffmann | Message-based web service composition, integrity constraints, and planning under uncertainty: A new connection[END_REF]: formulas talking about disjoint sets of variables can be updated separately. 4 Formally, we have the following.

(D) if Var(ϕ 1 )∩Var(ϕ 2 ) = ∅, Var(ϕ 1 )∩Var(µ 2 ) = ∅, Var(µ 1 )∩Var(ϕ 2 ) = ∅ and Var(µ 1 )∩ Var(µ 2 ) = ∅, then (ϕ 1 ∧ ϕ 2 ) ⋄ (µ 1 ∧ µ 2 ) ≡ (ϕ 1 ⋄ µ 1 ) ∧ (ϕ 2 ⋄ µ 2 ).
We now say that a formula/literal dependence function Dep is decomposable if and only if for any pair of consistent formulas µ 1 and µ

2 , if Var(µ 1 ) ∩ Var(µ 2 ) = ∅, then Dep(µ 1 ∧ µ 2 ) = Dep(µ 1 ) ∪ Dep(µ 2
). This property is quite innocuous, and it is easy to check that it is verified by all the basic dependence functions Var, RelVar, Lit, RelLit and P. PROPOSITION 4.9. If Dep is confined and decomposable, then ⋄ Dep satisfies (D).

PROOF. Let Dep be confined and decomposable, and suppose ϕ 1 , ϕ 2 , µ 1 , µ 2 satisfy the conditions given in (D). By the definition of ⋄ Dep , if at least one of µ 1 and

µ 2 is inconsistent then (ϕ 1 ∧ ϕ 2 ) ⋄ Dep (µ 1 ∧ µ 2 )
is inconsistent and at least one of ϕ 1 ⋄ µ 1 and ϕ 2 ⋄ µ 2 is inconsistent. Hence (D) is satisfied. Assume now that both µ 1 and µ 2 are consistent. Because Dep is confined, we have Dep(µ 1 ) ⊆ Lit(µ 1 ) and

Dep(µ 2 ) ⊆ Lit(µ 2 ). Var(µ 1 ) ∩ Var(µ 2 ) = ∅ implies Lit(µ 1 ) ∩ Lit(µ 2 ) = ∅, therefore (1) Dep(µ 1 ) ∩ Dep(µ 2 ) = ∅. Now, ∃ l Dep(µ 1 ∧ µ 2 ).(ϕ 1 ∧ ϕ 2 ) ≡ ∃ l Dep(µ 1 ) ∪ Dep(µ 2 ).(ϕ 1 ∧ ϕ 2 )
because Dep is decomposable, which together with (1) and the definition of ∃ l , leads to

∃ l Dep(µ 1 ∧ µ 2 ).(ϕ 1 ∧ ϕ 2 ) ≡ (∃ l Dep(µ 1 ).ϕ 1 ) ∧ (∃ l Dep(µ 2 ).ϕ 2 ). Therefore, (ϕ 1 ∧ ϕ 2 ) ⋄ (µ 1 ∧ µ 2 ) ≡ (∃ l Dep(µ 1 ).ϕ 1 ) ∧ (∃ l Dep(µ 2 ).ϕ 2 ) ∧ (µ 1 ∧ µ 2 ) ≡ ((∃ l Dep(µ 1 ).ϕ 1 ) ∧ µ 1 ) ∧ ((∃ l Dep(µ 2 ).ϕ 2 ) ∧ µ 2 ) ≡ (ϕ 1 ⋄ Dep v µ 1 ) ∧ (ϕ 2 ⋄ Dep v µ 2 )
Since the dependence functions Lit and RelLit are both confined and decomposable, the corresponding update operators satisfy (D).

Here are now some general negative results.

PROPOSITION 4.10.

(1) No operator ⋄ ⊤ Dep based on a standard formula/literal dependence function satisfies (U2). [START_REF] Shapiro | Iterated belief change in the situation calculus[END_REF] No operator ⋄ ⊤ Dep based on a standard and confined formula/literal dependence function satisfies (U6).

PROOF.

(1) Let ψ = a ∧ b and µ = a ∨ ¬b. We have ψ |= µ. As Dep is standard, both a and ¬b are contained in Dep(µ). Therefore the set of literals Dep(µ) to be forgotten in ψ contains both ¬a and b. Hence

ψ ⋄ ⊤ Dep µ |= b. (2) Let ψ = a ∧ b, µ 1 = a ∨ ¬b and µ 2 = a. We have RelLit(µ 1 ) = Lit(µ 1 ) = {a, ¬b}.
If Dep is standard and confined, then Dep(µ 1 ) = {¬a, b} has to be forgotten in ψ. Hence we have ψ ⋄ ⊤ Dep µ 1 ≡ a. Thus, ψ ⋄ ⊤ Dep µ 1 |= µ 2 . Furthermore, we have Once again, NP-hardness is due to the fact that ψ may be inconsistent. Indeed, consider the update operator ⋄ Dep that is induced by the full dependence function (Dep f (µ) = Lit Var for every µ), which is both standard and constant. As we have seen in Proposition 3.15, ψ ⋄ Dep µ is equivalent to µ if ψ is consistent, and ⊥ otherwise. Hence if ψ is consistent then ψ ⋄ Dep v µ is equivalent to µ, which is always consistent when µ is a variable.

The Inference Problem

In this section, we investigate the complexity of the inference problem (or query entailment problem) from an updated base when operators based on formula/literal dependence are used. The problem is as follows: given four formulas ϕ, ψ, µ and γ , how difficult is it to determine whether ψ ⋄ ϕ Dep µ |= γ holds? We first identify the complexity in the general case, then focus on some specific cases obtained by imposing further restrictions on some parts of the input. Lang et al. [2003a] showed that determining whether ψ is Lit-dependent of l is an NP-complete task. On this ground, one could suspect that the query entailment problem for operators based on RelLit is beyond coNP. That is not the case: under reasonable assumptions on Dep, inference from an updated base when operators based on formula/literal dependence are used remains in coNP (this result slightly extends Theorem 15 from Liberatore [2000a], which focuses on the MPMA case). PROPOSITION 5.3. Let Dep be a formula/literal dependence function such that for any l ∈ Lit Var and µ ∈ FML Var , determining whether l ∈ Dep(µ) is in NP. Given four formulas ϕ, ψ, µ and γ , determining whether ψ

⋄ ϕ Dep µ |= γ holds is coNP-complete.
Hardness is still the case when ϕ is valid (no integrity constraints) and the input formula µ and the query γ are atoms.

PROOF.

Membership. If determining whether l ∈ Dep(µ) is in NP, then determining whether any given set L ⊆ Lit Var of literals is included in Dep(µ) is in NP as well. Hence for every positive instance L, µ of this decision problem there exists a certificate c of size polynomial in the input size such that verifying that L, µ is a positive instance can be achieved in (deterministic) polynomial when c is given. Now, the complementary problem to query entailment can be solved in nondeterministic polynomial time, thanks to the following algorithm. Let V = Var(ϕ) ∪ Var(ψ) ∪ Var(µ) ∪ Var(γ ); guess two worlds ω and ω ′ over V, a subset L of V ∪V and a string c (both of them being of polynomial size if the input size), then check in polynomial time that L ⊆ Dep(µ) using c, and check that ω |= ψ, ω ′ |= ϕ ∧ µ ∧ ¬γ and ω = (ω ′ \ L) ∪ L.

Hardness. The reduction from UNSAT is as follows: to ψ ∈ FML Var we associate in polynomial time the formulas ϕ = ⊤ and µ = y, γ = z where y and z are two fresh variables not occurring in ψ. Whatever Dep is, ψ is inconsistent if and only if

ψ ⋄ ϕ Dep µ |= γ ; this is because for every L ⊆ Lit Var , ∃ l L.ψ is inconsistent if and only if ψ is inconsistent.
Lemma 4.7 is a valuable property from a computational point of view when CNF queries are considered since it shows that Lit-separability is a sufficient condition for separability in Levesque's sense. Indeed, thanks to Lemma 4.7, if there are no integrity constraints (i.e., ϕ ≡ ⊤) and if the dependence function is standard then inference from an updated base can be achieved by replacing one global entailment test by two simpler entailment tests, and exponential savings may be achieved this way in practice. Now, clausal entailment from ∃ l Dep(µ).ψ can be reduced in linear time to clausal entailment from a classical formula; this is achieved without turning ∃ l Dep(µ).ψ first into such a formula (by means of the definition of ∃ l ). Altogether, the two previous propositions give us some tractable restrictions for clausal query entailment from an updated belief base. Let us say that a subset C of FML Var is a tractable fragment for clausal entailment if and only if there exists a polytime algorithm for deciding whether ψ |= γ holds for any formula ψ from C and any CNF formula γ (see [START_REF] Darwiche | A knowledge compilation map[END_REF]). Many such fragments exist in the literature: the DNNF fragment (and its subsets DNF and OBDD < ), the Horn CNF fragment, the Krom fragment (conjunctions of binary clauses), the Blake fragment (formulas in prime implicates form), etc. We have the following corollary to the two previous propositions. COROLLARY 5.5. Let Dep be a standard dependence function. Let µ be a CNF formula from a tractable fragment for clausal entailment. Suppose also that determining whether any given literal l belongs to Dep(µ) can be achieved in polynomial time. Let ψ belong to a tractable fragment for clausal entailment. Then determining whether ψ ⋄ ⊤ Dep µ |= γ can be achieved in polynomial time for every CNF formula γ .

The conditions provided in this corollary hold for instance when Dep = RelLit, µ is a CNF formula from a tractable fragment for clausal entailment, which is stable for variable instantiation (see Proposition 11 in Lang et al. [2003a]), and ψ belongs to a tractable fragment for clausal entailment. To make things more concrete, say that ψ is a Horn CNF formula and µ is a Krom formula (a conjunction of binary clauses), or vice-versa. It is interesting to observe that in such a case, clausal entailment from the updated base ψ ⋄ ⊤ Dep µ is in P, thus computationally easier than clausal entailment from the corresponding expanded base ψ ∧ µ, under the assumption P = NP. Indeed, determining whether ψ ∧ µ |= γ is coNP-complete in this situation -tractable classes are known not to mix well.

Compactability Issues

We finally consider the compactability problem for updated bases when operators based on formula/literal dependence are used. In a nutshell, the problem is as follows: given three formulas ϕ, ψ, and µ, does there exist a propositional formula equivalent to ψ ⋄ ϕ Dep µ whose size is polynomial in the input size? Stated otherwise, is the propositional language FML Var enriched with ⋄ Dep (viewed as a connective) as succinct as FML Var , or is it strictly more succinct? Clearly enough, the naive rewriting of µ ∧ ϕ ∧ ∃ l Dep(µ).ψ into a propositional formula according to the definition of ∃ l , does not lead to a formula of size polynomial in the input size in the general case.

Formally, two versions of the compactability problem can be taken into account, depending on which notion of equivalence we choose [START_REF] Cadoli | The size of a revised knowledge base[END_REF].

-Logical compactability. ⋄ Dep is logically compactable if and only if there exists a polynomial p such that for every triple of propositional formulas ϕ, µ, ψ there exists a propositional formula such that:

( PROOF. For any L ⊆ Lit Var and any formula ψ, let ψ ′ L be the formula obtained by replacing in NNF(ψ) every occurrence of l ∈ L by an occurrence of l ′ ∈ L ′ , where symbols from

L ′ ⊆ Lit Var are fresh, i.e., {x ′ |x ′ ∈ L ′ or ¬x ′ ∈ L ′ } ∩ Var(ψ) = ∅. (For example, if ψ = a ∨ (¬a ∧ ¬b) and L = {a, ¬a, b} then ψ ′ L = a ′ ∨ (¬a ′ ∧ ¬b).) Let us consider the formula = ϕ ∧ µ ∧ ψ ′ L where L = Dep(µ) ∩ Lit(ψ).
µ) = ∃V.(µ ∧ ϕ ∧ ∃ l Dep(µ) ∩ Lit(ψ).ψ) is equivalent to µ ∧ ϕ ∧ ∃ l Dep(µ) ∩ Lit(ψ).ψ since every variable from Var(µ ∧ ϕ ∧ ∃ l Dep(µ) ∩ Lit(ψ).ψ) is in V. Now, since every variable from µ ∧ ϕ also is in V, we have that ∃V.(µ ∧ ϕ ∧ ψ ′ L ) is equivalent to µ ∧ ϕ ∧ ∃V.ψ ′ L , which is also equivalent to µ ∧ ϕ ∧ ∃ l V ∪ V.ψ ′ L . Since every literal of Lit(ψ ′ L ) is in V ∪ V, except the literals from L ′ , ∃V. is equivalent to µ ∧ ϕ ∧ ∃ l L ′ .ψ ′ L . But ∃ l L ′ .ψ ′ L is equivalent to ∃ l L.
ψ (quantified literals are 'dummy literals') and the substitution metatheorem for propositional logic concludes the proof.

There is no such a general result for ⋄ Dep operators w.r.t. logical compactability. Intuitively, some ⋄ Dep operators are logically compactable because they lead to forget no literal (except a preset number of them) or to forget every literal (except a preset number of them); for instance, the update operators induced by Dep(µ) = ∅ and Dep(µ) = Lit Var for every µ are logically compactable. Some other operators are not logically compactable. We have the following result, which slightly extends Theorem 10 from [START_REF] Liberatore | The compactness of belief revision and update operators[END_REF].

PROPOSITION 5.7. Let Dep be any standard and confined formula/literal dependence function. Then ⋄ Dep is not logically compactable unless the polynomial hierarchy collapses.

PROOF. First of all, it is obvious that the (non-standard) third parameter ϕ (the integrity constraints) of ⋄ Dep operators has no influence at all on the logical compactability issue of the operator: ⋄ Dep is logically compactable if and only if the standard (i.e., with two parameters) update operator ⋄ ⊤ Dep is logically compactable. Accordingly, we now assume that ϕ = ⊤. Let 3CNF n be the set of all propositional CNF formulas ψ, such that each clause of ψ contains at most 3 literals, and Var(ψ) contains n elements. We take advantage of Theorem 2.3 from [START_REF] Cadoli | The size of a revised knowledge base[END_REF]. This theorem says that if ⋄ is a belief change operator and if there exists a polynomial p such that for every integer n > 0, there exists a pair of formulas ψ n and µ n such that -|ψ n | + |µ n | ≤ p(n), and -for every formula π ∈ 3CNF n , there exists a world ω π over Var(ψ n ) ∪ Var(µ n ) that can be computed from π in polynomial time and which is such that π is consistent if and only if

ω π |= ψ n ⋄ µ n .
Then if ⋄ is query-compactable, then NP ⊆ P/poly. Let us consider the set X n = {x 1 , . . . , x n } of variables from Var. Let π max n be the conjunction of all clauses containing at most three literals built up from X n . π max n has a size polynomial in n since it contains O(n 3 ) clauses. Furthermore, viewing CNF formulas as sets of clauses, each π ∈ 3CNF n is (up to a variable renaming) a subset of π max n . To every clause γ i of π max n we associate a new symbol c i not occurring in X n . We now define ψ n , µ n and ω π as follows:

-

ψ n = ( γ i ∈π max n (¬c i ∨ γ i )) ∨ ¬t where t is a new symbol (not in X n and different of any c i ); -µ n = (( x i ∈X n ¬x i ) ∨ y) ∧ (( x i ∈X n x i ) ∨ z)
where y and z are two new symbols (not in X n and different of any

c i ); -ω π is such that for every x ∈ Var(ψ n ) ∪ Var(µ n ), ω π (x) = 0 if x = c i and γ i ∈ π , and ω π (x) = 1 otherwise.
If π is consistent, then it has a model ω ′ over X n ; let us extend ω ′ to Var(ψ n )∪Var(µ n ), by imposing that x ∈ ω ′ if x = c i and γ i ∈ π , and x ∈ ω ′ otherwise. By construction, we have ω

′ |= ψ. Now, let L = {x i ∈ X n | x i ∈ ω ′ } ∪ {¬x i | x i ∈ X n and x i ∈ ω ′ }. We have L ⊆ X n ∪ X n . Now, we also have X n ∪ X n ⊆ Dep(µ) since RelLit(µ) = X n ∪ X n ∪ {y, z}. As a consequence, we get L ⊆ Dep(µ). Since ω ′ = (ω π \ L) ∪ L, we get that ω π |= ψ n ⋄ ϕ Dep µ n . If π is inconsistent, then assume that ω π |= ψ n ⋄ ϕ Dep µ n . Then there exists a world ω ′ over Var(ψ n ) ∪ Var(µ n ) and a subset L of Dep(µ) such that ω ′ = (ω π \ L) ∪ L. Since c i ∈ Dep(µ) for every i, we have c i ∈ ω ′ iff c i ∈ ω π . Since π is inconsistent, we get that ω ′ |= γ i ∈π max n (¬c i ∨ γ i )
. Therefore, we have t ∈ ω ′ . But ¬t ∈ Dep(µ), so we should also have t ∈ ω π , contradiction.

Nevertheless, tractable cases can be achieved by restricting the input so that a formula logically equivalent to ∃ l Dep(µ).ψ and of size polynomial in the input size can be computed. Blake. It is then enough to take advantage of Proposition 19 from Lang et al. [2003a] showing that a prime implicate formula equivalent to ∃ l Dep(µ).ψ can be computed in polynomial time as the conjunction of all prime implicates of ψ that does not contain any literal from Dep(µ). DNNF. It is necessary to generalize Theorem 9 from [START_REF] Darwiche | Decomposable negation normal form[END_REF]] to literal forgetting. Let us note DNNF(∃ l L.ψ) where L ⊆ Lit Var and ψ is a DNNF formula the propositional formula defined by structural induction as follows:

-if ψ is a Boolean constant or a literal not belonging to L, then

DNNF(∃ l L.ψ) = ψ; -if ψ is a literal from L, then DNNF(∃ l L.ψ) = ⊤; -if ψ is a conjunction n i=1 α i , then DNNF(∃ l L.ψ) = n i=1 DNNF(∃ l L.α i ); -if ψ is a disjunction n i=1 α i , then DNNF(∃ l L.ψ) = n i=1 DNNF(∃ l L.α i ).
Clearly enough, DNNF(∃ l L.ψ) can be computed in linear time. It remains to show that ∃ l .ψ ≡ DNNF(∃ l L.ψ). We do so by structural induction on ψ.

Base. If ψ is a Boolean constant or a literal not belonging to L, then

DNNF(∃ l L.ψ) = ψ is equivalent to ∃ l L.ψ since in such a case ψ is Lit-independent of L. If ψ is a literal from L, then DNNF(∃ l L.ψ) = ⊤ is equivalent to ∃ l L.ψ (just consider the definition of ∃ l L.ψ). Inductive step. If ψ is a conjunction n i=1 α i , then DNNF(∃ l L.ψ) = n i=1 DNNF(∃ l L.α i ).
By induction hypothesis each DNNF(∃ l L.α i is equivalent to the corresponding ∃ l L.α i . From Item 2. of Corollary 2 in Lang et al. [2003a] we know that for each i ∈ {1, . . . , n},

∃ l L. n i=1 α i |= ∃ l L.α i holds. Hence we have ∃ l L. n i=1 α i |= n i=1 (∃ l L.α i ). It remains to show that n i=1 (∃ l L.α i ) |= ∃ l L. n i=1 α i . Let ω be a model of n i=1 (∃ l L.α i ) on Var(ψ).
Then ω is a model of ∃ l L.α i on Var(ψ) for each i ∈ {1, . . . , n}. By Proposition 15 from Lang et al. [2003a], for each i ∈ 1 . . . n, there exists a subset L i of Var(α i ) ∪ Var(α i ) and a model ω i of α i on Var(α i ) such that ω i = (ω \ L i ) ∪ L i . Now, since ψ = n i=1 α i is a DNNF formula, the sets Var(α i ) (i ∈ {1, . . . , n}) are pairwise disjoint. Hence the world ω ′ on Var(ψ) defined by: for all x ∈ Var, if x ∈ Var(α i ) then x ∈ ω ′ iff x ∈ ω, is a model of ψ. Furthermore, the L i 's are also pairwise disjoint. Hence, we have

ω ′ = (ω \ n i=1 L i )) ∪ n i=1 L i ). Since n i=1 L i ⊆ L, we get that ω is a model of ∃ l L.ψ and the result follows. Finally, if ψ is a disjunction n i=1 α i , then DNNF(∃ l L.ψ) = n i=1 DNNF(∃ l L.α i ) is equivalent to ∃ l L
.ψ: this follows directly from Proposition 17 from Lang et al. [2003a] and the induction assumptions stating that each DNNF(∃ l L.α i ) is equivalent to the corresponding ∃ l L.α i .

DEPENDENCE-BASED UPDATE AND ACTION PROGRESSION

It is well-known that belief update and action progression are highly related (see an extended discussion in [START_REF] Lang | Belief update revisited[END_REF]). Especially, since belief update can be used as a language for specifying action effects, it can be used for reasoning about action and planning. We start by reviewing some recent works that go in this direction. Liberatore [2000b] presents a framework for reasoning about actions, whose semantics can be seen as a proper restriction of the one pointed out in [START_REF] Baral | Representing actions: Laws, observations and hypotheses[END_REF], but which remains expressive enough to incorporate many update settings, including Winslett's PMA. In this framework, minimization of change is achieved through the minimization of happens statements (a primitive allowing to declare that a given action occurs at a given time point). Only deterministic actions are formalized in this framework, making it inappropriate for modeling nondeterministic updates (like the one happening when tossing a coin). This strongly contrasts with our approach. [START_REF] Amir | Logical filtering[END_REF] define a logical filtering operation that takes a belief state represented compactly by a propositional formula and consider actions with conditional effects of the form if α then a causes ϕ, where α and ϕ are propositional formulas. This filtering operator corresponds to WSS [START_REF] Winslett | Updating Logical Databases[END_REF]] enriched with conditional updates. Then they go further and address the practical computation of this conditional update operator, depending on the syntax of the input belief base. Most of the results of [START_REF] Amir | Logical filtering[END_REF] can be easily generalized to our update operators based on formula/literal dependence, thus completing nicely our results in Section 5. A first-order extension of logical filtering has also been proposed by [START_REF] Shirazi | First-order logical filtering[END_REF]. In such a general setting, the update issue is much more difficult (especially, progressing a belief state is known to be not first-order definable [START_REF] Lin | How to progress a database[END_REF]). In [START_REF] Shirazi | First-order logical filtering[END_REF], the authors present some restrictions on the belief state representations and on the action representations enabling some tractable algorithms for logical filtering to be designed. [START_REF] Lang | Belief update revisited[END_REF] characterizes the class of feedback-free actions for which progression corresponds to a belief update, and shows that two well-known forms of action regression correspond in a natural way to two forms of "reverse update". Now, let us investigate deeper the respective position of belief update and propositional action languages [START_REF] Baral | Logic Programming and Reasoning about Actions[END_REF][START_REF] Giunchiglia | An action language based on causal explanation: Preliminary report[END_REF][START_REF] Giunchiglia | Nonmonotonic causal theories[END_REF][START_REF] Mccain | Causal theories of action and change[END_REF]. Both frameworks are based on propositional logic and aim at expressing compactly action effects and reasoning about them. How do they compare in terms of expressivity? What is the position of dependency-based update in this zoo of propositional action representation languages?

Two remarks come immediately to mind.

-"Update" actions are specific actions with only one effect -in other terms, updating by α corresponds to progressing by the action "make α true" -and this effect α can be any propositional formula; on the other hand, action languages consider only 'literal' effects of the form a causes l, where l is a literal. -Action languages contain many constructs for "combining" action effects: conditional effects (if γ then a causes l), concurrent actions, as well as static causal rules (for ramifications). They can also express some forms of nondeterminism, using their nonmonotonic semantics in a clever way, or by the release construct, which nondeterministically reassigns the truth value of a variable.

A first conclusion emerging from these observations is that the expressivity of belief update comes from its handling of complex effects (expressed by arbitrary propositional formulas) while the expressivity of action languages comes from its ability to combine action effects. On the latter point, it is not difficult to enrich belief update so as to integrate these constructs; the second half of [START_REF] Herzig | Updates, actions, and planning[END_REF] shows how update operators can be extended so as to deal with more complex change formulas (so-called "extended inputs" ). An interesting feature of such extended updates is that they do not imply any complexity shift with respect to the corresponding basic updates for the inference problem (especially, when dependence-based updates operators are considered, the inference problem remains coNP-complete).

We focus first on conditional and concurrent updates. If we consider the restriction of ⋄ Dep to the case when the input formula is a literal, then when Dep = RelLit, we have Dep(l) = {l}, and therefore, ω ⋄ Dep l = (ω \ {l}) ∪ {l}, i.e., ω ⋄ Dep l is the model obtained from ω by forcing l to be true, which gives the same truth value as ω to all variables except Var(l). Consider now an update by the extended input

= (if C 1 then l 1 ) || . . . || (if C 1 then l n ), and let Ŵ + (l) = {C i |l i = l}. Then we have ∀x ∈ VAR, ω ⋄ Dep |= x iff ω |= (x ∧ ¬Ŵ + (¬x)) ∨ Ŵ + (x).
We recover here a well-known concept in the literature on reasoning about action: a successor state axiom. This result shows how ⋄ Dep can be positioned with respect to propositional action languages: both conditional update and progression in action languages coincide when conditional update is restricted to literal inputs (but allows for conditional and concurrent updates), and actions languages are restricted to dynamic effects (no static causal effects).

We focus now on nondeterminism. We see from our discussion above that there are two ways of expressing nondeterministic effects: either by using disjunctive effects (make a ∨ b true) or by using nondeterministic effect trigerring (make a true or make b true). This dichotomy in the expression of nondeterminism has been discussed first in [START_REF] Brewka | How to do things with worlds: On formalizing actions and plans[END_REF]. Some nondeterministic actions, such as tossing a coin, can be expressed easily in both ways (release p, equivalent to a nondeterministic update by p ∪ ¬p; and a dependency-based update by p ∨ ¬ p with Dep(p ∨ ¬p) = {p, ¬p}). However, some actions are more succinctly expressed using one of these two ways; for instance, making an equivalence true ("update by (p ⇒ q) ∧ (q ⇒ p)") can be expressed in action languages but in a less intuitive and less compact way (for instance, by the four static causal rules p causes q; q causes p; ¬p causes ¬q; ¬q causes ¬p), which demonstrates that allowing for complex effects gives much more flexibility than allowing just literals.

Moreover, identifying the literals on which the direct effect of an action may have a negative influence (including the negations of those on which it depends as in our update operators) appears also as a key to discriminate a disjunctive effect from a nondeterministic effect. Indeed, frame axioms should not be considered for literals occurring in nondeterministic actions like "tossing a coin": head ⋄ Dep head ∪ ¬head is expected to be equivalent to ⊤, which can be achieved only if head is released. Such a distinction is salient in the completions of the generalized action theories proposed by Lang et al. [2003b], which are based on the concept of causal explanation [START_REF] Giunchiglia | Nonmonotonic causal theories[END_REF][START_REF] Mccain | Causal theories of action and change[END_REF], just as many action languages proposed so far, especially C [START_REF] Giunchiglia | An action language based on causal explanation: Preliminary report[END_REF]. [START_REF] Herzig | Propositional belief update and minimal change[END_REF] gave a comprehensive study of belief update, which exhaustively surveyed all works on belief update up to that date. To our knowledge, no survey of this kind has been published since then, and we believe that it is the right time to do so. We now briefly review a number of papers about belief update, published after [START_REF] Herzig | Propositional belief update and minimal change[END_REF] and, when this is relevant, discuss their connections to our dependencebased operators.

RELATED WORK

Dependence-Based Update

We start by listing a series of works which address various forms of belief update based on formula/variable dependence. Early works [START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Herzig | The PMA revisited[END_REF][START_REF] Herzig | Propositional belief update and minimal change[END_REF][START_REF] Winslett | Updating Logical Databases[END_REF]] have been already discussed in Section 3 and in [START_REF] Herzig | Propositional belief update and minimal change[END_REF]. Since then, many works have studied, under various points of view, belief update operators based on formula/variable or, more rarely, formula/literal dependence. We review them below. [START_REF] Vo | A syntax-based approach to reasoning about action and belief update[END_REF] introduce a belief update operator where the syntax of the input matters, but the syntax of the initial knowledge base (a propositional formula) does not. More precisely, it consists in applying the following operations in sequence:

(1) rewrite the knowledge base ϕ to a set of clauses C;

(2) saturate C by resolution on the variables of Var(µ);

(3) eliminate from C the clauses containing variables from Var(µ); (4) expand C by µ.

For instance, if ϕ = (p ∨ q) ∧ (¬p ∨ r) and µ = p then C = {p ∨ q, ¬p ∨ r}; after step 2 we have C = {p ∨ q, ¬p ∨ r, q ∨ r}; after step 3 we have C = {q ∨ r}; and finally, the result of the update is equivalent to (q ∨ r) ∧ p. It appears that, although defined in a different manner, this operator is identical to WSS; it provides thus an alternative, syntactic, characterization of WSS. [START_REF] Lang | Updating epistemic states[END_REF] extend dependence-based update operators to epistemic states, allowing to express various degrees of beliefs in the initial base as well as action effects with various degrees of plausibility. In this article, epistemic states are modeled as ordinal conditional functions and represented as propositional stratified belief bases. While the authors focus on formula/variable dependence functions, it would be easy to extend their work to formula/literal dependence functions.

Madali ńska-Bugaj and Łukaszewicz [2009] propose a first-order version of the MPMA, where the knowledge base is a closed first-order formula and the input formula is a Boolean combination of ground atoms. Allowing first-order knowledge bases and input formulas gives much more expressivity to the language-and, on the other hand, leads to the computational difficulties inherent to first-order logic. Clearly, since dependence-based update generalizes the MPMA, we could build a general framework for first-order dependence-based update, which would of course generalize the approach given in Madalinska-Bugaj and Łukaszewicz [2009].

General Families of Update Operators

We now review some works that define general families of update operators which include some dependence-based operators. [START_REF] Delgrande | Gricean belief change[END_REF] define Gricean update operators as follows. Given U ⊆ Var, a U-world is defined as a partial interpretation (also viewed as a term) associating each variable of U with a truth value. Given a formula µ, let Mod RelVar(µ) (µ) be the set of all RelVar(µ)-worlds implying µ. Let O = { ω | ω ∈ 2 Var } be a collection of so-called strongly centered partial preorders over the worlds (called faithful partial preorders in [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF]), that is, partial preorders such that ω ≺ ω ω ′ for all ω and ω ′ = ω. Then the Gricean update operator induced from O is defined by:

Mod(ϕ ⋄O µ) = ω ′ ∈Mod(ϕ) σ ∈Mod RelVar(µ) (µ) min ω ′ (Mod(σ )).
The very essence of Gricean updates is that after updating a consistent ϕ by a consistent µ, what we know about RelVar(µ) is exactly µ [Delgrande et al. 2005, Theorem 4.11]. Let us call this key condition "the Gricean property" (GR). Using propositional quantification the Gricean property can be written more formally as:

(GR) ∃(Var\RelVar(µ)).(ϕ ⋄O µ) ≡ µ.
From this we can conclude that WSS↓ satisfies (GR) while WSS does not. In the general case, update operators based on formula/literal dependence are not Gricean either, since, for instance, updating a ∧ b by µ = a ∨ b using ⋄ Dep with Dep = RelLit leads to a formula equivalent to a ∧ b, which tells more about {a, b} than µ. The following result characterizes those update operators based on formula/literal dependence that satisfy the Gricean property:

C (µ 1 ∨ µ 2 ) ≡ (ϕ ⋄ C µ 1 ) ∨ (ϕ ⋄ C µ 2 ).
They also define a more general family of update operators, where compositional update is preceded by a syntactic transformation µ * of the input formula µ, giving rise to a family of generalized compositional update operators ⋄ * C ; for instance, µ * can be NNF(µ), or the conjunction of its prime implicates, or the disjunction of all conjunctions of literals corresponding to its models, or the disjunctions of all conjunctions of literals corresponding to its models restricted to the set of variables occurring in µ. In the latter case, ⋄ * C is shown to be equivalent to WSS. This shows that the class of generalized compositional updates and the class of dependence-based updates overlap. Characterizing their intersection precisely is an interesting open issue.

Update and Observations

Hunter and [START_REF] Hunter | Iterated belief change due to actions and observations[END_REF] propose a general framework for reasoning about action and change, where ontic actions are expressed by updates while observations are expressed by revisions. Especially, they define a new class of belief change operators, called belief evolution operators. A belief evolution operator takes two arguments: a set of states and an alternating sequence of actions and observations. Each belief evolution operator is defined with respect to a fixed update operator and a fixed AGM revision operator. The authors show that the interaction between update and revision can be complex, and specify how an agent should consider the history of actions when incorporating a new observation. In contrast, existing formalisms for reasoning about epistemic action effects either ignore the interaction between revision and update or they deal with it implicitly.

In the same vein, [START_REF] Shapiro | Iterated belief change in the situation calculus[END_REF] define a very expressive framework for reasoning about action and change, integrating revision and update, within the situation calculus. Generalizing belief update so as to take observations into account was also the key point of generalized update [START_REF] Boutilier | A unified model of qualitative belief change: A dynamical systems perspective[END_REF]]. Finally, belief extrapolation [Dupin de [START_REF] De Saint-Cyr | Belief extrapolation (or how to reason about observations and unpredicted change)[END_REF] focuses on reasoning about time-stamped observations by minimizing change, but without any action progression component.

Belief Update Beyond Classical Logic

There have been also a few recent extensions of belief update beyond classical logic, that we review briefly now. [START_REF] Liu | Updating description logic A-boxes[END_REF] consider the update problem in description logics. One of their main results is that there are cases where, for a fixed logic used to express the knowledge base, the result of an instance level evolution operation, i.e., when only the Abox is modified, is not expressible in the language of the logic under consideration. In particular, they show that this is the case for the description logic ALC. Contrastingly, de [START_REF] De Giacomo | On the update of description logic ontologies at the instance level[END_REF] show how Winslett's PMA can be extended to the description logic DL-Lite in a way such that the updated base is still expressible in DL-Lite. In de [START_REF] De Giacomo | On the approximation of instance level update and erasure in description logics[END_REF], the authors propose to address the problem of limited expressivity by resorting to a notion of maximal approximation of update and illustrate it by focusing on a restriction of the logic considered in the previous paper. Obviously enough, such expressiveness issues do not arise in the simple setting of classical propositional logic that we consider in this article. However, compactability issues (i.e., the ability of representing the updated base as a propositional formula using a polynomial amount of space) make sense for our update operators and we investigated them. [START_REF] Eiter | Updating action domain descriptions[END_REF][START_REF] Eiter | Updating action domain descriptions[END_REF] address the problem of updating action descriptions represented in a fragment of the action language C. The framework they design is quite general: the updated action description can be required to include some causal laws and to imply some given integrity constraints; moreover, a preference relation over action descriptions is also taken into account. Their approach has flavors of both belief revision and belief update. [START_REF] Baral | Knowledge updates: Semantics and complexity issues[END_REF] consider the problem of updating a belief base expressed in the language of epistemic logic S5. They introduce an update operator based on the principle of minimal change and show that it satisfies the KM postulates (interpreted under the context of S5). In this setting, forgetting µ in ϕ consists in updating the latter with ¬Kµ ∧ ¬K¬µ, asserting that neither µ nor its negation is known to hold. [START_REF] Zhang | Knowledge forgetting: Properties and applications[END_REF] is closer to our work: in that paper, the authors study a notion of knowledge forgetting in S5 and consider, among other things, knowledge update as a possible application of knowledge forgetting. Their notion of knowledge forgetting is similar to the one at work in classical propositional logic (and different from the one considered in [START_REF] Baral | Knowledge updates: Semantics and complexity issues[END_REF]); indeed, forgetting a set of propositional variables in a formula ϕ amounts to computing the logically strongest consequence of ϕ that is independent from the set (i.e., there exists a equivalent formula in which no atom from the given set occurs). Zhang and Zhou define two update operators, the second being the model-wise version of the first. A significant difference with our dependence-based update operators is that the set of variables to be forgotten depends not only on the change formula µ but also on the knowledge base ϕ itself. Roughly, the models of the updated base are obtained by considering in all possible ways minimal sets of atoms (w.r.t. ⊆) such that forgetting them in ϕ leads to a formula consistent with µ. This is a way of implementing the principle of minimal change, and accordingly, the corresponding update operator satisfies (U2). [START_REF] Bienvenu | Knowledge compilation in the modal logic S5[END_REF] show how an S5 belief base can be progressed in polynomial time when it has been first compiled into a specific DNF form and the action description (which can refer to an ontic action or to an epistemic action) has been normalized as well. The notion of progression by an ontic action that is considered in their paper corresponds to an update operator following the "forget-then-conjoin" scheme that we follow in the present article. [START_REF] Nayak | Forgetting and knowledge update[END_REF] investigate an interesting relationship between literal forgetting and update: they show that Forbus' update operator [START_REF] Forbus | Introducing actions into qualitative simulation[END_REF]] and literal forgetting are inter-definable. This establishes an interesting connection between minimization-based and dependence-based approaches to belief update. Note that although our work also talks about literal forgetting and belief update, the nature of their work differs from ours, which aims at defining new update operators, based on formula/literal dependence, that can be computed via literal forgetting. [START_REF] Georgatos | Belief update using graphs[END_REF] introduces a form of update based on the minimization of the geodesic distance on a graph. The corresponding update operators correspond bijectively to geodesic metrics. Since such operators are based on minimization of change (and not on a "forget-then-conjoin" scheme), they are quite different from our update operators. Especially, Georgatos's operators satisfy (U2) while this is not the case for our operators in general.

Other Related Works

From a more applicative side, [START_REF] Hoffmann | Message-based web service composition, integrity constraints, and planning under uncertainty: A new connection[END_REF] use belief update for planning and web service composition and, following previous proposals in that direction, show that applying a web service is essentially a belief update operation. The authors introduce the decomposability postulate (D) that we considered previously (they call it (IV)). As in our approach, some integrity constraints are considered in their work. However, their update operator is based on change minimization, following Winslett's PMA.

CONCLUSION

In this article, we have proposed a new family of belief update operators that are based on dependence functions associating to every change formula µ the set of literals on which µ has a negative influence. We have shown that the family of KM update operators and the family of update operators based on formula/literal dependence are disjoint. We have identified the KM postulates our operators satisfy (and under which conditions), and we have studied their computational properties: complexity of model checking, satisfiability and inference, as well as compactability.

We have shown that update operators based on formula/literal dependence generalize those based on formula/variable dependence as defined in [START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Doherty | The PMA and relativizing change for action update[END_REF][START_REF] Herzig | The PMA revisited[END_REF][START_REF] Herzig | Propositional belief update and minimal change[END_REF] Interestingly, this is achieved without requiring a complexity shift w.r.t. operators based on formula/variable dependence. In particular, the inference problem for update operators based on formula/literal dependence is coNP-complete, just as the inference problem for Winslett's standard semantics (WSS), Hegner's operator (which is identical to Doherty et al.'s MPMA operator and to Herzig and Rifi's WSS↓), Herzig and Rifi's WSS δ v and WSS↓ δ v . Observe also that the other update operators of the literature that are not dependence-based all have higher complexity than ours; for instance, the inference problem for Winslett's PMA operator, Forbus' operator, Zhang and Foo's MCD operator ("minimal change with maximal disjunctive inclusion") and Zhang and Foo's MCE operator ("minimal change with exceptions", the update version of Weber's revision operator) is p 2 -complete [START_REF] Eiter | On the complexity of propositional knowledge base revision, updates, and counterfactuals[END_REF]Liberatore 2000a]. As to the update postulates, [START_REF] Herzig | Propositional belief update and minimal change[END_REF] criticized the KM rationality postulates for update; they show that (U1), (U3) and (U8) are uncontroversial, while (U4) is desirable, (U7) is neutral and (U2), (U5), and (U6) are undesirable. Notably, the most interesting of our update operators, those based on standard formula/literal dependence functions, conform to the desiderata: they satisfy (U1), (U3), and (U8), and those who are syntax-independent moreover satisfy (U4); none of them satisfies (U2), and (U5) and (U6) are not always satisfied.

This article calls for some perspectives for further research. First of all, it would be interesting to investigate other logical settings where update operators based on the "forget-then-conjoin" scheme could be defined. A key property for it is the ability of expressing in the language of the logic the result of forgetting some atoms in a formula. Indeed, while this is feasible in many logical settings, it is not always possible (for instance, this cannot be achieved in modal logic S4). On the other hand, in this article we have supposed that dependence functions are given. In future work we plan to investigate how they can be built automatically.

  refer the reader to[START_REF] Papadimitriou | Computational Complexity[END_REF] for the details. Let us recall that a decision problem is said to be at the kth level of PH if and only if it PH is then said to collapse to level i. It is strongly believed that PH does not collapse (to any level), that is, it is a truly infinite hierarchy: for every integer k, PH = p k .

Fig. 1 .

 1 Fig. 1. Update operators based on formula/variable dependence.

  Example 3.1. Let ω = {¬a, ¬b, c, d} and µ = (¬a ∧ b ∧ c) ∨ ((b ⇒ c) ∧ (c ⇒ b)), and let the dependence function between variables δ v be induced by r v = {(a, a), (a, b), (b, b),

  Example 3.10. Let ω = {powerOn, engineReady} and µ = powerOn ∨ engineReady. Using any formula/literal dependence function Dep such that Dep(powerOn ∨ engineReady) neither contains ¬powerOn nor ¬engineReady, we get ω ⋄ ⊤ Dep µ |= powerOn ∧ engineReady. The next result gives us a more practical way to compute ⋄ ϕ Dep . We first need to recall the notion of literal forgetting.

  It will be useful to consider two extreme cases of formula/literal dependence. Call full the formula/literal dependence function Dep f such that Dep f (µ) = Lit Var for every formula µ; and call empty the formula/literal dependence function Dep e such that Dep e (µ) = ∅ for every formula µ. PROPOSITION 3.15. Let Dep e be the empty formula/literal dependence function and let Dep f be the full formula/literal dependence function. Then

  PROPOSITION 4.1. No update operator ⋄ ⊤ Dep based on formula/literal dependence is a KM update operator. More precisely: (1) No update operator ⋄ ⊤ Dep based on formula/literal dependence satisfies both (U2) and (U3).

  hence this entailment can be the case only if ¬b ∈ Dep(a ∨ ¬b). (b) ψ 2 = ¬a ∧ ¬b. Since ψ 2 |= µ holds, we must have ∃ l Dep(a ∨ ¬b).(¬a ∧ ¬b) |= ¬(a ∨ ¬b) ∨ (¬a ∧ ¬b).

2 )

 2 It is easy to check that the update operator based on full formula/literal dependence (Dep f (µ) = Lit Var for every formula µ) satisfies all KM postulates but (U2).(We use that ψ ⋄ ⊤ Dep f µ is equivalent to µ if ψ isconsistent and is equivalent to ⊥ otherwise, cf. Proposition 3.15.) (3) It is also easy to check that the update operator based on empty formula/literal dependence (defined by Dep e (µ) = ∅ for every formula µ) satisfies all KM postulates but (U3). (We use that ψ ⋄ ⊤ Dep e µ equals ψ ∧ µ, cf. Proposition 3.15.) Now, Proposition 4.2 makes precise the KM postulates that are offered by every update operator based on formula/literal dependence. PROPOSITION 4.2. Update operators ⋄ ⊤ Dep based on formula/literal dependence satisfy the two postulates (U1) and (U8). The postulates (U2), (U3), (U4) 3 , (U5), (U6) and (U7) are not satisfied by update operators ⋄ ⊤ Dep in the general case. PROOF. (U1) Obvious from the definition of update operators based on formula/literal dependence. (U2) Not satisfied by MPMA [Doherty et al. 1998]. (U3) Let ψ = a, µ = ¬a and let Dep be such that ¬a ∈ Dep(µ) (e.g., Dep(µ) = ∅ for every µ); then ψ and µ are

PROPOSITION 4. 5 .

 5 Let Dep be a formula/literal dependence function and let ⋄ ⊤ Dep be the induced update operator. (1) If Dep is standard then ⋄ ⊤ Dep satisfies (U3). (2) If Dep is syntax-independent then ⋄ ⊤ Dep satisfies (U4). (3) If Dep is monotone then ⋄ ⊤ Dep satisfies (U5). (4) If Dep is constant then ⋄ ⊤ Dep satisfies (U6). (5) If Dep is antimonotone then ⋄ ⊤ Dep satisfies (U7).

  7. If Dep is a standard function then µ and ∃ l Dep(µ).ψ are Lit-separable, hence µ ∧ ∃ l Dep(µ).ψ |= ⊥ (where ⊥ is viewed as the empty clause) if and only if µ |= ⊥ or ∃ l Dep(µ).ψ |= ⊥. (2) Easy from the fact that ∃ l Dep(µ 1 ).ψ 1 ≡ ∃ l Dep(µ 2 ).ψ 2 when ψ 1 ≡ ψ 2 and Dep(µ 1 ) = Dep(µ 2 ). (3) The result easily comes from the fact that ∃ l Dep(µ).ψ |= ∃ l Dep(µ ∧ ϕ).ψ when Dep is monotone. (4) By definition, Dep is constant if and only if for any µ

  PROPOSITION 5.4. Let L ⊆ Lit Var , ψ a formula and γ a non-tautological clause. ∃ l L.ψ |= γ if and only if ψ |= l∈Lit(γ )\L l. PROOF. (⇒) If ∃ l L.ψ |= γ holds then since ∃ l L.ψ is Lit-independent of every literal of L, we have ∃ l L.ψ |= l∈Lit(γ )\L l. Since ψ |= ∃ l L.ψ also holds, we get that ψ |= l∈Lit(γ )\L l. (⇐) Assume that ψ |= l∈Lit(γ )\L l. Since the clause l∈Lit(γ )\L l is Lit-independent of every literal of L, Corollary 4 from Lang et al. [2003a] tells us that ψ |= l∈Lit(γ )\L l iff ∃ l L.ψ |= l∈Lit(γ )\L l. Since l∈Lit(γ )\L l |= γ holds, we obtain the expected conclusion.

  By construction, this formula is of size polynomial in |ϕ| + |µ| + |ψ|. Let us show that ψ ⋄ ϕ Dep µ is queryequivalent to . Let V = Var(ϕ)∪Var(µ)∪Var(ψ). We have to show that ∃V.(ψ ⋄ ϕ Dep µ) ≡ ∃V. . The formula ∃V.(ψ ⋄ ϕ Dep

PROPOSITION 5. 8 .

 8 If ψ is a Blake formula or a DNNF formula, then ψ ⋄ ϕ Dep µ can be turned into an equivalent propositional formula of polynomial size. Furthermore, if Dep is a polytime function, then such a formula can be computed in polynomial time. PROOF. Clearly enough, since Dep is a computable function, Dep(µ) can be computed in finite time (resp. in polynomial time if Dep is a polytime function).

-

  Conditional effects. If γ then update ψ by α else update ψ by β, denoted by ψ ⋄ with = if γ then α else β. -Nondeterminism. Update ψ by α or update ψ by β, denoted by ψ ⋄ with = α ∪ β. -Concurrency. Update ψ concurrently by α and by β, denoted by ψ ⋄ with = α || β.

  PROPOSITION 7.1. ⋄ Dep satisfies the Gricean property (GR) if and only if Dep satisfies the following property.(DG) for every consistent formula µ, Dep(µ) contains both RelVar(µ) and RelVar(µ).PROOF. Assume Dep satisfies (DG).Then for any consistent µ and ϕ, RelVar(∃ l Dep(µ).ϕ) ∩ RelVar(µ) = ∅, therefore ϕ ⋄ Dep µ ≡ ψ ∧ µ for some ψ such that RelVar(ψ) ∩ RelVar(µ) = ∅, which implies that ⋄ Dep satisfies the Gricean property.Conversely, assume that ⋄ Dep satisfies the Gricean property and let µ be a consistent formula and l a literal such that Var(l) ∈ RelVar(µ) and l ∈ Dep(µ). We have ¬l⋄ Dep µ = (∃ l Dep(µ).¬l) ∧ µ ≡ ¬l ∧ µ. Because ⋄ Dep satisfies the Gricean property we must have ∃Var \ RelVar(µ).(¬l ⋄ Dep µ) ≡ µ. This, together with Var(l) ∈ RelVar(µ), implies that ¬l ∧ µ ≡ µ, hence µ |= ¬l. Therefore, any literal l such that Var(l) ∈ Var(µ) and µ |= ¬l must be in Dep(µ). It remains to be shown that if Var(l) ∈ RelVar(µ) and µ |= ¬l then l must be in Dep(µ) as well. Towards a contradiction, suppose it is not. Let ϕ = ¬l. Since by assumption l ∈ Dep(µ), we have ∃ l Dep(µ).ϕ ≡ ¬l, hence ϕ ⋄ Dep µ = ¬l ∧ µ ≡ ⊥, contradicting the assumption that ⋄ Dep satisfies the Gricean property.[START_REF] Delgrande | Compositional belief update[END_REF] define a compositional update operator ⋄ C whose most distinctive feature is that update distributes over disjunction, that is, ϕ ⋄

  . We have also shown by means of examples that natural definitions of formula/literal dependence such as Dep = RelLit induce smaller change of the belief base than operators based on formula/variable dependence; for example (a ∧ b) ⋄ ⊤ Dep (a ∨ b) |= a ∧ b, while (a ∧ b) ⋄ ⊤ Dep v (a ∨ b) |= a ∨ b.

  and µ is Lit-independent of ¬x if and only if µ[x ← ⊥] |= µ[x ← ⊤]. Third, x ∈ RelVar(µ) if and only if ψ is Lit-dependent on x or on ¬x.

  Let us first consider the query-compactability issue.PROPOSITION 5.6. Let Dep be a formula/literal dependence function. Then ⋄ Dep is query-compactable.

	1) | | ≤ p(|ϕ| + |µ| + |ψ|), and (2) is logically equivalent to ψ ⋄ ϕ Dep µ.
	-Query compactability. ⋄ Dep is query-compactable if and only if there exists a poly-
	nomial p such that for every triple of propositional formulas ϕ, µ, ψ there exists a
	propositional formula such that:
	(1) | | ≤ p(|ϕ| + |µ| + |ψ|), and (2) is query-equivalent to ψ ⋄ ϕ Dep µ, i.e.,	and ψ ⋄ ϕ Dep µ have the same logical
	consequences over Var(ϕ) ∪ Var(µ) ∪ Var(ψ).

Note that however some authors question the suitability of change minimization even for belief revision; see for instance[Delgrande et al.

2005].

A weaker requirement is the following postulate that was introduced for belief revision by[START_REF] Parikh | Beliefs, belief revision, and splitting languages[END_REF] and further studied by other authors[START_REF] Bienvenu | Prime implicate-based belief revision operators[END_REF][START_REF] Kourousias | Parallel interpolation, splitting, and relevance in belief change[END_REF][START_REF] Makinson | Propositional relevance through letter-sharing: Review and contribution[END_REF]:(D ′ ) if Var(ϕ 1 ) ∩ Var(ϕ 2 ) = ∅ and Var(µ) ⊆ Var(ϕ 2 ) then (ϕ 1 ∧ ϕ 2 ) ⋄ µ ≡ ϕ 1 ∧ (ϕ 2 ⋄ µ).

ACKNOWLEDGMENTS

The authors would like to thank the anonymous reviewers for some helpful comments.

RelLit(µ 2 ) = Lit(µ 2 ) = {a}. Dep(µ 2 ) = {¬a} has to be forgotten in ψ. Hence, we have ψ ⋄ ⊤ Dep µ 2 ≡ a ∧ b, which implies µ 1 . However, ψ ⋄ ⊤ Dep µ 2 ≡ ψ ⋄ ⊤ Dep µ 1 ,and the conclusion follows.

Whether an update operator should satisfy (U2) or not depends on what update is meant to represent. Viewing an update by µ as the action of making µ true, (U2) should be satisfied whenever the action of making µ true should leave the world unchanged as soon as µ is already true (see, for instance, [START_REF] Lang | Belief update revisited[END_REF]). There are many situations where this should not be satisfied (see for instance in [START_REF] Herzig | Propositional belief update and minimal change[END_REF], Example 39, Remark 40, and the discussion after Theorem 31, which argue why (U2) should not be required in the general case). However, when (U2) is desirable, it is always possible to enforce it without hampering the other desirable properties (see [START_REF] Delgrande | Compositional belief update[END_REF]) just by defining the update operator ⋄ ′ associated with ⋄ by:

Explaining why (U5), (U6), and (U7) are not satisfied in the general case is more difficult, due to the technical nature of these postulates, whose role is to guarantee the existence of a collection of faithful preorders on the minimization of which the operator is defined. Therefore, it is not easy to go beyond the explanation that these postulates are not satisfied in the general case because dependence-based operators are not based on minimization.

COMPUTATIONAL ASPECTS

We consider now a number of complexity issues for update operators based on formula/literal dependence. Some results hold for the whole family of operators, and others for some subsets that are obtained by imposing restrictions on Dep. We also consider some compactability issues.

The Model Checking Problem

We first investigate the complexity of the model checking problem from an updated base. The model checking problem for ⋄ Dep is as follows: given three formulas ϕ, ψ, µ and a world ω, how difficult is it to determine whether ω |= ψ ⋄ PROOF. Membership. If determining whether l ∈ Dep(µ) is in NP, then determining whether any given set L ⊆ Lit Var of literals is included in Dep(µ) is in NP as well. Hence for every positive instance L, µ of this decision problem, there exists a certificate c of size polynomial in the input size such that verifying that L, µ is a positive instance can be achieved in (deterministic) polynomial time when c is given. Let V = Var(ψ) ∪ Var(ϕ) ∪ Var(µ). The problem can be solved in nondeterministic polynomial time, thanks to the following algorithm: guess a world ω ′ over V, a subset L of V ∪ V and a string c (both of them being of polynomial size in the input size), then check in polynomial time that L ⊆ Dep(µ) using c, and check that ω |= ψ, ω ′ |= µ ∧ ϕ and ω = (ω ′ \ L) ∪ L.

Hardness. The reduction from SAT is as follows: to ψ ∈ FML Var , we associate in polynomial time the formulas ϕ = ⊤ and

where y and z are fresh variables not occurring in ψ. Let ω = Var. By construction, we have RelLit(ψ) ⊆ RelLit(µ). We have that ψ is consistent if and only if ω |= ψ ⋄ ϕ Dep µ holds; indeed, ∃ l RelLit(µ).ψ is valid if ψ is consistent, and ∃ l RelLit(µ).ψ is inconsistent otherwise.

There are special cases where NP-hardness does not hold. Suppose, for instance, Dep is both monotone and antimonotone. Then Dep(µ) = ∅, and ψ

which is the model checking problem in propositional logic (which is well-known to be decidable in deterministic polynomial time).

Moreover, it could be the case that hardness is due only to the fact that the knowledge base ψ may be inconsistent. If the knowledge based is required to be consistent, which is a reasonable assumption, then this hardness result no longer holds. Consider for instance the full dependence function defined by Dep(µ) = Lit Var for any µ. As we have seen in Proposition 3.15, if ψ is consistent then ψ ⋄ Dep µ ≡ µ and ψ ⋄ Dep µ ≡ ⊥ otherwise. Note that Dep is standard. Clearly, if ψ is required to be consistent then ψ ⋄ Dep v µ ≡ µ and model checking is obviously polynomial in this case.

Tractable cases can be obtained by restricting the input so that ∃ l Dep(µ).ψ can be computed in time polynomial in the input size. Such restrictions are discussed in Section 5.4.

The Consistency Problem

We now investigate the complexity of the consistency problem for an updated base when operators based on formula/literal dependence are used. The problem is as follows: given three formulas ϕ, ψ, µ how difficult is it to determine whether ψ ⋄ ϕ Dep µ is consistent? PROPOSITION 5.2. Let Dep be a formula/literal dependence function such that for any l ∈ Lit Var and µ ∈ FML Var , determining whether l ∈ Dep(µ) is in NP. Given three formulas ϕ, ψ, and µ, determining whether ψ ⋄ ϕ Dep µ is consistent is NP-complete, even if ϕ is valid (no integrity constraints) and the input formula µ is an atom. PROOF. Membership. It is close to the membership proof of Proposition 5.1. The consistency problem can be solved in nondeterministic polynomial time, thanks to the following algorithm: let V = Var(ψ) ∪ Var(µ) ∪ Var(ϕ); guess two worlds ω, ω ′ over V, a set of literals L of V ∪ V and a string c (both of them being of polynomial size if the input size), then check in polynomial time that L ⊆ Dep(µ) using c, and check that ω |= ψ, ω ′ |= ϕ ∧ µ and ω ′ = (ω ′ \ L) ∪ L.

Hardness. The reduction from SAT is as follows: to ψ ∈ FML Var , we associate in polynomial time the formulas ϕ = ⊤ and µ = y where y is a fresh variable not occurring in ψ. Then ψ ⋄ ϕ Dep µ ≡ y ∧ ϕ ∧ ∃ l Dep(µ).ψ is consistent iff ∃ l Dep(µ).ψ is consistent (the right-to-left direction holds just because y is fresh) iff ψ is consistent. (Observe that for any L ⊆ Lit Var , ∃ l L.ψ is consistent iff ψ is consistent.)