Semantics for a useful fragment of the situation calculus

1 Introduction

In a recent paper, we [Lakemeyer and Levesque, 2004] presented a new logic called ES for reasoning about the knowledge, action, and perception of an agent. Our main justi�cation for introducing yet another knowledge representation formalism was twofold. First, we claimed that the language was not a new formalism at all, but merely a situation-suppressed version of part of the situation calculus, as originally presented by McCarthy and Hayes [McCarthy and Hayes 1969] and subsequently formalized by Reiter [Reiter 2001a]. Second, we claimed that because the language was de�ned semantically rather than axiomatically, certain mathematical arguments about the formalismwere considerably simpler than in the original situation calculus. We presented evidence for this by showing a very compact proof of the correctness of Reiter's regression operator, and another involving a property called the determinacy of knowledge.

However, our �rst claim, which was that ES is in fact just an alternate way of writing some formulas of the situation calculus, was left unsubstantiated. In this paper, we remedy this. The main result we prove is the correctness of a simple mapping between sentences of ES and their counterparts in the classical language of the situation calculus. In addition, we show that the fragment of the situation calculus expressed

Hector J. Levesque

Dept. of Computer Science University of Toronto Toronto, Ontario Canada M5S 3A6

hector@cs.toronto.edu

by ES is rich enough to handle (among other things) basic action theories (as de�ned by Reiter) and the Do operator which is the basis of the Golog language [Levesque et al. 1997]. We also illustrate this richness more informally using an example involving the knowledge, action, and sensing of a simple robot. However, there are sentences of the situation calculus that cannot be expressed directly in ES, and which may be useful in some contexts. In the �nal part of the paper, we show that if we are prepared to use second-order quanti�cation, there is a way to encode (almost) every sentence of the situation calculus in ES. This encoding is a bit of a trick, and not something we advocate for everyday use. But it does exist. So we gain the clarity that comes from having a real semantic basis, and the ability to present concise semantic arguments, without any signi�cant loss of expressiveness.

The rest of the paper is organized as follows. In the next section, we de�ne the full language of ES, its syntax and semantics. This generalizes the version of ES presented in [Lakemeyer and Levesque, 2004] in a variety of ways, the most important of which is that it allows functions, predicates, and second-order variables that are fluent (vary from situation to situation) as well as rigid (�xed for all situations). In Section 3, we consider the mapping from ES to the situation calculus and prove that a sentence of ES is valid iff its mapping is a logical entailment of a suitable situation calculus theory. In Section 4, we consider the expressiveness of ES, �rst with an example basic action theory and then with Do. In Section 5, we consider the inverse mapping from the situation calculus to ES, followed by some remarks on related work and conclusions. Then we stop.

2 The language: syntax and semantics

The full language ES consists of formulas over symbols from the following vocabulary:

• �rst-order variables: x1, x2, . . . , y1, y2, . . . , a1, a2, . . .;
• �uent second-order variables of arity k: P k 1 , P k 2 , . . .;
• rigid second-order variables of arity k: Qk1,Qk2, . . .;
• standard names: n1, n2, . . .;
• �uent function symbols of arity k: f k 1 , f k 2 , . . .; for example, location, bestAction;
• rigid function symbols of arity k: g k 1 , gk 2 , . . .; for example, block5, repair;
• �uent predicate symbols of arity k: F k 1 , F k 2 , . . .; for example, Broken; 1
• rigid predicate symbols of arity k: Gk1 ,Gk2 , . . .; for example, Fragile;
• connectives and other symbols: =, ∧, ¬, ∀, Know, □, round and square parentheses, period, comma.

We assume that �rst-order variables, standard names, and function symbols come in two sorts, action (like repair and bestAction) and object (like block5 and location). Constants are function symbols of 0 arity. 2 We let N denote the set of all standard names and Z denote the set of all sequences of standard names for actions, including 〈 〉, the empty sequence.

2.1 Terms and formulas

The terms of the language are of sort action or object, and form the least set of expressions such that

1. Every standard name and �rst-order variable is a term of the corresponding sort;
2. If t1, . . . , tk are terms and h is a k-ary function symbol then h(t1, . . . , tk) is a term of the same sort as h.

By a primitive term we mean one of the form h(n1, . . . , nk) where h is a (�uent or rigid) function symbol and all of the ni are standard names.

The well-formed formulas of the language form the least set such that

