Proof-Theoretic analysis of modal logics
The PAnaMoL project aims at systematising proof theory for modal
logics.  We intend to provide a unified perspective on sequent-style
calculi and a deeper understanding of the general connections between
axiom systems and sequent-style calculi for such logics.  In detail
the research objectives are

- The systematic development of suitable syntactic characterisations
of classes of modal axioms corresponding to natural formats of rules
in different sequent-style frameworks (e.g. sequent, hypersequent,
nested sequent or display calculi) including algorithmic translations
from axioms to rules and back.

- A systematic comparison of the different sequent-style frameworks
according to their expressive strength.

- The exploitation of these results in the investigation of:
classification results stating necessary and sufficient
proof-theoretic strength for important examples of logics such as GL
and S5; uniform decidability and complexity results for large classes
of logics; general consistency proofs.

The research conducted in the project will be of relevance to
researchers in all fields where modal logics are used to model complex
phenomena and provide easy-to-use results and methods for the
proof-theoretic investigation and implementation of newly developed
modal logics.