@Article{BasinMatthewsVigano96e,
author        = {David Basin, Se{\'a}n Matthews and Luca Vigan{\`o}},
title         = {Natural Deduction for Non-Classical Logics},
journal       = {Studia Logica},
volume        = {60},
number        = {1},
pages         = {119--160},
year          = {1998},
note          = {Special issue on \emph{Natural Deduction} edited by
Frank Pfenning and Wilfried Sieg}, 
abstract      = {
We present a framework for machine implementation of families of
non-classical logics with Kripke-style semantics.  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.  By appropriate combinations we
capture both partial and complete fragments of large families of
non-classical logics such as modal, relevance, and intuitionistic
logics.  Our approach is modular and supports uniform proofs of
correctness and proof normalization.  We have implemented our work
in the Isabelle Logical Framework.
},
}