Dynamic Logic

0.0

Dynamic Logic is a formal system for reasoning about programs and it also enjoys the singular advantage of being strongly related to classical logic. Traditionally, this has meant formalizing correctness specifications are met by a particular program. This book presents a comprehensive introduction to Dynamic Logic (DL). It can be described as a blend of three complementary classical ingredients: first-order predicate logic, modal logic, and the algebra of regular events. These components merge to form a system of remarkable unity that is theoretically rich as well as practical. The text is divided into three parts: Part I reviews the fundamental concepts of logic and computability theory that are needed in the study of Dynamic Logic. Part II discusses Propositional Dynamic Logic and its variants, and Part III discusses First-Order Dynamic and its variants. Examples are provided throughout, and a collection of exercises and a short historical section are included at the end of each chapter. The book will be well suited for the students of computer science and those pursuing postgraduate courses in philosophy. Table of Contents Preface I: FUNDAMENTAL CONCEPTS 1. Mathematical Preliminaries 2. Computability and Complexity 3. Logic 4. Reasoning About Programs II: PROPOSITIONAL DYNAMIC LOGIC 5. Propositional Dynamic Logic 6. Filtration and Decidability 7. Deductive Completeness 8. Complexity of PDL 9. Nonregular PDL 10. Other Variants of PDL III: FIRST-ORDER DYNAMIC LOGIC 11. First-Order Dynamic Logic 12. Relationships with Static Logics 13. Complexity 14. Axiomatization 15. Expressive Power 16. Variants of DL 17. Other Approaches References Notation and Abbreviations Index