prattActionLogicPure1991:
  type: anthos
  title: Action logic and pure induction
  author: Pratt, Vaughan
  date: 1991
  editor:
  - Siekmann, J.
  - Goos, G.
  - Hartmanis, J.
  - Van Eijck, J.
  page-range: 97-120
  url:
    value: http://link.springer.com/10.1007/BFb0018436
    date: 2024-07-10
  serial-number:
    doi: 10.1007/BFb0018436
    isbn: 978-3-540-53686-4 978-3-540-46982-7
  note: 'Series Title: Lecture Notes in Computer Science'
  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.
  parent:
    type: anthology
    title: Logics in {AI}
    publisher:
      name: Springer Berlin Heidelberg
      location: Berlin, Heidelberg
    volume: 478