Belief Revision and Progression of Knowledge Bases in the Epistemic Situation Calculus

1 Introduction

Fundamental to reasoning about actions and beliefs is the projection problem: to decide what is believed after a sequence of actions is performed. There are two popular ways to solve this problem: regression rewrites a query about the future to a query about the initial situation only; progression changes the knowledge base to reflect the effects of the actions. Regression usually becomes infeasible when dealing with very long action sequences. A long-lived system-for instance, a domestic service robot-hence must progress its mental state once in a while. In particular, such a robot may continually acquire new information about its environment, which may or may not be consistent with what the robot believed or had learned before. When progressing its knowledge base, the robot needs to carefully revise its beliefs to handle these potentially conflicting pieces of information.

The following running example will illustrate our approach. Suppose our robot is carrying an object which it believes to be quite robust but not made of metal. Hence, when the robot drops the item, it believes the object is still intact. When a clinking noise occurs afterwards, perhaps indicating that the object is broken or is made of metal, this may change; as the robot considers fragility more plausible than the object

Maurice Pagnucco

University of New South Wales

Sydney, Australia

morri@cse.unsw.edu.au

being metallic, it now believes that the object is broken. If then the robot inspects the object and it turns out to be fine after all, the previous belief is given up again and the robot assumes the object neither broken nor metallic (implicitly assuming the clink was due to something else).

Progression is a very intuitive way to implement projection. It has attracted a lot of attention in the reasoning about action community, perhaps most notably in the seminal work by Lin and Reiter [Lin and Reiter, 1997] in the situation calculus [McCarthy, 1963; Reiter, 2001]. While Lin-Reiter progression has been transferred to one of the epistemic extensions of the situation calculus [Lakemeyer and Levesque, 2009], it has not yet been studied in any of the situation calculus dialects that deal with belief change. In fact, most variants of the situation calculus take the Scherl-Levesque view of sensing [Scherl and Levesque, 2003], where sensing is assumed to be correct and thus cannot be revised at all.

In this paper, we propose a logical framework where the robot's preferential belief structure is modelled using counterfactual conditionals. Sensing tells the agent new information, which may turn out wrong later and then becomes subject to belief revision. We propose a solution to the projection problem in this setting by belief progression. More precisely, we show that, by using the concepts of natural revision [Boutilier, 1993] and only-believing [Schwering and Lakemeyer, 2014], the progression of a conditional knowledge base can be represented by only-believing the revised set of conditional statements. The connection to only-believing is particularly attractive due to its unique-model property, which lays the foundations for feasible belief progression.

The next section discusses approaches related to our proposal here. In Section 3 we introduce our new logic, before we define Reiter's concept of basic action theories in this framework and examine our running example in Section 4. Section 5 presents the main result of this paper: how to revise and progress a conditional knowledge base. In Section 6 we compare our work with standard belief revision frameworks before concluding.

2 RelatedWork

The situation calculus is perhaps the most thoroughly studied action formalism, although there are other significant approaches such as the event calculus [Kowalski and Sergot,

1989], the fluent calculus [Thielscher, 1999], and the family of action languages A [Gelfond and Lifschitz, 1993]. A number of belief revision extensions of the situation calculus have been proposed [Shapiro et al., 2011; Demolombe and Pozos Parra, 2006; Delgrande and Levesque, 2012; Fang and Liu, 2013; Schwering and Lakemeyer, 2014]. Most of these do not address the issue of faulty sensors with the exception of [Delgrande and Levesque, 2012; Fang and Liu, 2013], who both achieve this through plausibility updating schemes. However, these formalisms are quite heavyweight and leave open the projection problem which we claim is the key to implementation. The only available solution to the belief projection problem is by regression [Schwering and Lakemeyer, 2015], but it assumes correct sensors. Another framework to deal with faulty sensors is the Bayesian approach by [Bacchus et al., 1999].

Belief revision has also been addressed in dynamic epistemic logic [van Benthem, 2007], where revised beliefs are reduced to initial beliefs in a regression-like fashion.

We use Boutilier's natural revision [Boutilier, 1993]. While several plausibility updating schemes have been proposed, for example [Spohn, 1988; Nayak et al., 2003], and despite legitimate criticism [Booth and Meyer, 2006], we choose natural revision because, as we shall see later, it agrees well with only-believing. Only-believing [Schwering and Lakemeyer, 2014] determines a unique epistemic model for a conditional knowledge base. It is related to only-knowing [Levesque and Lakemeyer, 2001] and System Z [Pearl, 1990].

