Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics (Q687278)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics |
scientific article |
Statements
Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics (English)
0 references
28 November 1993
0 references
It is shown that there exists a data theory, a program \(P\) and a formula \(\psi\) such that using Peano Arithmetic it is possible to show partial correctness of \(P\) w.r.t. \(\psi\), while this cannot be done using Presburger Arithmetic, so that it is sometimes needed to allow multiplication of time points in program verification. Also, connections with dynamic and temporal logics are discussed.
0 references
temporal logic
0 references
dynamic logic
0 references
data theory
0 references
Peano Arithmetic
0 references
partial correctness
0 references
Presburger Arithmetic
0 references
multiplication of time points
0 references
program verification
0 references
0 references
