From Axioms to Rules — The Factory of Modal Proof Systems

ESSLLI 2022 Course — 2nd Week (15-19 August) — 9:00-10:30

Sonia Marin & Lutz Straßburger

Overview

Modal logics have emerged as versatile, tractable tool for reasoning about such disparate concepts as necessity, provability, obligation, time, space, knowledge, and belief. Many applications, including software and hardware verification, require special tailored modal logics, determined by selected axioms. To make efficient use of these logics, one needs analytic proof systems for deciding the problems of validity, satisfiability, etc. The purpose of this course is to make the student familiar with modern proof-theoretic methods such as focusing that allow us to construct inference rules from the axioms of a chosen logic.

This course is intended to be introductory. This means that only some familiarity with the basics of propositional Boolean logic is required.


Slides of the lectures (in handout form) appear here during the week.



Tentative syllabus

Five 90-minute lectures are split into ten 45-minute units.

Links

Main ESSLLI 2022 webpage

ESSLLI 2022 webpage for this course