next up previous
Next: Actions Up: FORMALISM Previous: Fluents

Causality

 

We shall make assertions of causality by means of a fluent tex2html_wrap_inline727 where tex2html_wrap_inline419 is itself a propositional fluent. tex2html_wrap_inline731 asserts that the situation s will be followed (after an unspecified time) by a situation that satisfies the fluent tex2html_wrap_inline419 . We may use F to assert that if a person is out in the rain he will get wet, by writing:

displaymath739

Suppressing explicit mention of situations gives:

displaymath741

In this case suppressing situations simplifies the statement.

F can also be used to express physical laws. Consider the law of falling bodies which is often written

displaymath1026

together with some prose identifying the variables. Since we need a formal system for machine reasoning we cannot have any prose. Therefore, we write:

  equation94

Suppressing explicit mention of situations in this case requires the introduction of real auxiliary quantities v, h and tex2html_wrap_inline751 so that the sentence takes the following form:

  equation102

There has to be a convention (or declarations) so that it is determined that height(b), velocity(b) and time are fluents, whereas t, v, tex2html_wrap_inline751 and h denote ordinary real numbers.

tex2html_wrap_inline731 as introduced here corresponds to A. N. Prior's (1957, 1968) expression tex2html_wrap_inline769 .

The use of situation variables is analogous to the use of time-instants in the calculi of world-states which Prior (1968) calls U-T calculi. Prior provides many interesting correspondences between his U-T calculi and various axiomatizations of the modal tense-logics (that is, using this F-operator: see part 5). However, the situation calculus is richer than any of the tense-logics Prior considers.

Besides F he introduces three other operators which we also find useful; we thus have:

1. tex2html_wrap_inline731 . For some situation s' in the future of tex2html_wrap_inline787 holds.

2. tex2html_wrap_inline789 For all situations s' in the future of tex2html_wrap_inline787 holds.

3. tex2html_wrap_inline795 For some situations s' in the past of tex2html_wrap_inline787 holds.

4. tex2html_wrap_inline801 For all situations s' in the past of tex2html_wrap_inline787 holds.

It seems also useful to define a situational fluent tex2html_wrap_inline807 as the next situation s' in the future of s for which tex2html_wrap_inline813 holds. If there is no such situation, that is, if tex2html_wrap_inline815 , then tex2html_wrap_inline817 is considered undefined. For example, we may translate the sentence `By the time John gets home, Henry will be home too' as

displaymath819

Also the phrase `when John gets home' translates into

displaymath821

Though tex2html_wrap_inline817 will never actually be computed since situations are too rich to be specified completely, the values of fluents applied to tex2html_wrap_inline817 will be computed.


next up previous
Next: Actions Up: FORMALISM Previous: Fluents

John McCarthy
Mon Apr 29 19:20:41 PDT 1996