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.