PAnaMoL · Proof-theoretic Analysis of Modal Logics

The PAnaMoL project aims at systematising proof theory for modallogics. We intend to provide a unified perspective on sequent-stylecalculi and a deeper understanding of the general connections betweenaxiom systems and sequent-style calculi for such logics. In detailthe research objectives are- The systematic development of suitable syntactic characterisationsof classes of modal axioms corresponding to natural formats of rulesin different sequent-style frameworks (e.g. sequent, hypersequent,nested sequent or display calculi) including algorithmic translationsfrom axioms to rules and back.- A systematic comparison of the different sequent-style frameworksaccording to their expressive strength.- The exploitation of these results in the investigation of:classification results stating necessary and sufficientproof-theoretic strength for important examples of logics such as GLand S5; uniform decidability and complexity results for large classesof logics; general consistency proofs.The research conducted in the project will be of relevance toresearchers in all fields where modal logics are used to model complexphenomena and provide easy-to-use results and methods for theproof-theoretic investigation and implementation of newly developedmodal logics.