Van Harmelen F., Lifschitz V., Porter B. Handbook of Knowledge Representation

Подождите немного. Документ загружается.

652 16. Situation Calculus

(16.6)handempty(do(stack(x, y), s)),

(16.7)on(u, v, do(stack(x, y), s)) ≡ (u = x ∧ v = y) ∨ on(u,v,s),

(16.8)clear(u, do(stack(x, y), s)) ≡ u = x ∨ (clear(u, s) ∧ u = y),

(16.9)ontable(u, do(stack(x, y), s)) ≡ ontable(u, s),

(16.10)holding(u, do(unstack(x, y), s)) ≡ u = x,

(16.11)¬handempty(do(unstack(x, y), s)),

(16.12)on(u, v, do(unstack(x, y), s)) ≡ on(u,v,s)∧¬(x = u ∧ y = v),

(16.13)clear(u, do(unstack(x, y), s)) ≡ u

= y ∨ (clear(u,

s) ∧ u = x),

(16.14)ontable(u, do(unstack(x, y), s)) ≡ ontable(u, s),

(16.15)holding(u, do(pickup(x), s)) ≡ u = x,

(16.16)¬handempty(do(pickup(x), s)),

(16.17)on(u, v, do(pickup(x), s)) ≡ on(u,v,s),

(16.18)clear(u, do(pickup(x), s)) ≡ clear(u, s) ∧ u = x,

(16.19)ontable(u, do(pickup(x), s)) ≡ ontable(u, s) ∧ x = u,

(16.20)holding(u, do(putdown(x), s)) ≡ holding(u, s) ∧ u = x,

(16.21)handempty(do(putdown(x), s)),

(16.22)on(u, v,

do(putdown(x

), s)) ≡ on(u,v,s),

(16.23)clear(u, do(putdown(x), s)) ≡ u = x ∨ clear(u, s),

(16.24)ontable(u, do(putdown(x), s)) ≡ u = x ∨ ontable(u, s).

Similarly, we can write the following axioms for our second version of the blocks

world domain.

(16.25)Poss(move(x, y), s) ≡ x = table ∧ clear(x, s) ∧ clear(y, s)

clear(u, do(move(x, y), s)) ≡

(16.26)u = table ∨ on(x,u,s)∨ (clear(u, s) ∧ u = y),

on(u, v, do(move(x, y), s)) ≡

(16.27)(x = u ∧ y = v) ∨ (on(u,v,s)∧ u = x).

16.2 The Frame, the Ramiﬁcation and the Qualiﬁcation Problems

The set of axioms (16.1)–(16.24) provides a complete logical characterization of the

effects of actions for our ﬁrst blocks world domain. For each action, it gives necessary

and sufﬁcient conditions for it to be executable in any situation, and fully speciﬁes

the effects of this action on every ﬂuent. Similarly, the set of axioms (16.25)–(16.27)

completely captures the effects of actions for our second blocks world domain.

However, there is something unsatisfying about these two sets of axioms. When

we informally described the effects of actions, we did not describe it this way. For

F. Lin 653

instance, we said that after stack(x, y) is performed, in the resulting new situation,

on(x, y) and handempty will be true, and holding(x) and clear(y) will no longer be

true. We did not have to say, for instance, that if y is initially on the table, it will still

be on the table. Many researchers believe that when people remember the effects of

an action, they do not explicitly store the facts that are not changed by the action,

rather they just remember the changes that this action will bring about. Consequently,

when we axiomatize an action, we should only need to specify the changes that will be

made by the action. But if we specify in our theory only the changes that an action will

make, there is then a problem of how to derivethose that are not changed by the action.

This problem was identiﬁed by McCarthy and Hayes [29] in 1969, and they called it

the frame problem. For our blocks world example, we can view the frame problem

as the problem of looking for an appropriate logic that when given, for example the

following so-called “effect axioms” about stack(x, y):

on(x, y, do(stack(x, y), s)),

clear(x, do(stack(x, y), s)),

¬clear(y, do(stack(x, y), s)),

handempty(do(stack(x, y), s)),

¬holding(x, do(stack(x, y), s)),

will derive a complete speciﬁcation of the effects of action stack(x, y), like what the

set of axioms (16.5)–(16.9) does in ﬁrst-order logic [21].

The frame problem is one of the most well-known AI problems, if not the most

well-known one, and a lot of work has been done on solving it. It motivated much

