Paper: On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems (at LICS 1986)

Authors: Johann A. Makowsky Ildikó Sain

Abstract

We show how to derive Leivant's characterization of Floyd-Hoare Logic in weak second order logic ([L85]) directly from Csirmaz's characterization of Floyd-Hoare logic in Nonstandard Logics of Programs ([Cs80]). Our method allows us to spell out the precise role of the comprehension axiom in weak second order logic. We then prove similar results for other program verification systems (suggested by Burstall and Pnueli) and identify exactly the comprehension axioms corresponding to those systems.

BibTeX

  @InProceedings{MakowskySain-OntheEquivalenceofW,
    author = 	 {Johann A. Makowsky and Ildikó Sain},
    title = 	 {On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {293--300},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }