Advanced Logic

• Intro to Modal Logic (operators, frames, models, tautologies)
• Semantics: truth and validity, game semantics for formula validity
• Bisimulations
• Model transformations (tree unravelling, bisimulation contraction)
• Formula validity using sequents and tableaux
• Standard translation: mapping basic modal logic to first-order predicate logic
• The finite model property
• Proof systems and derivation
• Temporal logic
• Multi-modal logic
• Program correctness
• Propositional dynamic logic (PDL)
• Epistemic logic

Worked exercises:

• Exercise 1: validity, game semantics (verifier/falsifier)
• Exercise 3: bisimulation game semantics, sequents, tableaux
• Exercise 4: derivation in proof systems, temporal logic
• Exercise 5: PDL
• Homework 1: misc topics
• Some midterm solutions: validity, bisimulation, definability in BML

Here’s my Anki deck

I drew the graphs on these pages with Graphviz, I used vim-literate-markdown’s tangling functionality to quickly extract graph code to separate files. You can install Graphviz and run e.g. dot < graph.dot -Tsvg > graph.svg (also accepts input files as parameters). Or you can install PlantUML, surround the code with @startdot...@enddot, and run plantuml -p -Tsvg < graph.puml > graph.svg.