On the Progression of Knowledge in the Situation Calculus

1 Introduction

In a seminal paper, Lin and Reiter [1997] introduced the notion of progression for basic action theories in the situation calculus. Roughly, progression concerns updating the representation of the current world state after an action is executed. Lin and Reiter showed that progression is not first-order (FO) definable in general, and identified two simple cases where progression is first-order definable and computable. They also conjectured that there is no alternative definition of progression that is always first-order definable. The conjecture was resolved by Vassos and Levesque [2008].

However, knowledge was not taken into account in Lin and Reiter's study of progression. To motivate progression of knowledge, consider the litmus testing example from [Moore, 1985]. Suppose there is an initial representation describing that the solution is acid and the agent knows the paper is not red. After the agent performs a litmus test on the solution, how should we update the representation to reflect the change to the world state and the agent's knowledge

Ximing Wen1,2

1Dept. of Computer Science Sun Yat-sen University 2Guangdong Institute of Public Administration Guangzhou 510006, China wenxim@student.sysu.edu.cn

state? Intuitively, the new representation should entail that the agent knows the solution is acid. Moore [1985] adapted the possible-world model of knowledge to the situation calculus by introducing a special fluent K(s′ , s), meaning that situation s′ is accessible from situation s. Later, Scherl and Levesque [2003] proposed a solution to the frame problem for knowledge-producing actions by giving a successor state axiom for the K fluent.

Recently, Liu and Lakemeyer [2009] showed that for the so-called local-effect actions, progression is always firstorder definable and computable. Their proof is a very simple one by applying Lin and Reiter's result that progression reduces to forgetting predicates in first-order logic. They identified a simple case where forgetting a predicate reduces to forgetting a finite number of atoms, and used it in their proof. Forgetting in first-order logic was studied by Lin and Reiter [1994]. In the past decades, forgetting has found many applications in the area of knowledge representation and reasoning. Recently, Zhang and Zhou [2009] studied forgetting in propositional S5 modal logic. They defined forgetting based on the notion of bisimulation in modal logic, and their definition coincides with the semantic definition of formula ∃V φ in [French, 2005] and the notion of uniform interpolation in [Ghilardi et al., 2006]. A result of the latter paper illustrates that propositional S5 logic is closed under forgetting.

In this paper, we study progression of knowledge in the situation calculus. We first adapt the concept of bisimulation from modal logic and extend Lin and Reiter's definition of progression to accommodate knowledge. We show that for physical actions, progression of knowledge reduces to forgetting predicates in first-order modal logic. We study the problem of forgetting an atom or a predicate in first-order modal logic, and identify a class of first-order modal formulas for which forgetting an atom is definable in first-order modal logic, and forgetting a predicate is definable in second-order modal logic. This class of formulas goes beyond formulas without quantifying-in. We also identify a simple case where forgetting a predicate reduces to forgetting a finite number of atoms. Thus we are able to show that for local-effect physical actions, when the initial KB is a formula in this class, progression of knowledge is definable in first-order modal logic. As for sensing actions, we show how to do progression when the initial representation does not contain negative knowledge. Finally, we extend our results to the multi-agent case.

2 Preliminaries

2.1 First-order and second-order modal logic

The first-order modal language is obtained from the firstorder language by adding a syntactic rule: if φ is a formula, then Kφ (read as "knowing φ") is a formula, where K is a modal operator. We call Kφ a knowledge atom.

There are variations in the definition of semantics for FO modal logic. We take the constant domain variation in this paper. A Kripke structure is a tuple W = (S, R, D, π), where S is a set of states or possible worlds, R is a binary relation on S, called the accessibility relation, and π associates with each world s a first-order structure with D as the domain.

A variable assignment ν is a mapping from all variables to D. We let ν(x/d) denote the assignment that is the same as ν except that x is mapped to d. Given a Kripke structure W, a state s in W, a variable assignment ν, and a formula φ, W, s, ν |= φ ("W, s, ν satisfies φ") is defined as follows:

1. W, s, ν |= P(⃗τ) iff π(s), ν |= P(⃗τ);
2. W, s, ν |= φ ∨ ψ iff W, s, ν |= φ or W, s, ν |= ψ;
3. W, s, ν |= ¬φ iff W, s, ν ̸|= φ;
4. W, s, ν |= ∃xφ iff for some d ∈ D, W, s, ν(x/d) |= φ;
5. W, s, ν |= Kφ iff for all t such that sRt, W, t, ν |= φ.

A sentence φ is valid in W if W, s |= φ for all s ∈ S.

In modal logics, some commonly considered desired properties of knowledge are as follows:

• A3 Kφ ⊃ φ, the knowledge axiom;
• A4 Kφ ⊃ KKφ, the positive introspection axiom;
• A5 ¬Kφ ⊃ K¬Kφ, the negative introspection axiom.

These properties can be achieved by imposing various conditions on accessibility relations. For example, A3, A4, and A5 are valid in Kripke structures whose accessibility relations are reflexive, transitive, and Euclidean, respectively. A relation R is Euclidean if for any (x, y) ∈ R, (x, y′ ) ∈ R, we must have (y, y′ ) ∈ R. It is easy to show that a relation is an equivalence relation iff it is reflexive, transitive and Euclidean. In this paper, we restrict our attention to structures whose accessibility relations are equivalence relations. Such structures are called S5 structures in the literature.