1. If t1, . . . , tk are terms, andH is a k-ary predicate symbol then H(t1, . . . , tk) is an (atomic) formula;
2. If t1, . . . , tk are terms, and V is a k-ary second-order variable, then V (t1, . . . , tk) is an (atomic) formula;
3. If t1 and t2 are terms, then (t1 = t2) is a formula;
4. If t is an action term and α is a formula, then [t]α is a formula;
5. If α and β are formulas, v is a �rst-order variable, and V is a second-order variable, then the following are also formulas: (α ∧ β), ¬α, ∀v. α, ∀V. α, □α, Know(α).

We read [t]α as �α holds after action t�, and □α as �α holds after any sequence of actions.� As usual, we treat (α ∨ β), (α ⊃ β), (α ≡ β), ∃v. α, and ∃V. α as abbreviations. We call a formula without free variables a sentence. By a primitive sentence we mean a formula of the form H(n1, . . . , nk) where H is a (�uent or rigid) predicate symbol and all of the ni are standard names.

2.2 The semantics

The language contains both �uent and rigid expressions. The former vary as the result of actions and have values that may be unknown, but the latter do not. Intuitively, to determine whether or not a sentence α is true after a sequence of actions z has been performed, we need to specify two things: a world w and an epistemic state e. We write e, w, z |= α. A

1 We assume this list includes the predicates Poss and SF.

2 The standard names can be thought of as special extra constants that satisfy the unique name assumption and an in�nitary version of domain closure.

world determines truth values for the primitive sentences and co-referring standard names for the primitive terms after any sequence of actions. An epistemic state is de�ned by a set of worlds, as in possible-world semantics. More precisely:

• a world w ∈ W is any function from the primitive sentences and Z to {0, 1}, and from the primitive terms and Z to N (preserving sorts), and satisfying the rigidity constraint: if r is a rigid function or predicate symbol, then w[r(n1, . . . , nk), z] = w[r(n1, . . . , nk), z ′ ], for all z and z ′ in Z.
• an epistemic state e ⊆ W is any set of worlds.

We extend the idea of co-referring standard names to arbitrary ground terms as follows. Given a term t without variables, a world w, and an action sequence z, we de�ne |t|zw (read: the co-referring standard name for t given w and z) by:

1. If t ∈ N, then |t|zw = t;
2. |h(t1, . . . , tk)|zw = w[h(n1, . . . , nk), z], where ni = |ti|zw.

To interpret formulas with free variables, we proceed as follows. First-order variables are handled substitutionally using the standard names. To handle the quanti�cation over secondorder variables, we use second-order variable maps de�ned as follows:

The second-order primitives are formulas of the form V (n1, . . . , nk) where V is a (�uent or rigid) second-order variable and all of the ni are standard names. A variable map u is a function from worlds, second-order primitives, and Z to {0, 1}, satisfying the rigidity constraint: if Q is a rigid second-order variable, then for all w and w′ in W, and all z and z ′ in Z, u[w,Q(n1, . . . , nk), z] = u[w′ , Q(n1, . . . , nk), z ′ ].

Let u and u′ be variable maps, and let V be a (�uent or rigid) second-order variable; we write u′ ∼V u to mean that u and u′ agree except perhaps on the second-order primitives involving V . Finally, to interpret what is known after a sequence of actions possibly including sensing has taken place, we de�ne w′ ≃z w (read: w′ and w agree on the sensing throughout action sequence z) inductively by the following:

1. w′ ≃〈 〉 w iff w′ and w agree on the value of every primitive rigid term and sentence;
2. w′ ≃z·n w iff w′ ≃z w and w′ [SF(n), z] = w[SF(n), z].

Putting all these together, here is the semantic de�nition of truth. Given e ⊆ W and w ∈ W, we de�ne e, w |= α (read: α is true) as e,w, 〈 〉 |= α, where for any z ∈ Z and any second-order variable map u:

1. e,w, z, u |= (α ∧ β) iff e, w, z, u |= α and e, w, z, u |= β;
2. e,w, z, u |= ¬α iff e,w, z, u ̸|= α;
3. e,w, z, u |= ∀v. α iff e,w, z, u |= αxn, for every standard name n (of the same sort as v);
4. e,w, z, u |= ∀V. α iff e,w, z, u′ |= α, for every u′ ∼V u;
5. e,w, z, u |= □α iff e, w, z · z ′ , u |= α, for every z ′ ∈ Z;

10. e,w, z, u |= Know(α) iff

