@incollection{mod-modal,
Author = {David Basin, Sean Matthews and Luca Vigano},
Title = {A Modular Presentation of Modal Logics in a Logical Framework},
Booktitle = {The Tbilissi Symposium on Logic, Language, and
		  Computation},
EDITOR = {J. Ginzburg and Z. Khasidashvili and C. Vogel and
		  J.-J. L\'evy},
PUBLISHER = {CSLI},
YEAR = 1998,
PAGES = {293--307},
BIBTYPE = {INCOLLECTION},		  
ABSTRACT = {
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.},
}