Computing with Modal Logic
Maarten de Rijke
The purpose of the course is to introduce the student to a
number of fundamental concepts and core intuitions in the area of
automated reasoning for modal logic.
No background in modal logic or automated reasoning is required.
- Lecture 1: Introduction. Basic modal
logic, multi-modal logic.
Semantics, bisimulations, tree model property,
- Lecture 2: Direct versus indirect
methods for automated reasoning
with modal logic. Translation-based approaches
exploiting state of the art
resolution-based theorem provers for first-order
logic. Termination and
- Lecture 3: More on translation-based
approaches. Ensuring termination: refinements of resolution and
- Lecture 4: Direct methods for automated
reasoning with modal logic. Tableaux-based calculi. Refinements,
optimizations, and comparisons with indirect approaches.
- Lecture 5: Exploiting tableaux for
different reasoning tasks. Model generation. Temporal model
checking with the logic CTL. State explosion problem. Efficient
representations of models.