A Modular Presentation of Modal Logics in a Logical Framework
David Basin, Seán Matthews, Luca Viganò · 1998
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.