@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.}
}