BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-90-1343
       ENTRY:: September 14, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Action logic and pure induction
        TYPE:: Technical Report
      AUTHOR:: Pratt, Vaughan
        DATE:: November 1990
       PAGES:: 23
    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.
       NOTES:: [Adminitrivia V1/RAM/19940914]
         END:: STAN//CS-TR-90-1343