We now extend FO modal logic to the second-order (SO) case. We add two syntactic rules, where P is a predicate variable: P(⃗τ) is a formula; if φ is a formula, so is ∃Pφ. An n-ary intension wrt a Kripke structure W = (S,R,D, π) is a function f mapping each s ∈ S to an n-ary relation on D. Now a variable assignment ν maps each predicate variable to an intension, in addition to mapping each individual variable to an element of D. We add the following semantic rules:

1. W, s, ν |= P(⃗τ) iff π(s), ν ′ |= P(⃗τ), where ν ′ is the same as ν except that it maps each predicate variable Q to ν(Q)(s);
2. W, s, ν |=∃Pφ iff for some intension I, W, s, ν(P/I)|=φ.

2.2 Situation calculus with knowledge

The situation calculus [Reiter, 2001] is a many-sorted firstorder language suitable for describing dynamic worlds. There are three disjoint sorts: action for actions, situation for situations, and object for everything else. A situation calculus language Lsc has the following components: a constant S0 denoting the initial situation; a binary function do(a, s) denoting the successor situation to s resulting from performing action a; a binary predicate Poss(a, s) meaning that action a is possible in situation s; action functions, e.g., move(x, y); a finite number of relational fluents, i.e., predicates taking a situation term as their last argument, e.g., ontable(x, s); and a finite number of situation-independent predicates and functions. We ignore functional fluents in this paper.

The situation calculus has been extended to accommodate sensing and knowledge. Assume that in addition to ordinary actions that change the world, there are sensing actions of the form senseψ(⃗x), which does not change the world but tells the agent whether some condition ψ(⃗x) holds in the current situation. Knowledge is modeled in the possible-world style by introducing a special fluent K(s′ , s), meaning that situation s′ is accessible from situation s. Then knowing φ at situation s is represented as follows:

In the presence of sensing and knowledge, a domain of application is specified by a basic action theory of the form:

1. Σ are the foundational axioms:

• (a) do(a1, s1) = do(a2, s2) ⊃ a1 = a2 ∧ s1 = s2
• (b) (¬s ❁ S0) ∧ (s ❁ do(a, s′ ) ≡ s ⊑ s′ )
• (c) ∀P.∀s[Init(s) ⊃ P(s)] ∧
• ∀a, s[P (s) ⊃ P (do(a, s))] ⊃ (∀s)P (s), where

• (d) K(s, s′ ) ⊃ [Init(s) ≡ Init(s′ )].

A model of these axioms consists of a forest of isomorphic trees rooted at the initial situations, which can be K-related to only initial situations.

1. Dss is a set of successor state axioms (SSAs) for fluents. The SSAs for ordinary fluents must satisfy the no-sideeffect conditions, i.e., they are not affected by sensing actions. The SSA for K is as follows:

Intuitively, s′ is accessible after a is done in s iff it is the result of doing a in some s∗ which is accessible from s and which agrees with s on the formula being sensed.

1. Dap is a set of action precondition axioms.
2. Duna is the set of unique names axioms for actions.
3. KInit consists of axioms stating that K has certain properties in all initial situations. Such a property P must have the feature that, by virtue of the SSA for K, P holds in all situations as long as P holds in all initial situations. For example, the axiom for reflexivity is: ∀s.Init(s) ⊃ K(s, s). In this paper, we assume that KInit consists of the axioms for the reflexive, transitive and Euclidean properties.
4. DS0 , called the initial KB, is a set of first-order sentences uniform in S0. We will make this more precise in Section 2.3.

2.3 Terminology and notation

Let Lsc be a situation calculus language. We use L to denote the situation-suppressed language of Lsc, i.e., the first-order language obtained from Lsc by removing the sort situation and the K fluent, and removing the situation argument from every ordinary fluent. We use L′ to denote the primed version of L, i.e., for each ordinary fluent F(⃗x, s), there is an F ′ (⃗x) predicate in L′ . We let L∗ denote the union of L and L′ . Intuitively, we can use L to talk about a situation σ, and use L′ to talk about a successor situation of σ. For a first-order language L, say L, L′ , or L∗ , we use Lm to denote the firstorder modal language based on L. For a language L, say L or Lm, we let L2 denote its second-order extension. By an L-formula we mean a formula of a language L, and by an L-structure we mean a structure of L.

Now let φ ∈ L2m, and σ a situation term. We define an L2sc -formula φ[σ], which asserts that φ holds in σ.

Definition 2.1 φ[σ] is inductively defined as follows:

For example, let φ be the modal formula KK∃xF(x). Then φ[S0] is ∀s.K(s, S0) ⊃ [∀s′ .K(s′ , s) ⊃ ∃xF(x, s)].

Similarly, we can define φ[σ] for φ ∈ L′2m, which asserts that the unprimed φ (the formula obtained from φ by replacing each F ′ with F ) holds in σ.

Definition 2.2 We use Lσ (L2σ resp.) to denote the set of φ[σ] where φ ∈ Lm (L2m resp.). A formula in Lσ or L2σ is said to be uniform in σ.

