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.

• Type: Conference
• Year: 1990
• Where: JELIA
• Authors: Vaughan R. Pratt
• Keywords: Action Logic, Artificial Intelligence, Equational Theory, Equational Theory Reg, JELIA 1990