e, w′ , z, u |= α, for every w′ ∈ e such that w′ ≃z w.

When α is objective (has no Know operators), we can leave out the e and write w |= α. When Σ is a set of sentences and α is a sentence, we write Σ |= α (read: Σ logically entails α) to mean that for every e and w, if e,w |= α′ for every α′ ∈ Σ, then e,w |= α. Finally, we write |= α (read: α is valid) to mean {} |= α.

3 Mapping to the situation calculus

How do we know that the semantics of ES is correct? In this section, we argue that it is indeed correct by showing how formulas α in ES can be translated in a direct way to formulas α∗ in the situation calculus as de�ned by Reiter. 3

The most desirable and simplest outcome of this translation would be that |= α iff Σ |=FOL α∗ , where |= is validity in ES, Σ is the set of foundational axioms of the situation calculus (see [Levesque et al, 1998], for example), and |=FOL is ordinary classical logical consequence. Unfortunately, we do not get exactly this correspondence for a variety of reasons we will discuss below. But we do get something close:

where Υ is a set of four axioms that we will justify separately.

To prove this result it will be necessary to work with ordinary Tarski models of sentences of the situation calculus. As argued in [Lakemeyer and Levesque, 2004], this is dif�- cult and painstaking, and is indeed one of the main reasons to prefer ES over the situation calculus. So while the proof of the theorem is quite laborious, we remind the reader that this can be thought of as a �nal reckoning for a formalism that is unworkable semantically. For space reasons, we do not review the conventional notation used for talking about Tarski interpretations, denotations, extensions, variable maps. See, for example, [Enderton 1972].

3.1 Definition of the translation

Before describing Υ, we present the translation from ES into the situation calculus. In the simplest case, the idea is that a formula like Broken(c), where Broken is a �uent, will be mapped to the situation calculus formula Broken(c, S0), where we have restored the distinguished situation term S0 for the �uent. Similarly, [repair(c)]¬Broken(c) will be mapped to ¬Broken(c, do(repair(c), S0)). So ES formulas can be thought of as �situation-suppressed� (in situationcalculus terminology) and the ∗ mapping restores the situation argument to the �uents, leaving the rigids unchanged.

3 We assume that this language has functional and relational �uents, functions and predicates that are not �uents, the distinguished constant S0, function do, predicates ⊑, Poss and SF, and a two-place predicate K for knowledge. We take Knows(α, σ) in the situation calculus as an abbreviation for the formula ∀s(K(s, σ) ⊃ αnow s ), where αnow s is the result of replacing by s in α every occurrence of now that is not within the scope of a further Knows.

More precisely, we have the following:

Definition 3.1 Let α be any term or formula of ES without standard names. The expression α∗ is defined as α[S0] where, for any situation term σ, α[σ] is defined inductively by:

1. v[σ], where v is a first-order variable, is v;
2. g(t1, . . . , tk)[σ], where g is a rigid function, predicate, or second-order variable, is g(t1[σ], . . . , tk[σ]);
3. f(t1, . . . , tk)[σ], where f is a fluent function, predicate, or second-order variable is f(t1[σ], . . . , tk[σ], σ);
4. (t1 = t2)[σ] is (t1[σ] = t2[σ]);
5. ([t]α)[σ] is α[do(t[σ], σ)];
6. (α ∧ β)[σ] is (α[σ] ∧ β[σ])
7. (¬α)[σ] is ¬α[σ];
8. (∀v. α)[σ] is ∀v. α[σ];
9. (∀V. α)[σ] is ∀V. α[σ].
10. (□α)[σ] is ∀s′ (σ ⊑ s′ ⊃ α[s′ ]);
11. Know(α)[σ] is Knows(α[now], σ).

Note that the translation of □α introduces quanti�cation over situations, where the introduced variable s′ is assumed to be one that does not appear in situation term σ.

3.2 The situation-calculus axioms Υ

The axioms we assume in Υ are the following:

1. domain of objects is countably in�nite; 4
2. domain of actions is countably in�nite (as above);
3. equality is the identity relation: ∀x∀y. (x = y) ≡ ∀Q(Q(x) ≡Q(y)).
4. the K predicate: 5 ∀s(K(s, S0) ⊃ Ini(s)) ∧
5. ∀s′∀s.K(s′ , s) ≡ ∀P(. . . ⊃ P(s′ , s)), where the ellipsis stands for the universal closure of [K(s1, S0) ∧ Ini(s2) ⊃ P(s1, s2)] ∧ [P(s1, s2) ∧ SF(a, s1) ≡ SF(a, s2) ⊃ P (do(a, s1), do(a, s2))].

