next up previous
Next: Deriving Counterfactuals Up: Useful Counterfactuals Previous: Relating State vectors to



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 tex2html_wrap_inline1458 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 tex2html_wrap_inline1642 , tex2html_wrap_inline1644 and tex2html_wrap_inline1646 , tex2html_wrap_inline1648 , and tex2html_wrap_inline1650 . We have fluents, tex2html_wrap_inline1652 , tex2html_wrap_inline1654 , tex2html_wrap_inline1656 for every skill sk. Our two skills are tex2html_wrap_inline1660 and tex2html_wrap_inline1662 .

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 tex2html_wrap_inline1458 , so that sentences containing tex2html_wrap_inline1458 are notations for sentences containing tex2html_wrap_inline1448 .


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 tex2html_wrap_inline1448 , the situation constant tex2html_wrap_inline1454 and the constant tex2html_wrap_inline1674 .

We now add our frame axioms for each fluent.


These are enough frame axioms to generate explanation closure axioms for every fluent.

next up previous
Next: Deriving Counterfactuals Up: Useful Counterfactuals Previous: Relating State vectors to

John McCarthy
Wed Jul 12 14:10:43 PDT 2000