Item

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 but limits
the degree to which we can make use of extensions to the labelling algebra.