Axioms (1) and (2) talk about the cardinality of the set of objects and actions respectively: they are both countable and in�nite. The countability aspect is not very controversial. In the �rst-order case, every satis�able set of sentences is satis�able in a countable domain, and we do not expect users of the situation calculus to use second-order logic to defeat this. Note that this does not rule out having theories that talk about real numbers or other continuous phenomena; it simply rules out using second-order logic to force the interpretations of these theories to be uncountable. We can, however, imagine contexts where �niteness might be desirable. In such cases, we can introduce a new predicate O and instead of asserting that there are �nitely many objects, assert that there are �nitely many objects in O.

4 For space reasons, we omit the formula of second-order logic that �xes the cardinality of the domain of objects and actions.

5 We let Ini(t) be an abbreviation for the situation calculus formula ∀a∀s(t ̸= do(a, s)). In this version of the axiom, we ignore the correspondence between K and Poss.

Finally axiom (4) is a second order de�nition of the K predicate in terms of the value it has at S0. This is just another way of capturing the successor state axiom for K introduced by Scherl and Levesque [2003], and the added machinery to make Knows be a weak-S5 operator [Hughes and Cresswell, 1968]. Other knowledge operators are possible in the situation calculus, but weak-S5 and its extensions (such as strong-S5) are the most often used.

As for axiom (3), it is hard imagining anyone taking the negation of this one seriously. The usual �rst-order axiomatization of equality is often enough, but the intent is invariably for the equality symbol to be understood as the identity relation, which this second-order axiom ensures.

3.3 The embedding theorem

What we show is that provided certain properties hold between a Tarski structure on one side and an epistemic state, and a collection of worlds on the other, sentences will be true in ES iff their translations are true in the Tarski structure.

Let Mbe a Tarski structure for the situation calculus over the domain D = Dsit ∪ Dact ∪ Dobj , with Dini ⊆ Dsit as the set of initial situations, and with ι0 = SM 0 ∈ Dini . Let e be an epistemic state, and assume that we are given three mappings ω ∈ [Dini → W], θ ∈ [N → Dact ∪ Dobj ], and π ∈ [Z × Dini → Dsit ]. These mappings need to satisfy various consistency properties that we cannot enumerate here. But we can at least quote the lemma that uses them:

Lemma 3.2 Let α be a formula of ES with no standard names and whose free variables are among x1, . . . , xm. Then, given the consistency properties, for any variable map µ, the ES variable map uµ (defined in terms of µ), any variable s, any z ∈ Z, any ι ∈ Dini , and w = ω(ι),

This is proved by a (long) induction on the structure of α. The main result is then the following:

Theorem 3.3 Let α be any sentence of ES without standard names. Then α is valid iff Σ∪Υ |=FOL α∗ .

Proof: (Sketch) First assume that α is not valid. Then there is an e, w0 such that e, w0 ̸|= α. We de�ne a Tarski structure M whose domain is D = Dobj ∪ Dact ∪ Dsit , where Dobj (resp. Dact ) is the set of standard names of objects (resp. actions), and Dsit = Z ×W. Then we de�ne =M, SM 0 , doM, ⊑M, KM, as well as the extension of every rigid and �uent predicate and function symbol using e and w0 in a way that ensures that M satis�es Σ ∪ Υ. Next, de�ne the mappings θ, π, and ω by letting θ(n) = n, and for any initial ι = (〈 〉, w), letting π(z, ι) = (z, w), and ω(ι) = w. This ensures that the properties needed for Lemma 3.2 are satis�ed, and therefore M ̸|= α∗ . Consequently, Σ ∪ Υ ̸|=FOL α∗ .

Conversely, assume that Σ ∪ Υ ̸|=FOL α∗ . Then there is a Tarski structureM that satis�es Σ∪Υ but such that M ̸|= α∗ . The domain D must be Dsit ∪ Dact ∪ Dobj , with Dini ⊆ Dsit as the set of initial situations, and with ι0 = SM 0 ∈ Dini . Since M |= Υ, both Dobj and Dact are countably in�nite, Dobj = {δ1, δ2, . . .}, and Dact = {λ1, λ2, . . .}. We de�ne θ to map the i-th standard name for objects to δi and analogously for actions. We then de�ne π using doM, and ω using the extensions of the function and predicate symbols given by M. Finally, we let e = {ω(ι) | (ι, ι0) ∈ KM}, and w0 = ω(ι0). These ensure that the properties needed for Lemma 3.2 are satis�ed, and so e, w0 ̸|= α. Consequently, α is not valid.

