Abstract
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.