@Article{BasinLPML97,
Author = "David Basin, Sean Matthews and Luca Vigano",
TITLE =  "Labelled Propositional Modal Logics: Theory and Practice",
JOURNAL       = {Journal of Logic and Computation},
YEAR          = 1997,
Volume        = 7,
Number        = 6,
pages={685--717},
ABSTRACT =  { 
		  We show how labelled deductive systems can be combined
		  with a logical framework to provide a natural
		  deduction implementation of a large and well-known
		  class of propositional modal logics (including $K$,
		  $D$, $T$, $B$, $S4$, $S4.2$, $KD45$, $S5$). Our
		  approach is modular and based on a separation between
		  a base logic and a labelling algebra, which interact
		  through a fixed interface. While the base logic stays
		  fixed, different modal logics are generated by
		  plugging in appropriate algebras. This leads to a
		  hierarchical structuring of modal logics with
		  inheritance of theorems. Moreover, it allows modular
		  correctness proofs, both with respect to soundness and
		  completeness for semantics, and faithfulness and
		  adequacy of the implementation. We also investigate
		  the tradeoffs in possible labelled presentations: We
		  show that a narrow interface between the base logic
		  and the labelling algebra supports modularity and
		  provides an attractive proof-theory (in comparision
		  to, e.g., semantic embedding) but limits the degree to
		  which we can make use of extensions to the labelling
		  algebra.}
}