Report Number: CS-TR-90-1343
Institution: Stanford University, Department of Computer Science
Title: Action logic and pure induction
Author: Pratt, Vaughan
Date: November 1990
Abstract: In Floyd-Hoare logic, programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a --> b (had a then b) and postimplication b <-- a (b if-ever a). Unlike REG, ACT is finitely based, makes $a^*$ reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, ${(a --> a)}^*$ = a --> a.
http://i.stanford.edu/pub/cstr/reports/cs/tr/90/1343/CS-TR-90-1343.pdf