Progression was first studied by Lin and Reiter in the situation calculus [Lin and Reiter, 1997]. Roughly speaking, their idea is to progress a knowledge base by replacing all relevant predicates with existentially quantified second-order variables. Their purpose is to "memorize" what was true before the progression. The original predicates are then reintroduced and equated with a formula about the secondorder variables only. We will re-visit this idea in Section 5.

3 The Logic

In this section we introduce a novel logic that combines reasoning about action and belief revision. This first-order modal language is a variant of ES [Lakemeyer and Levesque, 2011]. Actions may lead to a revision of the agent's beliefs, which follows the rules of natural revision [Boutilier, 1993]. It also integrates an operator, called only-believing [Schwering and Lakemeyer, 2014], which uniquely determines the agent's beliefs for a given conditional knowledge base.

3.1 The Language

The language consists of formulas over fluent or rigid predicates and rigid terms. The truth value of fluents may vary as the result of actions, but rigids do not.

The set of terms is the least set which contains infinitely many first-order variables and is closed under the application of infinitely many function symbols of any arity.

The set of well-formed formulas is the least set that contains H(t1, . . . , tk), (t1 = t2), ¬α, (α ∧ β), ∀x.α, [t]α, □α, Bα, and O(α, {φ1 ⇒ ψ1, . . . , φm ⇒ ψm}), where H is a k-ary predicate symbol, ti and t are terms, x is a variable, and

α, β, φi, ψi are formulas. TRUE, FALSE, (α ∨ β), (α ⊃ β), (α ≡ β), and ∃x.α are the usual abbrevations.

We read [t]α as "α holds after action t" and □α as "α holds after any sequence of actions." Bα is read as "α is believed." Conditionals φ ⇒ ψ are understood counterfactually [Lewis, 1973]: "if φ was true, then ψ would be true." The only-believing operator O(α, {φ1 ⇒ ψ1, . . . , φm ⇒ ψm}) means that α is known, the conditionals φi ⇒ ψi are believed, and this is all that is known or believed. The purpose of only-believing is to uniquely determine a belief structure.

There are two special fluent predicates: Poss(t) represents the precondition of action t; IF(t) represents the new information learned by the agent through action t.

By αx t we mean the formula α with t substituted for all free occurrences of x. We sometimes write ⃗t for t1, . . . , tk.

A formula with no [t] or □ is called static. A formula with no B or O is called objective. A formula with no free variable is called a sentence.

3.2 The Semantics

We now give a possible-worlds semantics for this language. An interpretation of a sentence α consists of an epistemic state f, a world w, and a sequence of executed actions z. We write f,w, z |= α to say that the interpretation satisfies the sentence. We take as fixed in the domain of discourse the set of all ground terms denoted by R. Since R is countable, we can handle quantification by substitution. By R∗ we denote the set of all sequences of ground terms, including the empty sequence 〈〉. The action sequence z initially starts with 〈〉 and then grows deterministically with each executed action r to z · r. A world w maps all atomic sentences H(r1, . . . , rk) and action sequences z ∈ R∗ to truth values {0, 1}, and satisfies the rigidity constraint: if H is rigid, then w[H(r1, . . . , rk), z] = w[H(r1, . . . , rk), z′ ] for all z, z′ ∈ R∗ . An epistemic state f maps each plausibility (taken from N) to a set of worlds considered possible at this plausibility level. A value of 0 indicates the highest possible plausibility. A world may occur at multiple plausibility levels; usually we will indeed have f(0) ⊆ f(1) ⊆ . . ., that is, f(p) contains all worlds at least as plausible as p.

We begin with the objective semantics:

1. f,w, z |=H(r1, . . . , rk) iff w[H(r1, . . . , rk), z] = 1;
2. f,w, z |= (r1 = r2) iff r1 and r2 are identical;
3. f,w, z |= ¬α iff f,w, z ̸|= α;
4. f,w, z |= (α∧ β) iff f,w, z |= α and f,w, z |= β;
5. f,w, z |= ∀x.α iff f,w, z |= αx r for all r ∈ R;
6. f,w, z |= [r]α iff f,w, z · r |= α;

