@INPROCEEDINGS{kr96,
AUTHOR        = {David Basin and Sean Matthews and Luca Vigano},
TITLE         = {Implementing Modal and Relevance Logics in a Logical Framework},
BOOKTITLE     = {Principles of Knowledge Representation and Reasoning,
Proceedings of the Fifth International Conference (KR'96),  Cambridge,
Massachusetts, November 5--8, 1996},
EDITORS       = {Luigia Carlucci Aiello, and Jon Doyle, and Stuart Shapiro},
YEAR          = {1996},
PAGES         = {386--397},
PUBLISHER     = {Morgan Kaufmann Publishers, Inc.},
ADDRESS       = {San Francisco, California},
ABSTRACT = {
We present a framework for machine implementation of both partial and
complete fragments of large families of non-classical logics such as modal,
relevance, and intuitionistic logics.  We decompose a logic
into two interacting parts, each a natural deduction system: a base
logic of labelled formulae, and a theory of labels characterizing the
properties of the Kripke models. 
Our approach is modular and supports uniform proofs of
correctness and proof normalization.  We have implemented our work
in the Isabelle Logical Framework. },
}