D. Harel First-Order Dynamic Logic, Lecture Notes in Computer Science, Vol. 68, Springer-Verlag, New York, 1979.
Part I: Binary-Relation Semantics
Part II: Computation-Tree Semantics
Appendix A: Example of a Proof of a DL-wff in P(N)
This is a research monograph intended primarily for those researchers in Theoretical Computer Science interested in the areas of logics of programs, programming language semantics and program verification. It is also aimed at mathematically-inclined researchers in Logic, Linguistics and Philosophy, interested in a well-motivated application of ideas from modal logic. The theory developed here, although deriving its motivation and part of its terminology from programming theory, can be viewed as a theory for reasoning about action in general; hence the term dynamic logic.
Dynamic Logic (DL) is covered on the first-order (rather than the propositional) level. Regular DL, context-free DL and versions of them for treating infinite computations (or actions) are defined and analyzed, and a complete proof theory is developed for proving that formulae of these logics are valid in arithmetical universes. Various notions of correctness of programs with respect to their specifications are investigated within the DL framework.
This monograph constitutes a revised version of the author's doctoral dissertation, submitted to the Department of Electrical Engineering and Computer Science of the Massachusetts Institute of Technology in May 1978.