Before we proceed with the semantics of beliefs, we need to formalize the revision of an epistemic state. When the agent is informed that α holds, we promote the most plausible α-worlds to the highest plausibility level and shift all other worlds down by one level. This revision scheme is known as natural revision [Boutilier, 1993]. Intuitively, it is the minimal change required of the plausibility ordering to ensure belief in α. We denote the result of this revision by f ∗ α:

Definition 1 Given an epistemic state f and a sentence α, let p∗ = min{p | f,w, 〈〉 |= α for some w ∈ f(p)} ∪ {∞} be the first plausibility level 1 consistent with α and let W = {w | w ∈ f(p∗ ) and f, w, 〈〉 |= α} be the α-worlds from that level. For convenience, we let f(-1) stand for {}. Then the revision of f by α is denoted by f ∗ α and is defined as:

• if p∗ = ∞ then (f ∗ α)(p) = {} for all p ∈ N;
• if W ̸= f(p∗ ) \ f(p∗ -1) then

- (f ∗ α)(p) = f(p-1) ∪W for all 0 ≤ p ≤ p∗ ;

- (f ∗ α)(p) = f(p-1)

for all p > p∗ ;

• otherwise

The plausibility of a world w is the minimal p such that w ∈ f(p). In f ∗ α, the most plausible α-worlds from f are shifted to the first plausibility level. All other worlds are made less plausible by one level. The second and third case only differ in that the latter skips f(p∗ ) to avoid (f ∗α)(p∗ ) = (f ∗ α)(p∗ + 1) when f (p∗ - 1) ∪ W = f (p∗ ).

Any action r provides the agent with the (perhaps vacuously true) information that IF(r) holds. We therefore account for r in the epistemic state by revising by IF(r) and then applying the effects of r to all worlds in f:

Definition 2 The progression of a world w by z is a world wz such that wz[ρ, z′ ] = w[ρ, z · z′ ] for all atomic sentences ρ and action sequences z′ . The progression of an epistemic state f is denoted by fz and is defined inductively by

• f〈〉 = f;
• fz·r(p) = {wr | w ∈ (fz ∗ IF(r))(p)} for all p ∈ N.

With these definitions in hand, we are ready to proceed with the epistemic semantics:

1. f,w, z |=Bα iff fz,w′ , 〈〉 |= α for all w′ ∈ fz(0);

• (a) fz,w′ , 〈〉 |= (α∧ ∧i:pi≥p (φi ⊃ ψi)) iff w′ ∈ fz(p);
• (b) for all pi > p, for all w′ ∈ fz(p), fz,w′ , 〈〉 ̸|= φi;
• (c) for all pi = p, for some w′ ∈ fz(p), fz,w′ , 〈〉 |= φi.

In the following, we sometimes omit f or w in f, w, z |= α when it is irrelevant to the truth of α. We also may omit z when z = 〈〉. A set of sentences Σ entails a sentence α iff for all f and w, if f,w |= β for all β ∈ Σ, then f,w |= α. We write Σ |= α, and abbreviate |= α when Σ = {}.

3.3 Some Properties

Since f〈〉 = f, our definition of only-believing is identical with the one in [Schwering and Lakemeyer, 2014] when z = 〈〉. Therefore the following theorem carries over to our logic: Theorem 3 ([Schwering and Lakemeyer, 2014]) Let Γ = {φ1 ⇒ ψ1, . . . , φm ⇒ ψm} and let α, φi, ψi be objective. Then there is a unique f such that f |= O(α, Γ).

1 In Definition 1, p∗ = ∞ means that all plausibility levels are inconsistent with α. In Rule 9, pi = ∞ analogously indicates that all plausibility levels are inconsistent with the antecedent φi.

In fact, the following straightforward procedure generates the epistemic state that satisfies O(α, Γ) [Schwering and Lakemeyer, 2014]. Initially let p1 := 0, . . . , pm := 0. Then let p run from 0 to m and repeat the following two steps:

• Let f(p) := {w | w |= (α ∧ ∧i:pi≥p (φi ⊃ ψi))}.
• For all i, if there is no w ∈ f(p) such that w |= φi, let pi := p+1.

Then let f(p) := f(m) for all p > m. Finally let pi := ∞ for all pi > m. Then f |= O(α, Γ) for the plausibilities p1, . . . , pm. Observe that then f(0) ⊆ f(1) ⊆ . . . holds.

