Computability and Completeness in Logics of Programs
Dynamic logic is a generalization of first order logic in which quantifiers of the form "for all X…" are replaced by phrases of the form "after executing program α…". This logic subsumes most existing first-order logic of programs that manipulate their environment, including Floy...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/148925 |
| _version_ | 1826196415259344896 |
|---|---|
| author | Harel, David Meyer, Albert R. Pratt, Vaughan R. |
| author_facet | Harel, David Meyer, Albert R. Pratt, Vaughan R. |
| author_sort | Harel, David |
| collection | MIT |
| description | Dynamic logic is a generalization of first order logic in which quantifiers of the form "for all X…" are replaced by phrases of the form "after executing program α…". This logic subsumes most existing first-order logic of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness, yet is more closely related to classical first-order logic than any other proposed logic of programs. We consider two issues: how hard is the validity problem for the formulae of dynamic logic, and how might one axiomatize dynamic logic? We give bounds on the validity problem for some special cases, include a π0/2-completeness result for the partial correctness theories of uninterpreted flowchart programs and a π1/1-completeness result for unrestricted dynamic logic. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic. |
| first_indexed | 2024-09-23T10:26:30Z |
| id | mit-1721.1/148925 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T10:26:30Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1489252023-03-30T04:01:49Z Computability and Completeness in Logics of Programs Harel, David Meyer, Albert R. Pratt, Vaughan R. Dynamic logic is a generalization of first order logic in which quantifiers of the form "for all X…" are replaced by phrases of the form "after executing program α…". This logic subsumes most existing first-order logic of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness, yet is more closely related to classical first-order logic than any other proposed logic of programs. We consider two issues: how hard is the validity problem for the formulae of dynamic logic, and how might one axiomatize dynamic logic? We give bounds on the validity problem for some special cases, include a π0/2-completeness result for the partial correctness theories of uninterpreted flowchart programs and a π1/1-completeness result for unrestricted dynamic logic. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic. 2023-03-29T14:09:44Z 2023-03-29T14:09:44Z 1978-02 https://hdl.handle.net/1721.1/148925 4802622 MIT-LCS-TM-097 application/pdf |
| spellingShingle | Harel, David Meyer, Albert R. Pratt, Vaughan R. Computability and Completeness in Logics of Programs |
| title | Computability and Completeness in Logics of Programs |
| title_full | Computability and Completeness in Logics of Programs |
| title_fullStr | Computability and Completeness in Logics of Programs |
| title_full_unstemmed | Computability and Completeness in Logics of Programs |
| title_short | Computability and Completeness in Logics of Programs |
| title_sort | computability and completeness in logics of programs |
| url | https://hdl.handle.net/1721.1/148925 |
| work_keys_str_mv | AT hareldavid computabilityandcompletenessinlogicsofprograms AT meyeralbertr computabilityandcompletenessinlogicsofprograms AT prattvaughanr computabilityandcompletenessinlogicsofprograms |