top

Labelled propositional modal logics: Theory and practice

D. Basin, M. Seán, and L. Viganò. Labelled propositional modal logics: Theory and practice. Journal of Logic and Computation, 7(3):685–717, 1997.

Download: [pdf] 

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.

BibTeX: (download)

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

Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33