Since our objective semantics is the same as the one for ES [Lakemeyer and Levesque, 2004], its theorems carry over to our logic:

Theorem 4 Let |=ES denote the entailment relation of ES. For any objective sentence α, |= α iff |=ES α.

This correspondence does not hold for knowledge or belief because our notion of informing differs from the sensing concept predominant in the situation calculus: ES and its descendents, including the belief revision variant [Schwering and Lakemeyer, 2014], follow Scherl and Levesque [Scherl and Levesque, 2003] and define sensing to be always correct-a strong assumption we do not make here. We hence resort to the weaker concept of informing where new information may contradict older information.

4 Basic Action Theories

To axiomatize a dynamic domain we use the modal variant of Reiter's basic action theories [Reiter, 2001; Lakemeyer and Levesque, 2011]. A basic action theory over a finite set of fluent predicates F consists of a static and a dynamic part. In the context of a basic action theory a formula is called fluent when it is objective, static, and all predicates are either from F or rigid.

The dynamic axioms express when an action is executable (Σpre), how actions change the truth values of fluents (Σpost), and which belief actions produce (Σinfo): 2

• Σpre contains a single sentence □Poss(a) ≡ π where π is a fluent formula;
• Σpost contains a sentence □[a]F(⃗x) ≡ γF for all F ∈ F where γF is a fluent formula;
• Σinfo contains a single sentence □IF(a) ≡ ϕ where ϕ is a fluent formula.

The sentences in Σpost are called successor state axioms because they relate the state after an action a to the one before a. They incorporate Reiter's solution to the frame problem [Reiter, 2001]. The informed fluent axiomΣinfo is to axiomatize the information an action tells the agent. We refer to the dynamic axioms as Σdyn.

The static part of a basic action theory expresses what the agent believes to be true: Σbel contains finitely many belief conditionals φ ⇒ ψ where φ and ψ are fluent sentences.

2 We assume □ has lower and [t] has higher precedence than logical connectives and that all first-order variables are quantified from outside. So □[a]F(⃗x) ≡ γF stands for ∀a.∀⃗x.□(([a]F(⃗x)) ≡ γF ).

The projection problem in this setting is to decide if O(Σdyn,Σbel) |= α holds, 3 where α may involve actions and/or beliefs. In the next section we present a solution to the projection problem by progression, which modifies the initial beliefs to take into account the actions' effects.

Example

The example from Section 1 can be modelled as a basic action theory as follows. There are two rigid predicates, F and M, for the object being fragile or metallic, respectively. There is one fluent predicate, B, which indicates whether or not the object is broken. The action drop 4 causes the object to break if it is fragile. The clinking noise is represented by the action clink, which informs that the object is broken or metallic (B ∨ M). Lastly, the inspect action tells us that the object is not broken (¬B). We do not model any preconditions for simplicity. This translates to the following dynamic axioms:

The robot believes that the object is neither fragile nor metal, and it generally considers it more likely that the object is fragile than being metal. Furthermore we are absolutely certain that the object is not broken in the beginning. Thus we have:

Notice that the effect of B ⇒ FALSE is to assert ¬B at all plausibility levels. We will now examine how belief changes after dropping the object, hearing a clink, and inspecting the object.

After dropping the object, we believe it to be still intact, that is, O(Σdyn,Σbel) |= [drop]B(¬B ∧ ¬F ∧ ¬M). This is because drop triggers no revision and hence:

When we hear a clink after dropping the object, the revision by IF(clink) promotes the most plausible (B ∨ M)- worlds to the first plaubility level. The first (B ∨M)-worlds come from fdrop(1), namely those w ∈ fdrop(1) with w |= F . Hence we have:

3 We identify a finite set of sentences with their conjunction.

4 We use sans-serif font for ground terms.

Since for all w ∈ fdrop·clink(0), w |= B ∧ F ∧ ¬M , we have O(Σdyn, Σbel) |= [drop][clink]B(B ∧ F ∧ ¬M ).

When we now inspect the object, we revise by IF (inspect), which promotes the first ¬B-worlds from fdrop·clink to the first plausibility level. The first ¬B-worlds come from fdrop·clink(1), namely those w ∈ fdrop·clink(1) with w |= ¬F. For z = drop · clink · inspect we hence have:

