next up previous
Next: Formalizing Oscillations Up: Extensions of the formalism Previous: ``Branching time'' and ``linear

Induction in the situation calculus


Several kinds of mathematical induction seem to be required. For example, one may want to prove a proposition tex2html_wrap_inline1281 by showing that it is true for s and is preserved by the events that occur between s and tex2html_wrap_inline1287 . A related kind of induction is needed to prove that something is true for all situations arising in the operation of a buzzer. The simplest case of the tex2html_wrap_inline1123 induction might be to show that a block unmoved by each of a sequence of events is in the same position in tex2html_wrap_inline1291 .

The simplest situation calculus is Reiter's [Rei01]. The formula is


Here are two formulas


(47) is appropriate when tex2html_wrap_inline1291 is defined.

When tex2html_wrap_inline1291 is not defined, as in the buzzer case, we can use tex2html_wrap_inline1297 to mean that s' is a distant successor of s and have the axiom.


John McCarthy
Fri Feb 8 17:29:20 PST 2002