A Modular Presentation of Modal Logics in a Logical Framework

We present a theoretical and practical approach to the modular naturaldeduction presentation of modal logics and their implementationin a logical framework. Our work treats a large and well-known classof modal logics (including K, D, T , B, S4, S4:2, KD45, S5) in a uniformway with respect to soundness and completeness for semantics, andfaithfulness and adequacy of the implementation. Moreover, it resultsin a pleasingly simple and usable implementation of these logics./ 10.1...