Paper: The Power of Temporal Proofs (at LICS 1987)

Authors: Martín Abadi

Abstract

Some methods to reason about concurrent programs and hardware devices have been based on proof systems for temporal logic. Unfortunately, all effective proof systems for temporal logic are incomplete for the standard semantics. We evaluate and compare the power of several proof systems for temporal logic. Specifically, we relate temporal systems to classical systems with explicit time parameters.
A usual temporal system turns out to be incomplete even for weak nonstandard semantics; we exhibit a short valid formula it fails to prove. We suggest the addition of new rules to define auxiliary predicates. With these rules, we obtain nonstandard completeness results. In particular, one of the simple temporal systems we describe is as powerful as Peano Arithmetic.

BibTeX

  @InProceedings{Abadi-ThePowerofTemporalP,
    author = 	 {Martín Abadi},
    title = 	 {The Power of Temporal Proofs},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {123--130},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }