Abstract:

A Modular Presentation of Modal Logics in a Logical Framework

David Basin and Seán Matthews and Luca Viganò


We present a theoretical and practical approach to the modular natural deduction presentation of modal logics 
and their implementation in a logical framework. Our work treats a large and well-known class of modal logics 
(including K, KD, T, B, S4, S4.2, S5) in a uniform way with respect to soundness and completeness for 
semantics, and faithfulness and adequacy of the implementation. Moreover, it results in a pleasingly simple 
and usable implementation of these logics.