Let φ be a formula, μ and μ′ two expressions. We denote by φ(μ/μ′ ) the result of replacing every occurrence of μ in φ with μ′ . For a structure M and a syntactic object o, we let oM stand for the denotation of o in M. We use sitM to denote the domain of an Lsc-structure M for sort situation. Let α be a ground action. We denote by Sα the situation term do(α, S0).

We say that a formula in Lm is objective if it does not contain any K operator. We introduce a notation Lφ ("φ is possible"), which abbreviates for ¬K¬φ, and a notation Wφ ("knowing whether φ"), which abbreviates for Kφ ∨ K¬φ. We also use KWhether(φ, σ) to denote Wφ[σ].

3 Progression of knowledge

In this section, we extend Lin and Reiter's definition of progression to accommodate knowledge.

Let D be a basic action theory. Intuitively, a progression of DS0 wrt a ground action α should be a set of sentences DSα with the following properties: First, just as DS0 is uniform in S0, DSα should be uniform in Sα. Second, for all queries about the possible future of Sα, the old theory D is equivalent to the new theory (D - DS0 ) ∪ DSα .

To define progression, we first adapt the concept of bisimulation from modal logic and define a similarity relation between Lsc-structures. Roughly, a bisimulation is a relation between situations of two Lsc-structures where related situations agree on all ordinary fluents and have matching accessibility possibilities.

Definition 3.1 Let M and M ′ be Lsc-structures with the same domains for sorts action and object. Let γ ∈sitM and γ ′ ∈sitM′ . We writeM, γ∼M ′ , γ ′ ifM andM ′ interpret all situation-independent predicate and function symbols identically, and there is a bisimulation relation B ⊆ sitM × sitM′ such that γBγ ′ , and whenever δBδ′ , we have:

1. M, δ ≡ M ′ , δ′ , denoting that M, δ and M ′ , δ′ agree on all ordinary fluents, that is, for every ordinary fluent F, and every variable assignment ν, M, ν(s/δ) |= F(⃗x, s) iff M ′ , ν(s/δ′ ) |= F(⃗x, s).
2. For all ρ s.t. δKM ρ, there is ρ′ s.t. δ′KM′ ρ′ and ρBρ′ (the forth condition), here KM is the denotation of the K fluent inM.
3. For all ρ′ s.t. δ′KM′ ρ′ , there is ρ s.t. δKM ρ and ρBρ′ (the back condition).

We write M ∼Sα M ′ if M, SM α ∼ M ′ , SM′ α . Following the definition of progression in [Reiter, 2001], we have:

Definition 3.2 A set of sentences DSα in L2Sα is a progression of DS0 wrt α if D |= DSα , and for every model M of (D - DS0 ) ∪ DSα , there is a model M ′ of D such that M ∼Sα M ′ .

By induction on the formula, it is easy to prove:

Proposition 3.3 Let M, γ ∼ M ′ , γ ′ and φ ∈ L2m. Then for any ν, M, ν(s/γ) |= φ[s] iff M ′ , ν(s/γ ′ ) |= φ[s].

Then it is straightforward to prove:

Thus for any query about Sα, the old theory D and the new theory (D - DS0 ) ∪ DSα are equivalent.

4 Forgetting in first-order modal logic

In this section, we define forgetting in first-order modal logic, and analyze basic properties of forgetting. We identify a class of first-order modal formulas for which forgetting an atom is definable in first-order modal logic, and forgetting a predicate is definable in second-order modal logic. This class of formulas goes beyond formulas without quantifying-in.

We first review forgetting in first-order logic. We extend the definition to formulas with free variables.

Definition 4.1 Let φ(⃗x) ∈ L, and let μ be a ground atom or predicate. A formula ψ(⃗x) is a result of forgetting μ in φ(⃗x), written forget(φ(⃗x), μ) ⇔ ψ(⃗x), if for any L-structure U, and any variable assignment ν, U, ν |= ψ(⃗x) iff there exists an Lstructure U ′ such that U ′ , ν |= φ(⃗x) and U ∼μ U ′ , which denotes that U and U ′ agree on everything except possibly on the interpretation of μ.

A nice result about forgetting an atom in first-order logic is that it is always definable in first-order logic. As to forgetting a predicate, the result is definable in second-order logic. Let φ be a formula, P(⃗τ) a ground atom, and v a truth value. We denote by φvP(⃗τ) the result of replacing every occurrence of the form P (⃗τ ′ ) in φ by ⃗τ = ⃗τ ′ ∧ v ∨ ⃗τ ̸= ⃗τ ′ ∧ P (⃗τ ′ ).

Proposition 4.2

1. forget(φ, P(⃗τ)) ⇔φtrue P(⃗τ) ∨ φfalse P(⃗τ) ;
2. forget(φ, P) ⇔ ∃R.φ(P/R), whereR is a second-order predicate variable.

To define forgetting in first-order modal logic, we first define a similarity relation between pairs of the form (W, s) where W is a Kripke structure and s a state in M.

Definition 4.3 Let μ be a ground atom or predicate. Let W = (S, R, D, π) and W ′ = (S′ , R′ , D, π′ ) be Kripke structures with the same domain. Let s ∈ S and s′ ∈ S′ . We write W, s ∼μ W ′ , s′ if there exists a bisimulation relation B ⊆ S × S′ such that sBs′ , and whenever tBt′ , we have:

