A Note on Equivalences Among Logics of Programs
Several different first order formal logics of programs -- Algoritmic Logic, Dynamic Logic, and Logic of Effective Definitions -- are compared and shown to be equivalent to a fragment of constructive L ω1ω. When programs are modelled as effective flowcharts, the logics of deterministic and nondeterm...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149022 |
| Summary: | Several different first order formal logics of programs -- Algoritmic Logic, Dynamic Logic, and Logic of Effective Definitions -- are compared and shown to be equivalent to a fragment of constructive L ω1ω. When programs are modelled as effective flowcharts, the logics of deterministic and nondeterministic programs are equivalent. |
|---|