@ARTICLE{basin97:_label,
author = {D. Basin and M. Se{\'a}n and L. Vigan{\`o}},
title = {Labelled propositional modal logics: Theory and practice},
journal = {Journal of Logic and Computation},
year = {1997},
volume = {7},
pages = {685--717},
number = {3},
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, and 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 but limits the degree to
which we can make use of extensions to the labelling algebra. }
}