Observe that the revision by IF(inspect) undoes the previous revision by IF(clink), that is, fz = fdrop, and thus: O(Σdyn, Σbel) |= [drop][clink][inspect]B(¬B ∧ ¬F ∧ ¬M). In particular, we believe the object is not metallic, due to natural revision. In approaches where sensing is assumed to be correct, like [Shapiro et al., 2011; Schwering and Lakemeyer, 2014], such a conclusion would not have been possible because they would have ruled out all worlds contradicting (B ∨M) and ¬B, so only M-worlds would be left.

5 Progression

In this section we present a form of progression which captures the beliefs after an action using only-believing. We need to take into account both the epistemic revision effect of the action and its physical effects. To this end, we first define revision of only-believing and show its correctness with respect to the semantics (Definition 5 and Theorem 6). Then we integrate the physical effects of actions to obtain a form of progression of basic action theories (Definition 7 and Theorem 8).

Definition 5 Let Γ = {φ1 ⇒ ψ1, . . . , φm ⇒ ψm} and let α, β, φi, ψi be objective. Let f be the epistemic state such that f |= O(α, Γ) for plausibilities p1, . . . , pm. Let

Then the revision of O(α, Γ) by β is denoted by O(α, Γ) ∗ β and defined as O(α, Γ′ ) where

O(α, Γ)∗β thus means to believe β, but if β turns out to be wrong, we return to the old beliefs φi ∧¬β ⇒ ψi. The conditional ¬δ ⇒ γp∗ ensures that when also all φi∧¬β ⇒ ψi turn out to be wrong, we return to the same beliefs as before the revision. Intuitively, a world satisfies δ if before the revision its plausibility was at least p∗ - 1 or if its plausibility was p∗ and it satisfies β. (The different definitions for δ handle cases where plausibility levels concur.) Therefore, ¬δ ⇒ γp∗ means that if β and everything we considered at least as plausible as p∗ - 1 before the revision turn out to be wrong, then after the revision we believe the same as before the revision if β and all beliefs at least as plausible as p∗ - 1 had turned out to be wrong. Notice that O(α, Γ) ∗ β can be generated using first-order reasoning.

We now prove that this revision matches natural revision that is used in the semantics:

Proof Sketch. The proof is lengthy, so we sketch the main idea. The idea is to show that f ∗ β satisfies the right-hand side of Rule 9 for the following plausibilities. For TRUE ⇒ β, the plausibility is 0. For each φi ∧ ¬β ⇒ ψi, the plausibility is pi + 1. For each φi ⇒ ψi, the plausibility is 0 if pi = p∗ and w |= φi ∧β for some w ∈ f(p∗ ); it is pi +1 if w ̸|= β for some w ∈ f(p∗ )\f(p∗ -1); and pi otherwise. For ¬δ ⇒ γp∗ , the plausibility is p∗ + 1 if γp∗ ∧ ¬γp∗-1 ̸|= β; p∗ otherwise. It is then tedious but straightforward to show that Rule 9 is satisfied. Crucial for this is that |= (¬δ ⊃ γp∗) ≡ γp∗, which allows to rearrange the conditionals from level p∗ because ¬δ ⇒ γp∗ takes their place.

We are now ready to define the progression of a basic action theory with conditional beliefs O(Σdyn,Σbel). Given an action r, we first revise the theory by IF(r) and then handle the effects of r on the fluents. The revision is captured by O(Σdyn, Σbel) ∗ ϕar where ϕ is the informed fluent axiom (□IF(a) ≡ ϕ ∈ Σdyn). (The reason for taking ϕar instead of IF(r) is to keep the belief conditionals fluent.) In the following we show how to handle the physical effect of r. Let the set of fluents be F = {F1, . . . , Fn} and let P = {P1, . . . , Pn} be rigid predicates of corresponding arity which do not otherwise occur in O(Σdyn, Σbel). We denote by α ⃗ F⃗ P the formula obtained from replacing each Fi with Pi. The progression of a basic action theory is then defined as follows:

Definition 7 Let Σ′bel be the revised belief conditionals, that is, O(Σdyn,Σbel) ∗ ϕar = O(Σdyn,Σ′bel ). The progression of O(Σdyn,Σbel) by r is then denoted by O(Σdyn,Σbel)r and is defined as O(Σdyn, Σ′′ bel ) where

