View article

PDL is the propositional version of dynamic logic, and was defined by MJ Fischer and RE Ladner in [FL]"[to] play a role in the logic of programs analogous to the role the propositional calculus plays in the classical first order logic." They comment:" We have attempted to abstract from [work on logics of programs] the'pure'logical structure underlying these formal systems. We feel a thorough understanding of this structure is a prerequisite to obtaining a good grasp on the more complicated, albeit more applicable, systems, just as classical propositional logic is fundamental to the understanding of first-order predicate calculus." In this spirit, we preface our treatment of first-order DL with a definition of PDL.