From Axioms to Rules — The Factory of Modal Proof Systems

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.

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

• Monday, August 15:
  
  
  • 01: Syntax and semantics of modal logic (slides)
  
  
  • 02: Sequent calculus (slides)


• Tuesday, August 16:
  
  
  • 03: First order logic (slides)
  
  
  • 04: Focusing (slides)


• Wednesday, August 17:
  
  
  • 05: Synthetic rules and bipoles (slides)
  
  
  • 06: Exercises


• Thursday, August 18:
  
  
  • 07: Labelled sequents (slides)
  
  
  • 08: Synthetic rules in labelled sequents (slides)
  
  
• Friday, August 19:
  
  
  • 09: Path logics (slides)
  
  
  • 10: Nested sequents (slides)

Main ESSLLI 2022 webpage

ESSLLI 2022 webpage for this course