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

**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} }