1977 · 76 citations · 8 references
ComputingComputer ScienceMathematicsFormal MethodsLogicTheory Of ComputationAutomated ReasoningComputability TheoryFirst-order LogicHoare LogicMathematical LogicPredicate LogicComputational LogicDynamic LogicDynamic Logic ModelsFirst-order Logic ReasoningPartial CorrectnessProgram CorrectnessProgram LogicsTotal Correctness
Dynamic logic generalizes first‑order logic by replacing quantifiers with program execution phrases, subsuming most existing first‑order logics of programs such as Floyd’s, Hoare’s, and Manna–Waldinger’s, while remaining closer to classical first‑order logic than other program logics. The authors investigate the computational hardness of dynamic logic’s validity problem and explore possible axiomatizations. They establish Π02‑completeness for the validity problem of partial‑correctness theories of uninterpreted flowchart programs and prove completeness of a dynamic‑logic axiomatization relative to arithmetic.
Dynamic logic is a generalization of first order logic in which quantifiers of the form “for all χ...” are replaced by phrases of the form “after executing program α...”. 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 Π02-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.
8
An Introduction to Modal Logic.
G. D. Duthie, G. E. Hughes, M. J. Cresswell · The Philosophical Quarterly · 1971 · 197 citations
Humanities, Mathematics, Philosophy +12
Program Proving as Hand Simulation with a Little Induction.
R. M. Burstall · IFIP Congress · 1974 · 194 citations