4 The expressiveness of the language

Now that we have established that ES is actually a disguised fragment of the situation calculus, we next consider the expressiveness of this fragment, starting with a simple example problem, adapted from [Levesque and Lakemeyer 2001].

Imagine a robot that lives in a 1-dimensional world, and that can move towards or away from a �xed wall. The robot also has a sonar sensor that tells it when it gets close to the wall, say, less than 10 units away. See Figure 1. So we might imagine three actions, forward and backward which move the robot one unit towards and away from the wall, and a sonar sensing action which tells the robot if it is close to the wall. Each of these is a rigid constant, but for simplicity, we will simply assume that they are standard names. We have a single �uent, distance, which gives the actual distance from the robot to the wall. We can use Close as an abbreviation for the formula �distance < 10.� 6 We begin our formalization by writing preconditions for the three actions:

∀a□Poss(a) ≡ a = forward ∧ distance > 0 ∨ a = backward ∧ TRUE ∨ a = sonar ∧ TRUE.

Next, we de�ne the sensing results for the actions:

∀a□SF(a) ≡ a = forward ∧ TRUE ∨ a = backward ∧ TRUE ∨

6 Here and below, we use simple arithmetic involving <, +, and -, which can easily be de�ned in second-order terms with the standard names acting as natural numbers. We omit the details.

• a = sonar ∧ Close.

Finally, we write a successor state axiom for our only �uent:

a = forward ∧ distance = x+1 ∨ a = backward ∧ distance = x-1 ∨

• a ̸= forward ∧ a ̸= backward ∧ distance = x.

Now we are ready to consider some speci�cs having to do with what is true initially by de�ning an action theory Σ. Let φ denote the conjunction of the sentences above. We assume that φ is true and the robot knows it. We also assume the robot is located initially 6 units away from the wall, but that the robot has no idea where it is. So, we let Σ be

{φ, Know(φ), distance = 6, ∀x¬Know(distance ̸= x)}, and we get this:

Theorem 4.1 The following are logical entailments of Σ:

1. Close ∧ ¬Know(Close) ∧ [forward] ¬Know(Close) the robot is close to the wall, but does not know it, and continues not to know it after moving forward;
2. [sonar] (Know(Close) ∧ [forward]Know(Close)) after reading the sonar, the robot knows it is close, and continues to know it after moving forward;
3. [sonar] [backward] ¬Know(Close) after reading the sonar and then moving backward, the robot no longer knows that it is close to the wall;
4. [backward] [sonar] Know(Close) after moving backward and then reading the sonar, the robot knows that it is close to the wall;
5. [sonar] [forward] [backward] Know(Close) after reading the sonar, moving forward, and then backward, the robot knows that it is still close to the wall;
6. [sonar] Know([forward] Close)

main close after moving forward;

after reading the sonar, the robot knows that it will re-

1. ¬Know([sonar] Know(Close)) the robot does not know initially that it will know that it
2. is close after reading the sonar;
3. Know([sonar] (Know(Close) ∨Know(¬Close))) the robot does know initially that after reading the sonar, it will then knowwhether or not it is close to the wall;
4. Know([sonar] [backward] ¬Know(Close)) the robot knows initially that it will not know that it is close after reading the sonar and moving backwards.

Proof: The proofs of these are similar. Here we will only do item 3. Let z = 〈sonar · backward〉, and suppose that e, w |= Σ; we must show that e, w, z |= ¬Know(Close). Because e, w |= ¬Know(distance ̸= 9), there exists w′ ∈ e such that w′ ≃〈 〉 w and w′ [distance, 〈 〉] = 9. Since 9 < 10, we also have that w′ ≃z w. However, w′ [distance, z] = 10. So there exists w′ ∈ e such that w′ ≃z w and w′ , z |= ¬Close. Therefore, e, w, z |= ¬Know(Close).

Although we will not attempt to formulate a theorem here, it should be clear from this example that any basic action theory [Reiter 2001a] including those involving the Scherl-Levesque knowledge operator can be expressed in ES.

4.1 The Do operator

