No label defined (Q3975138)

[For the entire collection see Zbl 0726.00018.] In the framework of time-oriented nonstandard logics of programs, the authors characterize the reasoning powers of various established temporal logics used in computer science such as the Floyd-Hoare method, Intermittent Assertions method, Pnueli's temporal method and the inference system of dynamic logic. Then, based on an axiomatization of temporal logic with the five modalities First, Next, Always, ``Always-in- the-future'', and ``Always-in-the-past'', they are compared in connection with several properties on both deterministic and nondeterministic programs. The provability of temporal formulas in general is also discussed, that is, several completeness and incompleteness results on the logics axiomatized in that way are given.