B. Biro et I. Sain, PEANO ARITHMETIC AS AXIOMATIZATION OF THE TIME FRAME IN LOGICS OF PROGRAMS AND IN DYNAMIC LOGICS, Annals of pure and applied Logic, 63(3), 1993, pp. 201-225
We show that one can prove the partial correctness of more programs us
ing Peano's axioms for the time frames of three-sorted time models tha
n using only Presburger's axioms, that is it is useful to allow multip
lication of time points at program verification and in dynamic and tem
poral logics. We organized the paper as follows: 1. Preliminaries, 2.
The main result, 3. Peano arithmetic with bounded multiplication, 4. C
onnections with temporal logics and dynamic logics, Acknowledgements,
References.