LCS Publication Details
Publication Title: COMPUTABILITY AND COMPLETENESS IN LOGICS OF PROGRAMS
Publication Author: Harel, David
Additional Authors: Meyer, Albert R. and Pratt, Vaughan R.
LCS Document Number: MIT-LCS-TM-097
Publication Date: 2-1-1978
LCS Group: No Group Specified
Additional URL: No URL Given
Abstract:
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 a...”. This logic subsumes most existing first-order logics 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, including a II02-completeness result for the partial correctness theories of uninterpreted flowchart programs. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic.
To obtain this publication:

    To purchase a printed copy of this publication please contact MIT Document Services.