The intuition behind the definition is as follows. Each new predicate Pi captures the pre-r truth value of Fi. Now, when an action r is executed, we first revise by the information ϕar produced by r which gives us the new beliefs Σ′bel . The beliefs Σ′bel ⃗ F⃗ P represent the same belief structure as Σ′bel , except that each Fi is renamed to Pi. Adding a conditional ¬(∀⃗x.F(⃗x) ≡ γF ar ⃗ F⃗ P ) ⇒ FALSE finally has the effect of requiring ∀x.F(⃗x) ≡ γF ar ⃗ F⃗ P at every plausibility level, which leads to F taking the correct post-r value. Note that the revision of a basic action theory again is a basic action theory.

We say α is P-free if no predicate in α is from P. The following theorem establishes the correctness of progression:

Proof Sketch. The proof proceeds in two steps. Firstly, it is shown that O(Σdyn,Σ′bel ) and O(Σdyn,Σ′′ bel ) (as defined in Definition 7) lead to the same belief structure. Intuitively, this is because in O(Σdyn, Σ′′ bel ) each Fi is renamed by Pi, so the additional conditionals in Σ′′ bel do not affect the plausibilities. Secondly, if f |=O(Σdyn,Σ′bel ) and g |=O(Σdyn,Σ′′ bel ), then f and g are bisimilar in the sense that for all p, for each w ∈ f(p), there is some w′ ∈ g(p) such that wr and w′ agree on all truth values except for the predicates from P, and viceversa. Then one can show by induction that any two states bisimilar in this sense satisfy the same P-free sentences.

Our definition of progression is closely related to Lin and Reiter's progression [Lin and Reiter, 1997]. While they use existentially quantified second-order variables to memorize the pre-r truth value of each Fi, we use new rigid Skolempredicates Pi. This is weaker than Lin-Reiter progression in the sense that O(Σdyn,Σbel) ̸|= [r]O(Σbel,Σdyn)r. However, second-order logic would have led to a considerably more complex definition of the O operator.

Example

We now examine the progression of O(Σdyn,Σbel) by drop and then by clink. The epistemic states we obtain match the ones from Section 4 except for the newly added predicate PB to memorize the old value of B.

We first consider the progression by drop. As the revision by ϕadrop just adds another conditional to O(Σdyn, Σbel)∗ϕadrop whose antecedent and consequent both are equivalent to TRUE, we proceed with the progression of the physical effects. By Definition 7, the resulting conditionals are:

Observe that the only difference between fdrop from Section 4 and g is the additional restrictions on PB, and hence both epistemic states satisfy the same formulas without PB.

Let us now consider O(Σdyn,Σ′bel )clink, which leads to a revision by (B ∨M). Since clink has no physical effect, we only examine this revision and omit the progression. The first plausibility level from g consistent with (B ∨M) is p∗ = 1. Since there is no w ∈ g(1) \ g(0) such that w ̸|= (B ∨M), the additional constraint ¬δ ⇒ γp∗ is such that:

Hence we obtain as the revised set of beliefs:

This syntactic revision satisfies the same PB-free formulas as fdrop·clink from Section 4: we have g′ |= O(Σdyn,Σ′bel ) iff g′ (p) = {w | w |= λp} where:

Note that λ0 is inconsistent with ¬δ but λ1 is not, so ¬δ ⇒ γp∗ is satisfied at g′ (1) and has the effect of asserting ¬M.

6 AGM, DP, and NPP Postulates

In this section we relate our framework to the most well known accounts of belief change: AGM [Alchourron et al., 1985; G¨ardenfors, 1988], DP [Darwiche and Pearl, 1997], and NPP [Nayak et al., 2003]. We will see that all the AGM postulates and a slight modification of the DP postulates hold, whereas the NPP postulates are not satisfied.

An action r is called a revision action when it has no physical effect, that is, Σdyn |= □[r]F(⃗x) ≡ F(⃗x) for all F ∈ F. The only effect of such a revision action r is the belief revision by IF(r). Since it is equivalent, and to ease the presentation, we consider in the following just the revision instead of progression of O by a revision action r.

For the rest of this section, let Σ = O(Σdyn,Σbel) and let β, γ, δ be P-free fluent sentences. In the following results, we have translated the relevant postulates into our formalism (similarly as in [Shapiro et al., 2011]).

