de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Labelled propositional modal logics: theory and practice

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44075

Basin,  David
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45002

Matthews,  Seán
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45670

Viganò,  Luca
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

1996-2-002
(Any fulltext), 11KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Basin, D., Matthews, S., & Viganò, L.(1996). Labelled propositional modal logics: theory and practice (MPI-I-1996-2-002). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-A40A-4
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.