1. π(t) ∼μ π′ (t′ );
2. For all u s.t. tRu, there exists u′ s.t. t′R′u′ and uBu′ ;
3. For all u′ s.t. t′R′u′ , there exists u s.t. tRu and uBu′ .

We define forgetting as follows:

Definition 4.4 Let φ(⃗x) ∈ Lm, and let μ be a ground atom or predicate. A formula ψ(⃗x) is a result of forgetting μ in φ(⃗x), written kforget(φ(⃗x), μ) ⇔ ψ(⃗x), if for any S5 pair (W, s), and any ν, W, s, ν |= ψ(⃗x) iff there exists an S5 pair (W ′ , s′ ) such that W ′ , s′ , ν |= φ(⃗x) and W, s ∼μ W ′ , s′ .

Next, we analyze basic properties of forgetting. We say a formula φ irrelevant to a predicate P if φ is equivalent to a formula which does not use P. We say φ irrelevant to a ground atom P (⃗τ ) if φ is equivalent to a formula ψ where any appearance of P (⃗τ ′ ) must be in the form of P (⃗τ ′ ) ∧ ⃗τ ′ ̸= ⃗τ .

Proposition 4.5 Let φ be a sentence and kforget(φ, μ) ⇔ ψ. Then φ |= ψ; and for any η irrelevant to μ, φ |= η iff ψ |= η.

Proposition 4.6 1. If φ is an objective formula, then kforget(φ, μ) ⇔ forget(φ, μ);

1. If kforget(φi, μ) ⇔ψi, i = 1, 2, then kforget(φ1 ∨ φ2, μ) ⇔ ψ1 ∨ ψ2;
2. If kforget(φ(⃗x, y), μ) ⇔ψ(⃗x, y), then kforget(∃yφ(⃗x, y), μ) ⇔ ∃yψ(⃗x, y).

In general, we do not have: kforget(φ1∧φ2, μ) ⇔ ψ1∧ψ2, where kforget(φi, μ) ⇔ ψi, i = 1, 2. But we can identify a form of conjunctive formulas for which forgetting reduces to forgetting for component formulas. Clearly, we have Kφ1 ∧ Kφ2 ⇔ K(φ1 ∧ φ2), but not Lφ1 ∧ Lφ2 ⇔ L(φ1 ∧ φ2). An extended term is a formula of the form φ ∧ Kψ ∧ ∧i ∀⃗xiLηi, where φ, ψ, and ηi's are all objective. The following proposition shows that extended terms are closed under forgetting.

Proposition 4.7 Let ξ be an extended term φ ∧Kψ ∧ ∧i ∀⃗xiLηi. Let forget(φ ∧ψ, μ) ⇔φ′ , forget(ψ, μ) ⇔ψ′ , forget(ψ ∧ ηi, μ) ⇔ η′i .

Then kforget(ξ, μ) ⇔ φ′ ∧ Kψ′ ∧ ∧i ∀⃗xiLη′i .

Proof sketch: Let ζ denote φ′ ∧ Kψ′ ∧ ∧i ∀⃗xiLη′i . We show that for any S5 pair (W, s) and any ν, W, s, ν |= ζ iff there is an S5 pair (W ′ , s′ ) s.t. W ′ , s′ , ν |= ξ and W, s ∼μ W ′ , s′ . We only show the only-if direction here. So suppose W, s, ν |= ζ. Let W = (S,R,D, π). Then π(s), ν |= φ′ ; for any t s.t. sRt, π(t), ν |= ψ′ ; and for all i, for all ⃗ei ∈ D, there exists τ(⃗ei) s.t. sRτ(⃗ei) and π(τ(⃗ei)), ν(⃗xi/⃗ei) |= η′i . We define W ′ = (S′ ,R′ ,D, π′ ) and the bisimulation B as follows: there is a state s′ in S′ , sBs′ , π(s) ∼μ π′ (s′ ), and π′ (s′ ), ν |= φ ∧ ψ; for any i and any ⃗ei ∈ D, there is a state τ ′ (⃗ei) in S′ , τ(⃗ei)Bτ ′ (⃗ei), π(τ(⃗ei)) ∼μ π′ (τ ′ (⃗ei)), and π′ (τ ′ (⃗ei)), ν |= ψ ∧ ηi; for any t s.t. sRt, if there has not been a state t′ in S′ s.t. tBt′ , add a state t′ in S′ , let tBt′ , π(t) ∼μ π′ (t′ ), and π′ (t′ ), ν |= ψ. Let R′ = S′ × S′ . Then W, s ∼μ W ′ , s′ and W ′ , s′ , ν |= ξ.

We now define a normal form for Lm-formulas:

Definition 4.8 We say that an Lm-formula φ is in ∃-disjunctive normal form (∃-DNF) if it is of the form ∃⃗x(φ1 ∨ . . . ∨ φn), where each φi is an extended term.

By Propositions 4.2, 4.6, and 4.7, we have:

Theorem 4.9 Let φ be in ∃-DNF. Then the result of forgetting an atom in φ is definable in first-order modal logic, and the result of forgetting a predicate in φ is definable in secondorder modal logic without second-order quantifying-in.

