This section presents a formalization of a skiing domain in the situation calculus. The major novelty of this domain is that it allows some reasoning about the actions of an agent. Normally, in the situation calculus all sequences of actions are considered. Here we look at what sequences would happen given some facts about our agent's beliefs and some rules about how he acts.
We include the notion of an actual time line picked out of the
possible time lines in the situation calculus. This follows Reiter
and Pinto [Pinto and Reiter, 1993]. We enrich this with a 
partial
function, that picks out the next actual situation.
We have five sorts, the usual situation, fluent and action sorts, plus sorts for terrain types and skills.
We have five actions 
, 
and 
, 
, and
. We have fluents, 
, 
, 
for
every skill sk. Our two skills are 
and 
.
We have that after his one lesson our hero knows how to bend his knees.
We now have some facts about what the actual time line is, given the state of the world, and the knowledge of our hero. If our hero sees a bump, and has learned to bend his knees, he will actually do so, otherwise he will actually fall. If he sees a turn, then he will put his weight on his downhill ski if he has learned to do that, otherwise he will actually fall. We also add that if he does the wrong thing, then he will fall, and add the results of falling etc.
These axioms are enough to pick out an actual timeline, of skiing Slope4, then carrying out an action that depends on the terrain of Slope4 and Junior's knowledge, and then waiting for ever.
We now state that after every actual situation there is a unique
actual situation, that picked out by Next. We take this to be the
definition of a partial function , so that sentences containing
are notations for sentences containing 
.
We also add that Slope4 is a turn.
We also need to add unique names, domain closure, and frame axioms.
We have as our unique names axioms, fully unique names, except for the
function , the situation constant 
and the constant
.
We now add our frame axioms for each fluent.
These are enough frame axioms to generate explanation closure axioms for every fluent.
