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.
- Lecture 1: Introduction. Basic modal
logic, multi-modal logic.
Semantics, bisimulations, tree model property,
decidability.
- 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
non-termination.
- Lecture 3: More on translation-based
approaches. Ensuring termination: refinements of resolution and
alternative translations.
- 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.
No background in modal logic or automated reasoning is required.