We now turn our attention to the Do operator which is the basis of the Golog language [Levesque et al. 1997], and show that a variant of Do can be represented in ES. We cannot encode Do(δ, s, s′ ) directly since we do not have situations as terms. Instead we will use D˜o(δ, α) which intuitively means that α holds after doing Golog program δ. There are two possible readings: one says that α holds in all �nal states, and the other says that α holds in some �nal state. They can be interde�ned, so we consider only the latter. We treat D˜o(δ, α) as an abbreviation for a formula of ES, de�ned recursively on the δ as follows:

1. for any action a, D˜o(a, α) def = (Poss(a) ∧ [a]α);
2. D˜o(φ?, α) def = (φ ∧ α);
3. D˜o(δ ; δ′ , α) def = D˜o(δ, D˜o(δ′ , α));
4. D˜o(δ | δ′ , α) def = (D˜o(δ, α) ∨ D˜o(δ′ , α));
5. D˜o(πx. δ, α) def = ∃x. D˜o(δ, α);
6. D˜o(δ∗ , α) def = ∀P. {□(α ⊃ P ) ∧ □(D˜o(δ, P ) ⊃ P )} ⊃ P .

As usual, we can de�ne while-loops and if-then-else as abbreviations. The main theorem that we state here is that this account of D˜o is correct relative to the original account of Do and the mapping from ES de�ned above:

Theorem 4.2 Let δ be any program, α be any sentence of ES, and σ be any situation term of the situation calculus.

This is proved by induction over δ, the only troublesome case being for the nondeterministic iteration, δ ∗ .

5 Mapping from the situation calculus

When mapping the situation calculus into ES, the main issue is the treatment of quanti�ed situations. While simple formulas can be translated using the inverse of ∗ from Section 3, a sentence like ∀s∃s′ .s ⊑ s′ ∧ (s ̸= s′ ) ∧F (s) ≡ F (s′ ), which says that from every situation another situation is reachable that agrees on the truth value of F, has no counterpart in ES.

To deal with situation-calculus sentences like these, our proposal is to encode action sequences in second-order ES. Let nil be a (rigid) constant and seq a (rigid) binary function symbol of ES. We de�ne ActionSeq(x) as an abbreviation for

In the situation calculus, a �uent like F(do(α, do(β, S0))) actually means that F holds after doing β then α. So the actions are in reverse order in a situation term. It is therefore useful to be able to reverse a sequence as follows:

Definition 5.1 Rev(x, y) def = ∀R(. . . ⊃ R(x, nil, y)), where the ellipsis stands for the universal closure of

Next we de�ne what it means for a formula α to be true after a sequence of actions.

Definition 5.2 After(s, α) def = ∀P.(. . . ⊃ P(s)) where the ellipsis stands for the universal closure of

The �uent ¬Broken(do(repair, do(drop, S0))) will then be translated as After(seq(repair, seq(drop, nil)), ¬Broken). In order to deal with quanti�cation over situations, we de�ne ≤ as a relation over action sequences, similar to the situation calculus relation ⊑.

Definition 5.3 (x ≤ x′ ) def = ∀Q.(. . . ⊃ Q(x, x′ )) where the ellipsis stands for the universal closure of

The formula ∀s∃s′ .s ⊑ s′ ∧ (s ̸= s′ ) ∧ F(s) ≡ F(s′ ) of the situation calculus will then be translated as

The �nal problem we must deal with concerns unrestricted quanti�cation over initial situations. To simplify things, we restrict ourselves to SC r , the rooted situation calculus, where all situation quanti�cation is of the form ∀s. σ ⊑ s ⊃ α, for some situation term σ. Note that this is no restriction at all for the non-epistemic situation calculus, since ∀s.α is equivalent to ∀s.S0 ⊑ s ⊃ α. We handle the Knows operator separately.

The mapping from the situation calculus into ES begins with a mapping · from situation terms into sequences of actions in ES. We assume that there is a countably in�- nite set Vs of extra object variables in ES for this purpose. For any situation variable s, we assume that s· ∈ Vs and that · is 1-to-1 and onto wrt Vs when restricted to situation variables. We also have that S · 0 = now· = nil, and that do(a, s)· = seq(a, s· ). We extend · to formulas as follows:

To ease the translation, we assume that situation-calculus formulas are in the following normal form: all arguments of predicates and functions are variables; equality expressions have the form (x = t), where x is a variable and t is a term mentioning at most 1 function symbol. It is easy to show that every formula of SC r is equivalent to one in this normal form.

