PEANO ARITHMETIC AS AXIOMATIZATION OF THE TIME FRAME IN LOGICS OF PROGRAMS AND IN DYNAMIC LOGICS

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.