By second-order quantifying-in, we mean occurrence of SO quantifiers outside the K operators. To shed light on the expressiveness of ∃-DNF, we note two results. First, due to the constant domain semantics, we have ∀xKφ(x) ⇔ K∀xφ(x) and ∃xLφ(x) ⇔ L∃xφ(x). Also, we have

Theorem 4.10 Let φ be a formula without quantifying-in, i.e., no quantifiers occur outside the K operators. Then φ can be transformed in S5 to an equivalent formula without nesting of the K operators.

The proof is the same as that for propositional S5, which can be found in, for example, [Hughes and Cresswell, 1996]. The resulting formula can be further transformed into a form of DNF whose atoms are objective formulas and knowledge atoms. Such DNF is a special case of ∃-DNF.

Thus the class of formulas, for which forgetting an atom is definable in FO modal logic and forgetting a predicate is definable in SOmodal logic, includes the following, where φ is objective: formulas without quantifying-in; ∀xKφ, ∃xKφ, ∀xLφ, ∃xLφ; and ∃x∀yLφ, ∀x∃yLφ, ∃x∀yKφ.

Example 4.1 Consider a simple blocks world. There are two predicates: clear(x): block x has no blocks on top of it, and on(x, y): block x is on block y. Let φ be the conjunction of the following sentences:

1. φ1 : ∀x(x ̸= A∧ x ̸= B ∧ x ̸= C ⊃ ¬clear(x)),
2. Kφ2, where φ2 is ∀x∀y(on(x, y) ⊃ ¬clear(y)),
3. φ3 : ∀u∀vLon(u, v) ∧ ∀u∀vL¬on(u, v), stating that the agent has no knowledge about the on predicate,
4. K¬clear(A) ∨K¬clear(B),
5. ∃z(z ̸= A∧z ̸= B∧K¬clear(z)), stating that the agent knows that some block other than A and B is not clear.

We will compute kforget(φ, on) and kforget(φ, clear(C)). To save space, in the sequel, we will use "c(x)" for "clear(x)".

We first convert φ into ∃-DNF ∃z(ψ1 ∨ ψ2), where ψ1 is φ1 ∧ z ̸= A ∧ z ̸= B ∧ K(φ2 ∧ ¬c(z) ∧ ¬c(A)) ∧ φ3, and ψ2 is φ1 ∧ z ̸= A ∧ z ̸= B ∧ K(φ2 ∧ ¬c(z) ∧ ¬c(B)) ∧ φ3.

Then kforget(φ, on) is ∃z(η1 ∨ η2), where η1 is

∃R[φ1 ∧ z ̸= A ∧ z ̸= B ∧ ∀x∀y(R(x, y) ⊃ ¬c(y)) ∧

K∃R[∀x∀y(R(x, y) ⊃ ¬c(y)) ∧ ¬c(z) ∧ ¬c(A)] ∧

∀u∀vL∃R[R(u, v) ∧ ∀x∀y(R(x, y) ⊃ ¬c(y)) ∧

¬c(z) ∧ ¬c(A)], and η2 is the same as η1 except that ¬c(A) is replaced with ¬c(B).

Finally, kforget(φ, clear(C)) is ∃z(ξ1 ∨ ξ2), where ξ1 is

[¬on(u, v) ∧ φ2 ∧ ¬c(z) ∧ ¬c(A)]false

c(C) }, and ξ2 is

the same as ξ1 except that ¬c(A) is replaced with ¬c(B).

5 Representing progression of knowledge

In this section, we prove that for physical actions, progression of knowledge reduces to forgetting predicates in first-order modal logic. Further, we show that for local-effect physical actions, when the initial KB is in ∃-DNF, progression of knowledge is definable in first-order modal logic. As for sensing actions, we show how to do progression when the initial KB does not contain negative knowledge.

5.1 Progression wrt physical actions

The SSA for any ordinary fluent F is in the form of F(⃗x, do(a, s)) ≡ ΦF (⃗x, a)[s], where ΦF (⃗x, a) ∈ L. Let α be a physical action. We let Dss[α, S0] denote the instantiation of Dss wrt α and S0, i.e., the set of sentences F (⃗x, Sα) ≡ ΦF (⃗x, α)[S0]. We use D∗ ss [α, S0] to denote the set of sentences F ′ (⃗x) ≡ ΦF (⃗x, α).

The following theorem shows that for physical actions, progression of knowledge reduces to forgetting all the F predicates in an L∗m-formula.

Theorem 5.1 Let DS0 be φ[S0] where φ ∈ Lm, and α a physical action. Let kforget(φ∧KD∗ ss [α, S0], ⃗ F ) ⇔ ψ, where ψ ∈ L′2m. Then ψ[Sα] is a progression of DS0 wrt α.

Note about the K operator in front of D∗ ss [α, S0] in the theorem. As pointed out in [Reiter, 2001], a consequence of the way knowledge is modeled in the situation calculus is that an agent knows the successor state axioms of her actions.

To prove the theorem, we now introduce a method to induce a Kripke structure from a model of D - DS0 . Note that the instantiation of the SSA for K wrt a physical action α is:

So the K relation on situations resulting from doing α in initial situations is a copy of the K relation on initial situations.

