Welcome to the webpage of the course Dynamic Logic. The course is taught at the Faculty of Arts, Charles University in the fall semester 2025. The seminars take place Wednesdays 9:10–10:40 in room 116.
Course outline
The course introduces some logical methods for reasoning about equivalence and correctness of computer programs. We look at program semantics, Propositional Dynamic Logic and Kleene Algebra.
Instructors
Office hours: By appointment (email us).
Syllabus and materials
- 1. Programs and their semantics
1.1 A propositional logic of programs and its relational semantics (1.10.)
1.2 Trace semantics and its equivalence to relational semantics (8.10.)
1.3 Hoare logic (15.10.) -
2. Propositional Dynamic Logic
2.1 Modal logic - syntax and semantics (22.10.)
2.2 Modal logic - decidability via filtration and completeness via canonicity (29.10.)
2.3 PDL - syntax and semantics (5.11.)
2.4 PDL - decidability via filtration and completeness via finite canonical models (12.11.) - 3. Kleene algebra
Announcements
Stay tuned.
Reading
Besides the lecture notes, I suggest the following (more suggestions later):
- D. Blackubrn, M. de Rijke, Y. Venema: Modal Logic. Cambridge University Press, 2001.
- M. Huth and M. Ryan: Logic in Computer Science. Cambridge University Press, 2004.
- D. Harel, D. Kozen, J. Tiuryn: Dynamic Logic. MIT Press, 2000.
- T. Kappé: Elements of Kleene Algebra. Course at ESSLI 2023.
A useful tool for proving/disproving equations:
Grading
The pass/fail grade will be based on your solutions of three problem sets and on lecture attendance.