of the early work on nonmonotonic logic (see papers in [6] and Chapter 6). While

the problem was identiﬁed in the situation calculus, it shows up in other formalisms

like the event calculus (Chapter 17), temporal action logics (Chapter 18), and non-

monotonic causal logic (Chapter 19). In fact, the general consensus is that any formal-

ism for reasoning about change will have to deal with it.

McCarthy [27] initially proposed to solve the frame problem by the following

generic frame axiom:

(16.28)Holds(p, s) ∧¬abnormal(p,a,s)Holds(p, do(a, s))

with

the abnormality predicate abnormal circumscribed. Unfortunately, Hanks and

McDermott [10] showed that this approach does not work using by now the infamous

Yale Shooting Problem as a counterexample. This is a simple problem with three ac-

tions: wait (do nothing), load (load the gun), and shoot (ﬁre the gun). Their effects can

be axiomatrized by the following axioms:

(16.29)loaded(do(load, s)),

(16.30)loaded(s) ⊃ dead(do(shoot, s)).

Now suppose S

is a situation such that the following is true:

(16.31)¬loaded(S

) ∧¬dead(S

654 16. Situation Calculus

Hanks and McDermott showed that the circumscription of abnormal in the theory

{(16.28), (16.29), (16.30), (16.31)} with Holds allowed to vary has two models, one

in which

loaded(do(load,S

)) ∧ loaded(do(wait, do(load,S

))) ∧

dead(do(shoot, do(wait, do(load ,S

))))

is true as desired, and the other in which

loaded(do(load,S

)) ∧¬loaded(do(wait, do(load,S

))) ∧

¬dead (do(shoot, do(wait, do(load,S

))))

is true, which is counter-intuitive as the action wait, which is supposed to do nothing,

mysteriosly unloaded the gun.

For the next few years, the YSP motivated much of the work on the frame problem,

and the frame problem became the focus of the research on nonmonotonic reasoning.

In response to the problem, Shoham [37] proposed chronological minimization that

prefers changes at later times. Many other proposals were put forward (e.g. [13, 14, 2,

33, 21, 35, 15, 38, 24]).

The thrust of modern solutions to the frame problem is to separate the speciﬁcation

of the effects of actions from the tasks of reasoning about these actions. For instance,

given the effect axioms (16.29) and (16.30), one can obtain the following complete

speciﬁcation of the effects of the actions concerned:

loaded(do(load, s)),

dead(do(load,s)) ≡ dead(s),

loaded(do(shoot,s)) ≡ loaded(s),

dead(do(shoot,s)) ≡ loaded(s) ∨ dead(s),

loaded(do(wait,s)) ≡ loaded(s),

dead(do(wait,s))≡ dead(s).

Now given the initial state axiom (16.31), one can easily infer that dead(do(shoot,

do(wait, do(load,S

)))) holds.

This separation between the speciﬁcation of action theories and the tasks of rea-

soning under these theories can be done syntactically by distinguishing general effect

axioms like (16.29) from speciﬁc facts like (16.31) about some particular situations,

as in Reiter’s solution [33] that we shall describe next. It can also be done by encoding

general effect axioms in a special language using predicates like Caused,asinLin’s

causal theories of action [15] for solving the ramiﬁcation problem.

16.2.1 The Frame Problem—Reiter’s Solution

Based on earlier work by Pednault [31], Haas [9] and Schubert [36], Reiter [33, 34]

proposed a simple syntactic manipulation much in the style of Clark’s predicate com-

pletion [4] (see Chapter 7) that turns a set of effect axioms into a set of successor state

axioms that completely captures the true value of each ﬂuent in any successor situa-

tion. It is best to illustrate Reiter’s method by an example. Consider our ﬁrst blocks

world domain, and let us write down all the effect axioms:

F. Lin 655

(16.32)on(x, y, do(stack(x, y), s)),

(16.33)clear(x, do(stack(x, y), s)),

(16.34)¬clear(y, do(stack(x, y), s)),

(16.35)handempty(do(stack(x, y), s)),

(16.36)¬holding(x, do(stack(x, y), s)),

(16.37)¬on(x, y, do(unstack(x, y), s)),

(16.38)¬clear(x, do(unstack(x, y), s)),

(16.39)clear(y, do(unstack(x, y), s)),

(16.40)¬handempty(do(unstack(x, y), s)),

(16.41)holding(x, do(unstack(x, y), s)),

(16.42)ontable(x, do(putdown(x), s)),

(16.43)clear(x, do(putdown(x), s)),

(16.44)handempty(do(putdown(x), s)),

(16.45)¬holding

(x, do(putdown(x

), s)),

(16.46)¬ontable(x, do(pickup(x), s)),

(16.47)¬clear(x, do(pickup(x), s)),

(16.48)¬handempty(do(pickup(x), s)),

(16.49)holding(x, do(pickup(x), s)).

Now for each of these effect axioms, transform it into one of the following two forms:

γ(a, -x, s) ⊃ F(-x,do(a, s)),

γ(a, -x, s) ⊃¬F(-x,do(a, s)).

For instance, the effect axiom (16.32) can be transformed equivalently into the follow-

ing axiom:

a = stack(x, y) ⊃ on(x, y, do(a, s)),

and the effect axiom (16.34) can be transformed equivalently into the following axiom:

(∃y)a = stack(y, x) ⊃¬clear(x, do(a, s)).

Now for each ﬂuent F , suppose the following is the list of all such axioms so obtained:

(a, -x,s) ⊃ F(-x,do(a, s)),

···

(a, -x,s) ⊃ F(-x,do(a, s)),

−

(a, -x,s) ⊃¬F(-x,do(a, s)),

···

−

(a, -x,s) ⊃¬F(-x,do(a, s)).

656 16. Situation Calculus

Then under what Reiter called the causal completeness assumption, which says that

the above axioms characterize all the conditions under which action a causes F to

become true or false in the successor situation, we conclude the following successor

state axiom [33] for ﬂuent F :

(16.50)F(-x,do(a, s)) ≡ γ

(a, -x,s) ∨ (F (-x, s) ∧¬γ

−

(a, -x, s)),

where γ

(a, -x,s) is γ

(a, -x,s) ∨···∨γ

(a, -x,s), and γ

−

(a, -x,s) is γ

−

(a, -x,s) ∨

···∨γ

−

(a, -x,s).

For instance, for our ﬁrst blocks world, we can transform the effect axioms about

clear(x) into the following axioms:

(∃y.a = stack(x, y)) ⊃ clear(x, do(a, s)),

(∃y.a = unstack(y, x)) ⊃ clear(x, do(a, s)),

a = putdon(x) ⊃ clear(x, do(a, s)),

(∃y.a = stack(y, x)) ⊃¬clear(x, do(a, s)),

(∃y.a = unstack(x, y)) ⊃¬clear(x, do (a, s)),

a = pickup(x) ⊃¬clear(x, do(a, s)).

Thus we have the following successor state axiom for clear(x):

clear(x, do(a, s)) ≡

∃y.a = stack(x, y) ∨∃y.a = unstack(y, x) ∨

a = putdown(x) ∨ clear(x, s) ∧

¬[∃y.a =

stack(y

, x) ∨∃y.a = unstack(x, y) ∨ a = pickup(x)].

Once we have a successor state axiom for each ﬂuent in the domain, we will

then have an action theory that is complete in the same way as the set of axioms

(16.1)–(16.24) is.

This procedure can be given a semantics in nonmonotonic logics, in particular

circumscription [27] (see Chapter6). This in facthas been done by Lin and Reiter [19].

We should also mentionthat for this approach towork, when generating the succes-

sor state axiom (16.50) from effect axioms, one should also assume what Reiter called

the consistency assumption: the background theory should entail that ¬(γ

∧ γ

−

Once we have a set of successor state axioms, to reason with them we need the unique

names assumption about actions: for each n-ary action A:

A(x

,...,x

) = A(y

,...,y

) ⊃ x

= y

∧···∧x

= y

and for each distinct actions A and A



A(x

,...,x

) = A



,...,y

For more details, see [33, 34].

F. Lin 657

16.2.2 The Ramiﬁcation Problem and Lin’s Solution

Recall that the frame problem is about how one can obtain a complete axiomatization

of the effects of actions from a set of effect axioms that speciﬁes the changes that

the actions have on the world. Thus Reiter’s solution to the frame problem makes the

assumption that the given effect axioms characterize completely the conditions under

which an action can cause a ﬂuent to be true or false. However, in some action do-

mains, providing such a complete list of effect axioms may not be feasible. This is

because in these action domains, there are rich domain constraints that can entail new

effect axioms. To see how domain constraints can entail new effect axioms, consider

again the blocks world. We know that each block can be at only one location: either

being held by the robot’s hand, on another block, or on the table. Thus when action

stack(x, y) causes x to be on y, it also makes holding(x) false. The ramiﬁcation prob-

lem, ﬁrst discussed by Finger [5] in 1986, is about how to encode constraints like this

in an action domain, and how these constraints can be used to derive the effects of the

actions in the domain.

In the situation calculus, for a long time the only way to represent domain con-

straints was by universal sentences of the form ∀s.C(s). For example, the aforemen-

tioned constraint that a block can be (and must be) at only one location in the blocks

world can be represented by the following sentences:

holding(x, s) ∨ ontable(x, s) ∨∃y.on(x, y),

holding(x, s) ⊃¬(ontable(x, s) ∨∃y.on(x, y)),

ontable(x, s) ⊃¬(holding(x, s) ∨∃y.on(x, y)),

(∃y.on(x, y)) ⊃¬(holding(x, s) ∨ ontable(x, s)).

So, for example, these axioms and the following effect axiom about putdown(x),

ontable(x, do(putdown(x), s))

will entail in ﬁrst-order logic the following effect axiom:

¬holding(x, do(putdown(x), s)).

However, domain constraints represented this way may not be strong enough for

determining the effects of actions. Consider the suitcase problem from [15]. Imagine

a suitcase with two locks and a spring loaded mechanism which will open the suitcase

when both of the locks are in the up position. Apparently, because of the spring loaded

mechanism, if an action changes the status of the locks, then this action may also

cause, as an indirect effect, the suitcase to open.

As with the blocks world, we can represent the constraint that this spring loaded

mechanism

gives rise to as the following sentence:

(16.51)up(L1,s)∧ up(L2,s) ⊃ open(s).

Although summarizing concisely the relationship among the truth values of the three

relevant propositions at any particular instance of time, this constraint is too weak to

describe the indirect effects of actions. For instance, suppose that initially the suitcase

is closed, the ﬁrst lock in the down position, and the second lock in the up position.

658 16. Situation Calculus

Suppose an action is then performed to turn up the ﬁrst lock. Then this constraint

is ambiguous about what will happen next. According to it, either the suitcase may

spring open or the second lock may get turned down. Although we have the intuition

that the former is what will happen, this constraint is not strong enough to enforce that

because there is a different mechanism that will yield a logically equivalent constraint.

For instance, a mechanism that turns down the second lock when the suitcase is closed

and the ﬁrst lock is up will yield the following logically equivalent one:

up(L1,s)∧¬open(s) ⊃¬up(L2,s).

So to faithfully represent the ramiﬁcation of the spring loaded mechanism on

the effects of actions, something stronger than the constraint (16.51) is needed. The

proposed solution by Lin [15] is to represent this constraint as a causal constraint:

(through the spring loaded mechanism) the fact that both of the locks are in the up

position causes the suitcase to open. To axiomatize this, Lin introduced a ternary

predicate Caused(p,v,s), meaning that ﬂuent p is caused to have truth value v in

situation s. The following are some basic properties of Caused [15]:

(16.52)Caused(p, true,s)⊃ Holds(p, s),

(16.53)Caused(p, false,s)⊃¬Holds(p, s),

(16.54)true = false ∧ (∀v)(v = true ∨ v = false),

where v is a variable ranging over a new sort truthValues.

Let us illustrate how this approach works using the suitcase example. Suppose that

ﬂip(x) is an action that ﬂips the status of the lock x. Its direct effect can be described

by the following axioms:

(16.55)up(x, s) ⊃ Caused(up(x), false, do(ﬂip(x), s)),

(16.56)¬up(x

, s) ⊃ Caused(up(x), true, do(ﬂip(x), s)).

Assume that L1 and L2 are the two locks on the suitcase, the spring loaded mechanism

is now represented by the following causal rule:

(16.57)up(L1,s)∧ up(L2 ,s) ⊃ Caused(open, true,s).

Notice that this causal rule, together with the basic axiom (16.52) about causality,

entails the state constraint (16.51). Notice also that the physical, spring loaded mech-

anism behind the causal rule has been abstracted away. For all we care, it may just as

well be that the device is not made of spring, but of bombs that will blow open the

suitcase each time the two locks are in the up position. It then seems natural to say

that the ﬂuent open is caused to be true by the fact that the two locks are both in the up

position. This is an instance of what has been called static causal rules as it mentions

only one situation. In comparison, causal statements like the effect axioms (16.55) and

(16.56) are dynamic as they mention more than one situations.

The above axioms constitute the starting theory for the domain. To describe fully

the effects of the actions, suitable frame axioms need to be added. Using predicate

Caused, a generic frame axiom can be stated as follows [15]: Unless caused otherwise,

a ﬂuent’s truth value will persist:

(16.58)¬(∃v)Caused(p, v, do(a, s)) ⊃[Holds(p, do(a, s)) ≡ Holds(p, s)].

F. Lin 659

For this frame axiom to make sense, one needs to minimize the predicate Caused.

Technically this is done by circumscribing Caused in the above set of axioms with

all other predicates (Poss and Holds) ﬁxed. However, given the form of the axioms,

this circumscription coincides with Clark’s completion of Caused, and it yields the

following causation axioms:

Caused(open,v,s) ≡

(16.59)v = true ∧ up(L1,s)∧ up(L2,s),

Caused(up(x), v, s) ≡

v = true ∧ (∃s



)[s = do(ﬂip(x), s



) ∧¬up(x, s



)]∨

(16.60)v = false ∧ (∃s



)[s = do(ﬂip(x), s



) ∧ up(x, s



)].

Notice that these axioms entail the two direct effect axioms (16.55), (16.56) and the

causal rule (16.57).

Having computed the causal relation, the next step is to use the frame axiom

(16.58) to compute the effects of actions. It is easy to see that from the frame ax-

iom (16.58) and the two basic axioms (16.52), (16.53) about causality, one can infer

the following pseudo successor state axiom:

Holds(p, do(a, s)) ≡

Caused(p, true, do(a, s)) ∨

(16.61)Holds(p, s) ∧¬Caused(p, false, do(a, s)).

From this axiom and the causation axiom (16.60) for the ﬂuent up, one then obtains

the following real successor state axiom for the ﬂuent up:

up(x, do(a, s)) ≡

(a = ﬂip(x) ∧¬up(x, s)) ∨ (up(x, s) ∧ a = ﬂip(x)).

Similarly for the ﬂuent open,wehave

open(do(a, s)) ≡

[up(L1, do(a, s)) ∧ up(L2, do(a, s))]∨open(s).

Now from this axiom, ﬁrst eliminating up(L1, do(a, s))

and up(L2, do(a

, s)) using

the successor state axiom for up, then using the unique names axioms for actions, and

the constraint (16.51) which, as we pointed out earlier, is a consequence of our axioms,

we can deduce the following successor state axiom for the ﬂuent open:

open(do(a, s)) ≡ a = ﬂip(L1) ∧¬up(L1,s)∧ up(L2,s)∨

a = ﬂip(L2) ∧¬up(L2,s)∧ up(L1,s)∨

open(s).

Obtaining these successor state axioms solves the frame and the ramiﬁcation problems

for the suitcase example.

Lin [15] showed that this procedure can be applied to a general class of action

theories, and Lin [18] described an implemented system that can compile these causal

660 16. Situation Calculus

action theories into Reiter’s successor state axioms and STRIPS-like systems, and

demonstrated the effectiveness of the system by applying it to many benchmark AI

planning domains.

16.2.3 The Qualiﬁcation Problem

Finally, we notice that so far we have given the condition for an action a to be exe-

cutable in a situation s, Poss(a, s), directly. It can be argued that this is nota reasonable

thing to do. In general, the executability of an action may depend on the circum-

stances where it is performed. For instance, we have deﬁned Poss(putdown(x), s) ≡

holding(x, s). But if the action is to be performed in a crowd, then we may want to

add that for the action to be executable, the robot’s hand must not be blocked by some-

one; and if the robot is running low on battery, then we may want to ensure that the

robot is not running out of battery; etc. It is clear that no one can anticipate all these

possible circumstances, thus no one can list all possible conditions for an action to be

executable ahead of time. This problem of how best to specify the precondition of an

action is called the qualiﬁcation problem [26].

One possible solution to this problem is to assume that an action is always exe-

cutable unless explicitly ruled out by the theory. This can be achieved by maximizing

the predicate Poss, or in terms of circumscription, circumscribing ¬Poss. If the axioms

about Poss all have the form

Poss(A, s) ⊃ ϕ(s),

that is, the user always provides explicit qualiﬁcations to an action, then one can com-

pute Poss by a procedure like Clark’s predicate completion by rewriting the above

axiom as:

¬ϕ(s) ⊃¬Poss(A, s).

The problem becomes more complex when some domain constraints-like axioms can

inﬂuence Poss. This problem was ﬁrst recognized by Ginsberg and Smith [7], and

discussed in more detailed by Lin and Reiter [19]. For instance, we may want to add

into the blocks world a constraint that says “only yellow blocks can be directly on

the table”. Now if the robot is holding a red block, should she put it down on the

table? Probably she should not. This means that this constraint has two roles: it rules

out initial states that do not satisfy it, and it forbids agents to perform any action that

will result in a successor situation that violates it. What this constraint should not do

is to cause additional effects of actions. For instance, it should not be the case that

putdown(x) would cause x to become yellow just to maintain this constraint in the

successor situation.

Lin and Reiter [19] called those constraints that yield indirect effects of actions

ramiﬁcation constraints, and those that yield additional qualiﬁcations of actions qual-

iﬁcation constraints. They are both represented as sentences of the form ∀s.C(s), and

it is up to the user to classify which category they belong to.

A uniform way of handling these two kinds of constraints is to use Lin’s causal

theories of actions as described above. Under this framework, only constraints repre-

sented as causal rules using Caused can derive new effects of actions, and ordinary

situation calculus sentences of the form ∀s.C(s) can only derive new qualiﬁcations on

F. Lin 661

actions. However, for this to work, action effect axioms like (16.55) need to have Poss

as a precondition:

Poss(ﬂip(x), s) ⊃[up(x, s) ⊃ Caused(up(x), false, do(ﬂip(x), s))],

and the generic frame axiom (16.58) need to be modiﬁed similarly:

Poss(a, s) ⊃{¬(∃v)Caused(p, v, do(a, s)) ⊃

[Holds(p, do(a, s)) ≡ Holds(p, s)]}.

In fact, this was how action effect axioms and frame axioms are represented in [15].

An interesting observation made in [15] was that some causal rules may give rise to

both new action effects and action qualiﬁcations. Our presentation of Lin’s causal the-

ories in the previous subsection has dropped Poss so that, in line with the presentation

in [34], the ﬁnal successor state axioms do not have Poss as a precondition.

16.3 Reiter’s Foundational Axioms and Basic Action Theories

We have deﬁned the situation calculus as a ﬁrst-order language with special sorts for

situations, actions, and ﬂuents. There are no axioms to constrain these sorts, and all

axioms are domain speciﬁc given by the user for axiomatizing a particular dynamic

system. We have used a binary function do(a, s) to denote the situation resulted from

performing a in s, thus for a speciﬁc ﬁnite sequence of actions a

,...,a

,wehave

a term denoting the situation resulted from performing the sequence of actions in s:

do(a

, do(a

k−1

,...,do(a

,s)...)). However, there is no way for us to say that one

situation is the result of performing some ﬁnite sequence of actions in another situa-

tion. This is needed for many applications, such as planning where the achievability

of a goal is deﬁned to be the existence of an executable ﬁnite sequence of actions that

will make the goal true once executed. We now introduce Reiter’s foundational axioms

that make this possible.

Brieﬂy, under Reiter’s foundational axioms, there is a unique initial situation, and

all situations are the result of performing some ﬁnite sequences of actions in this initial

situation. This initial situation will be denoted by S

, which formally is a constant of

sort situation.

It is worth mentioning here that while the constant S

has been used before to in-

formally stand for a starting situation, it was not assumed to be the starting situation

as under Reiter’s situation calculus. It can be said that the difference between Re-

iter’s version of the situation calculus and McCarthy’s original version is that Reiter

assumed the following foundational axioms that postulate the space of situations as a

tree with S

as the root:

(16.62)do(a, s) = do(a



) ⊃ a = a



∧ s = s



(16.63)∀P.[P(S

) ∧∀a, s.P (s) ⊃ P(do(a, s))]⊃∀sP (s).

Axiom (16.63) is a second-order induction axiom that says that for any property P ,to

prove that ∀s.P (s), it is sufﬁcient to show that P(S

), and inductively, for any situa-

tion s,ifP(s)then for any action a, P(do(a, s)). In particular, we can conclude that

• S

is a situation;