Definition 5.2 Let M |= D-DS0 . We define a Kripke structure Wα = (S,R,D, π) as follows. S is the set of initial situations of M. R is the restriction of KM to S. D is the union of M's domains for sorts action and object. Let ϵ ∈ S. π(ϵ) interprets any situation-independent predicate and function symbol as M does. For each ordinary fluent F(⃗x, s), π(ϵ) interprets F(⃗x) as M interprets F(⃗x, s) at ϵ, and interprets F ′ (⃗x) as M interprets F (⃗x, s) at doM (αM , ϵ).

Proposition 5.3 Let M |= D - DS0 . Then

1. Wα, SM 0 |=KD∗ ss [α, S0];
2. for any φ ∈ L2m, M |= φ[S0] iff Wα, SM 0 |= φ;

We now prove the theorem:

Proof sketch: We first prove D |= ψ[Sα]. So let M |= D. By Proposition 5.3, Wα, SM 0 |= φ ∧ KD∗ ss [α, S0], which, by Proposition 4.5, implies ψ. Thus Wα, SM 0 |= ψ. So M |= ψ[Sα]. Nowwe prove for anyM, if M |= (D-DS0 )∪ {ψ[Sα]}, then there exists M ′ |= D s.t. M ∼Sα M ′ . So let M |= (D-DS0 )∪{ψ[Sα]}. ThenWα, SM 0 |= ψ. Thus there exists an S5 pair (W ∗ , s∗ ) s.t. W ∗ , s∗ |= φ ∧ KD∗ ss [α, S0] and Wα, SM 0 ∼⃗ F W ∗ , s∗ . We construct M ′ as follows: M and M ′ have the same domains for sorts action and object, and interpret any situation-independent predicate and function identically. The initial situations of M ′ are the states of M ∗ accessible from s∗ , M ′ interprets S0 as s∗ , and the situations of M ′ form a forest rooted at the initial situations. All the initial situations of M ′ are K-related, and for each initial situation ϵ of M ′ , M ′ interprets any ordinary fluent F at ϵ as M ∗ does at ϵ. Finally, M ′ |= Dss ∪Dap.

By Theorems 4.9 and 5.1, we have:

Corollary 5.4 Let DS0 be in ∃-DNF, and α a physical action. Then progression of DS0 wrt α is definable in second-order modal logic without second-order quantifying-in.

5.2 Progression wrt local-effect physical actions

We first present an intuitive result concerning forgetting a predicate in first-order modal logic: if a sentence φ entails knowing that the truth values of two predicates P and Q are different at only a finite number of certain instances, then forgetting Q in φ can be obtained from forgetting the Q atoms of these instances in φ and then replacing Q by P in the result.

Let ⃗x be a vector of variables, and let Δ = {⃗τ1, . . . , ⃗τm} be a set of vectors of ground terms, where all the vectors have the same length. We use ⃗x ∈ Δ to represent the formula ⃗x = ⃗τ1 ∨ . . . ∨ ⃗x = ⃗τm. Let P and Q be two predicates. We let Q(Δ) denote the set {Q(⃗τ) | ⃗τ ∈ Δ}, and we let P ≈Δ Q represent the sentence ∀⃗x.⃗x ̸∈ Δ ⊃ P (⃗x) ≡ Q(⃗x).

Proposition 5.5 Let kforget(φ,Q(Δ)) ⇔ ψ, and M, s |= K(P ≈ΔQ). Then M, s |= ψ iff M, s |= ψ(Q/P).

Theorem 5.6 Let P and Q be two predicates, and Δ a finite set of vectors of ground terms. If kforget(φ, Q(Δ)) ⇔ ψ, then kforget(φ ∧ K(P ≈Δ Q), Q) ⇔ ψ(Q/P ).

Actions in many dynamic domains have only local effects in the sense that if an action A(⃗c ) changes the truth value of an atom F(⃗a, s), then ⃗a is contained in ⃗c . This contrasts with actions having non-local effects such as moving a briefcase, which will also move all the objects inside the briefcase without having mentioned them. For a formal definition of local-effect action theory, see [Liu and Lakemeyer, 2009].

Now let D be a local-effect action theory. Let α = A(⃗c) be a physical action. We use Ω to denote the set of F(⃗a) where F is an ordinary fluent, and ⃗a is contained in ⃗c. Then α only changes the truth values of atoms from Ω. Recall that D∗ ss [α, S0] denotes the set of sentences F ′ (⃗x) ≡ ΦF (⃗x, α). We let D∗ ss [Ω] denote the set of sentences F ′ (⃗a) ≡ ΦF (⃗a, α), where F(⃗a) ∈ Ω. Then D∗ ss [α, S0] is logically equivalent to D∗ ss [Ω] together with the set of sentences F ′ ≈Δ F, where Δ = {⃗a | ⃗a is contained in ⃗c}.

By Theorems 4.9, 5.1, and 5.6, we get:

Theorem 5.7 Let D be local-effect, and α a physical action. Let DS0 be φ[S0] where φ is in ∃-DNF. Then there is ψ ∈ L∗m such that kforget(φ ∧KD∗ ss [Ω], Ω) ⇔ ψ, and ψ( ⃗ F/ ⃗ F ′ )[Sα] is a progression of DS0 wrt α.