Theorem 9 The AGM postulates hold:

1. Σ ∗ β is deductively closed.
2. Σ ∗ β |=Bβ.
3. If Σ ∗ β |=Bδ, then Σ |=B(β ⊃ δ).
4. If Σ ̸|=B¬δ and Σ |=B(β ⊃ δ), then Σ ∗ β |=Bδ.
5. If Σ ̸|=BFALSE and ̸|= ¬β, then Σ ∗ β ̸|=BFALSE.
6. If |= β ≡ γ, then |= Σ ∗ β ≡ Σ ∗ γ.
7. If Σ ∗ (β ∧ γ) |=Bδ, then Σ ∗ β |=B(γ ⊃ δ).
8. If Σ ∗ β ̸|=B¬γ and Σ ∗ β |=B(γ ⊃ δ), then Σ ∗ (β ∧ γ) |= Bδ.

Proof. The proofs are straightforward. Here we only show Postulate 8: suppose f |= Σ and the antecedent holds. Then for some w ∈ (f ∗ β)(0), w |= γ, and for all w ∈ (f ∗ β)(0), w |= γ ⊃ δ. Therefore (f ∗β ∧γ)(0) ⊆ (f ∗β)(0). Since for all w ∈ (f ∗ β ∧ γ)(0), w |= γ, by assumption w |= δ.

While our main interest here is not in physical actions, it can be noted that the KM update postulates [Katsuno and Mendelzon, 1991] hold with the exception of Postulates 3, 6, and 7 for the reasons noted by [Shapiro et al., 2011].

As for the DP postulates for iterated revision, we need to add the requirement β ̸|= γ to the antecedent of DP2 because we cannot recover from revision by an unsatisfiable formula.

Theorem 10 The DP postulates hold with a restricted version of the second postulate:

1. If γ |= β, then (Σ ∗ β) ∗ γ |=Bδ iff Σ ∗ γ |=Bδ.
2. If β |= ¬γ and β ̸|= γ, then (Σ ∗ β) ∗ γ |= Bδ iff Σ ∗ γ |= Bδ.
3. If Σ ∗ γ |=Bβ, then (Σ ∗ β) ∗ γ |=Bβ.
4. If Σ ∗ γ ̸|=B¬β, then (Σ ∗ β) ∗ γ ̸|=B¬β.

Proof. Again the proofs are reasonably straightforward, so we only show Postulate 3 here: suppose f |= Σ and the antecedent holds. If for some w ∈ (f ∗ β)(0), w |= γ, then {} ̸= ((f ∗ β) ∗ γ)(0) ⊆ (f ∗ β)(0) and therefore for all w ∈ ((f ∗ β) ∗ γ)(0), w |= β. Otherwise, for all w with w |= γ, w ∈ f(p) ∪ (f ∗ β)(0) iff w ∈ f(p). Therefore (f ∗ γ)(0) = ((f ∗ β) ∗ γ)(0).

The NPP postulates, however, are not satisfied. This is because natural revision is inconsistent with the third postulate:

1. If ̸|= ¬(β∧γ) then (Σ∗β)∗γ |=Bδ iff Σ∗(β∧γ) |=Bδ. Consider our running example: after revising by (B∨M) and then by ¬B, we believe that ¬M, whereas after revising by (B ∨ M ) ∧ ¬B we would believe M .

7 Conclusion

We have developed a logic for reasoning about actions and belief revision. In particular, our approach is able to revise inconsistent sensing information by natural revision. We showed that this formalism is in line with the AGM and DP postulates, but not with the NPP postulates. Most importantly, however, we addressed the belief projection problem by progression: we showed that, if the agent only-believes a conditional knowledge base before an action, then they onlybelieve another conditional knowledge base after the action.

The next step is to employ this notion of progression in feasible subclasses of the situation calculus such as [Liu and Lakemeyer, 2009]. We then aim to integrate our work with an existing implementation of a limited reasoner about actions and knowledge based on [Lakemeyer and Levesque, 2014].

Acknowledgments

We thank the anonymous reviewers for helpful comments and pointers to related work. This work was partially supported by the DAAD Go8 project 56266625 and by the DFG research unit FOR 1513. The first author was supported by a DAAD doctoral scholarship.