Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 7, Issue 6: December 1997.

Labelled propositional modal logics: theory and practice

D Basin, S Matthews and L Viganò

Max-Planck-Institut fur Informatik, Im Stadtwald, D-66123 Saarbrucken, Germany. E-mail: {basin,sean,luca}@mpi-sb.mpg.de

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 presentation: 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.

Pages 685-717


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_07/Issue_06/070685.sgm.abs.html
Last modification: 16 April 1998.
Copyright© Oxford University Press, 1998.