 Later Pratt and Harel generalized Hoare logic to dynamic logic (Pratt 1976, Pratt 1979a, Harel 1979, Harel 1984, Kozen and Tiuryn 1990, Harel et al. 2000), of which it was   realized[1]  that it is in fact a form of modal logic, by viewing the input-output relation of a program \(S\) as an accessibility relation in the sense of Kripke-style   semantics.[2]  A Hoare triple \(\left\{P\right\}S\left\{Q\right\}\) becomes in dynamic logic the following formula: \(P \rightarrow[S] Q\), where [\(S\)] is the modal box operator associated with (the accessibility relation associated with) the input-output relation of program \(S\). The propositional version of Dynamic Logic, PDL, was introduced by Fischer and Ladner (1977), and became an important topic of research in itself. The key axiom of PDL is the induction axiom