General Invariance Proofs
- Special case Phi => always T
- T was invariant of [A]<x, y>
- T could be used as I in INV1.
- Generally Phi => always P
- P need not be invariant.
- Find invariant I => P
- Creativity is in finding I
- Invariance proof itself mechanical.
INV1 reduces temporal reasoning to ordinary (non-temporal) reasoning!
Author: Wolfgang Schreiner
Last Modification: May 14, 1998