So for local-effect actions, when DS0 is in ∃-DNF, progression of knowledge is definable in first-order modal logic, and can be computed by forgetting in φ∧KD∗ ss [Ω] atoms fromΩ and then replacing each F by F ′ in the result.

Example 5.1 Consider the litmus testing example. There are two actions: test, insert litmus paper into solution, and sensered, sense whether the paper turns red.

DS0 = {acid(S0), Knows(¬red, S0)}. Dss includes: red(do(a, s)) ≡ a = test ∧ acid(s) ∨ red(s), acid(do(a, s)) ≡ acid(s) ∧ a ̸= dilute.

Here test is a local-effect action: it only changes the truth value of red. Let S1 = do(test, S0). Dss[red] is red(S1) ≡ acid(S0) ∨ red(S0). By Theorem 5.7, to compute DS1 , the progression of DS0 wrt test, we compute kforget(φ, red), where φ = acid ∧K¬red ∧K(red′ ≡ acid ∨ red), which is equivalent to acid ∧ K(¬red ∧ (red′ ≡ acid)). Since forget(acid∧¬red∧(red′ ≡ acid), red) ⇔ acid∧red′ , and forget(¬red ∧ (red′ ≡ acid), red) ⇔ (red′ ≡ acid), by Proposition 4.7, we have

kforget(φ, red) ⇔ acid ∧ red′ ∧ K(red′ ≡ acid). Thus DS1 = {acid(S1), red(S1), Knows(red ≡ acid, S1)}.

5.3 Progression wrt sensing actions

We say that a formula does not contain negative knowledge if no knowledge atom appears within the scope of an odd number of negation operators. The following theorem shows when the initial KB does not contain negative knowledge, progression wrt sensing actions can be achieved by simply adding knowing whether the sensed formula holds.

Theorem 5.8 Assume that DS0 does not contain negative knowledge. Let ψ(⃗x) be an objective formula. Let α be the sensing action senseψ(⃗c). Then the following is a progression of DS0 wrt α: DS0 (S0/Sα) ∪ {Wψ(⃗c)[Sα]}.

Proof sketch: We first prove D |= DS0 (S0/Sα) ∪ {Wψ(⃗c)[Sα]}. So let M |= D. Since DS0 does not contain negative knowledge and M |= DS0 , we get M |= DS0 (S0/Sα). We can prove that if M |= ψ(⃗c, S0), thenM |= Knows(ψ(⃗c), Sα), otherwise M |= Knows(¬ψ(⃗c), Sα). Now let M |= (D - DS0 ) ∪ DS0 (S0/Sα) ∪ {Wψ(⃗c)[Sα]}. We prove that there existsM ′ |= D s.t. M ∼Sα M ′ . We construct M ′ as follows: The initial situations of M ′ is the set of situations K-related to SM α , and M ′ interprets S0 as SM α . For each initial situation ϵ of M ′ , M ′ interprets any ordinary fluent F at ϵ as M does at ϵ. The rest of the construction is the same as that in the proof of Theorem 5.1. Note that we need M |= Wψ(⃗c)[Sα] to prove M ∼Sα M ′ .

Example 5.1 continued. Let S2 = do(sensered, S1). Since DS1 does not contain negative knowledge, by Theorem 5.8, the progression of DS1 wrt sensered is {acid(S2), red(S2), Knows(red ≡ acid, S2), KWhether(red, S2)}, which is equivalent to

{Knows(red, S2), Knows(acid, S2)}.

6 Extension to the multi-agent case

In this section, we extend our results on forgetting and progression to the multi-agent case.

The multi-agent first-order modal language is the same as the single-agent one except that there is a modal operator Ki for each agent i, and there is an extra modal operator C. If φ is a formula, so are Kiφ ("agent i knows φ") and Cφ ("φ is common knowledge"). A Kripke structure for n agents is the same as before except that there is an accessibility relation Ri for each agent i. The semantics is defined as follows:

1. M, s, ν |= Kiφ iff for all t such that sRit, M, t, ν |= φ;
2. M, s, ν |= Cφ iff M, t, ν |= φ for all t that are reachable from s by the the relation R, the union of all Ri's.

The definition of forgetting is the same as before except: when defining the similarity relation between Kripke structures, we require the forth and back conditions hold for each agent i; and when defining forgetting, we consider S5 structures, i.e., structures where each Ri is an equivalence relation.

Clearly, we have Cφ1 ∧ Cφ2 ⇔ C(φ1 ∧ φ2). We now define ∃-DNF in the multi-agent case. We say that a formula φ is purely objective if it does not contain any modal operator. We say that φ is objective wrt agent i if it does not use any Ki operator. We inductively define extended terms as follows:

1. A purely objective formula is an extended term;
2. A formula of formφ∧Cϕ∧∧i (Kiψi∧∧j ∀⃗xijLiηij) is an extended term if φ, ϕ and all ψi's are purely objective, and all ηij's are extended terms objective wrt agent i.

The following proposition shows that extended terms are closed under forgetting.

Proposition 6.1