Definition 5.4 Let α be any formula of SC r in normal form. Then its translation into ES, α· , is defined inductively by:

1. G(x1, . . . , xk)· , where G is a rigid predicate or rigid second-order variable, is G(x1, . . . , xk);
2. F(x1, . . . , xk, s)· , where F is a fluent predicate or fluent second-order variable, is After(s· , F(x1, . . . , xk));
3. (x = g(x1, . . . , xk))· , where g is a rigid function, is (x = g(x1, . . . , xk));
4. (x = f(x1, . . . , xk, s))· , where f is a fluent function, is After(s· , x = f(x1, . . . , xk));
5. (s = σ)· is (s· = σ· );
6. (σ1 ⊑ σ2)· is (σ· 1 ≤ σ· 2 );
7. (¬α)· is ¬α· ;
8. (α ∧ β)· is α· ∧ β· ;
9. (∀x.α) is ∀x.α· for an object or action variable x;

1. (∀V.α)· is ∀V.α· for a second-order variable V ;
2. Knows(α, s)· is After(s· , Know(α· )).

To show correctness of the translation, we need two more axioms Ψ, which are the universal closure of the following:

Theorem 5.5 Let α be a sentence of SC r in normal form. Then Σ∪Υ |=FOL α iff Ψ |= α· .

6 RelatedWork

The situation calculus, which has been the sole focus of this paper, is of course not the only language for reasoning about action. Over the years, there have been many other proposals such as the event calculus [Kowalski and Sergot 1986], Sandewall's features and �uents [Sandewall 1994], the language A [Gelfond and Lifschitz 1993], or the �uent calculus [H¤olldobler and Schneeberger 1990], to name but a few. What distinguishes the situation calculus perhaps most from its alternatives is that it admits an elegant monotonic solution to the frame problem [Reiter 1991], which is shared by its close relative, the �uent calculus [Thielscher 1999]. However, the �uent calculus also has situation terms as part of the language and hence suffers from the same shortcomings which ES tries to address.

ES itself has much in common with dynamic logic [Pratt 1976; Harel 1984], which has also been applied to reasoning about action [Castilho, Gasquet, and Herzig 1999]. A new feature of ES, compared to dynamic logic, are quanti�ed modalities as in ∀a.[a]α, which are key in expressing successor state axioms, among other things.

Dynamic logic has been combined with epistemic logic [Herzig et al. 2000; Demolombe 2003]. In the language of [Herzig et al. 2000], it is possible to express things like [backward] [sonar] Know(Close) using an almost identical syntax and where Know also has a possible-world semantics. Despite such similarities, there are signi�cant differences, however. In particular, their language is propositional. Consequently, there is no quanti�cation over actions. Demolombe (2003) proposes an axiomatic translation of parts of the epistemic situation calculus into modal logic. While his modal language is �rst-order, he does not consider quanti�ed modalities.

Although they do not consider epistemic notions, the work by [Blackburn et al. 2001] is relevant as it reconstructs a version of the situation calculus in Hybrid Logic [Blackburn et al. 2001], a variant of modal logic which was inspired by the work on tense logic by Prior [Prior 1967]. In a sense, though, this work goes only part of the way as an explicit reference to situations within the logic is retained. To us this presents a disadvantage when moving to an epistemic extension. The problem is that the epistemic situation calculus requires us to consider uncountably many situations, which precludes a substitutional interpretation of quanti�cation.

7 Conclusion

In this paper, we have substantiated the claim made informally in a previous paper that ES is a fragment of the situation calculus that admits an intuitive possible-world semantics. We argued that this fragment is expressive enough to represent basic action theories by presenting a simple example involving the action, knowledge, and sensing of a robot. We also showed how a version of the Do operator of the Golog language could be accommodated within the language. Finally, we proved that by using second-order encodings of sequences, virtually all of the situation calculus can be represented in ES. So what we get out of ES is a tool with practically the same expressive power as the standard situation calculus, but which is much more amenable to analysis due to its simple semantic basis.

In work currently under way [Cla�en 2005], ES is used to simplify and extend results by Reiter on knowledge-based programs [Reiter 2001b]. There are also a number of directions for future research, but perhaps the most immediate would be to implement a new version of Golog based on ES and put it to work.

Acknowledgments

We thank the anonymous reviewers for their helpful comments.