Sciweavers

JELIA
1990
Springer

Action Logic and Pure Induction

14 years 4 months ago
Action Logic and Pure Induction
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 ab (had a then b) and postimplication ba (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, (aa) = aa.
Vaughan R. Pratt
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1990
Where JELIA
Authors Vaughan R. Pratt
Comments (0)