Let ξ be an extended term φ∧Cϕ∧∧i (Kiψi∧∧j ∀⃗xijLiηij). Let forget(φ ∧ ϕ ∧ ∧i ψi, μ) ⇔ φ′ , forget(ϕ, μ) ⇔ ϕ′ , forget(ϕ ∧ ψi, μ) ⇔ ψ′i , kforget(ψi ∧ Cϕ ∧ ηij , μ) ⇔ η′ij . Let ζ be φ′ ∧ Cϕ′ ∧ ∧i (Kiψ′i ∧ ∧j ∀⃗xijLiη′ij ). Then kforget(ξ, μ) ⇔ ζ .

Proof sketch: The proof is similar to that of Proposition 4.7. Let W, s, ν |= ζ. Then for all i and j, for all ⃗eij ∈ D, there is τ(⃗eij) s.t. sRiτ(⃗eij) and W, τ(⃗eij), ν(⃗xij/⃗eij) |= η′ij . Thus there exists W(⃗eij), τ ′ (⃗eij) ∼μ W, τ(⃗eij) such that W(⃗eij), τ ′ (⃗eij), ν(⃗xij/⃗eij) |= ψi ∧ Cϕ ∧ ηij. When constructing W ′ , we include W(⃗eij) and add Ki edges between τ ′ (⃗eij) and other states of W ′ . Since ηij is objective wrt agent i, we get W ′ , τ ′ (⃗eij), ν(⃗xij/⃗eij) |= ηij .

The definition of ∃-DNF is as before, and Theorem 4.9 also holds in the multi-agent case, i.e., for an ∃-DNF formula, forgetting an atom is definable in FO modal logic, and forgetting a predicate is definable in SO modal logic without SO quantifying-in.

We now consider progression in the multi-agent case. Each agent i can perform a number of sensing actions: sensei,ψij (⃗xij), j = 1, . . . ,m. For each agent i, there is a special fluent Ki(s′ , s). The SSA for Ki is as follows:

We assume that all agents can perform the same kinds of actions. Under this assumption, a consequence of the way knowledge is modeled in the situation calculus is that the agents commonly knows the successor state axioms of physical actions. We consider the case of public actions whose occurrence is common knowledge. For example, when two agents cooperate in the blocks world, the physical actions are public. When two agents play a card game, a public sensing action of an agent is the action of picking up and reading a card dealt to her. We have the following results on progression, which are the same as in the single-agent case except that the K operator is replaced with the C operator. The first result shows that after an agent publicly performs a physical action, its effect becomes common knowledge. The second result shows that after agent i publicly senses a formula ψ, it becomes common knowledge that agent i knows if ψ holds.

Theorem 6.2 Let DS0 be φ[S0] where φ ∈ Lm, and α a public physical action. Let kforget(φ ∧ CD∗ ss [α, S0], ⃗ F) ⇔ ψ, where ψ ∈ L′2m. Then ψ[Sα] is a progression of DS0 wrt α.

Theorem 6.3 Assume that DS0 does not contain negative knowledge. Let ψ(⃗x) be an objective formula, and α a public sensing action sensei,ψ(⃗c). Then the following is a progression of DS0 wrt α: DS0 (S0/Sα) ∪ {CWiψ(⃗c)[Sα]}, where Wiψ abbreviates for Kiψ ∨ Ki¬ψ.

Example 6.1 There is a red card and a green card. A dealer gives a card each to Ann and Bob. We use a fluent red(i, s), meaning that agent i has the red card in situation s. We use a sensing action sensei,red(x), meaning that agent i picks up and reads his/her card. Suppose that the dealer has dealt the red card to Ann, and green card to Bob. Then

DS0 = {red(a, S0), ¬red(b, S0), C(red(a) ∧ ¬red(b) ∨ ¬red(a) ∧ red(b))[S0]}. Let S1 = do(sensea,red(a), S0). Then DS1 = DS0 (S0/S1) ∪ {CWared(a)[S1]}, which entails Kared(a)[S1], KbWared(a)[S1], and KbWared(b)[S1], but does not entail Kbred(a)[S1].

Let S2 = do(senseb,red(b), S1). Then DS2 = DS1 (S1/S2) ∪ {CWbred(b)[S2]}, which is logically equivalent to {Cred(a)[S2], C¬red(b)[S2]}.

7 Conclusions

In this paper, we studied progression of knowledge in the situation calculus. We showed that for physical actions, this reduces to forgetting predicates in first-order modal logic. We studied forgetting in first-order modal logic, and identified a class of first-order modal formulas for which forgetting an atom is definable in first-order modal logic, and forgetting a predicate is definable in second-order modal logic. This class of formulas goes beyond formulas without quantifyingin. We showed that for local-effect physical actions, when the initial KB is a formula in this class, progression of knowledge is definable in first-order modal logic. As for sensing actions, we showed that when the initial KB does not contain negative knowledge, progression can be achieved by simply adding knowing whether the sensed formula holds. Finally, we extended our results to the multi-agent case. For the future, we would like to do an in-depth study of forgetting in first-order modal logic. We would also like to investigate how to do progression wrt sensing actions in the general case. It would also be interesting to explore progression for only-knowing.

Acknowledgments

We thank the anonymous reviewers for helpful comments. This work was supported in part by the Natural Science Foundation of China under Grant No. 61073053.