top

Labelled modal logics: Quantifiers

D. Basin, S. Matthews, and L. Viganò. Labelled modal logics: Quantifiers. Journal of Logic, Language, and Information, 7(3):237–263, 1998.

Download: [pdf] 

Abstract:

In previous work [J. Logic Comput. 7 (1997), no. 6, 685--717], we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4.2, KD45, and S5. Here we extend this approach to quantified modal logics, providing formalizations for logics with varying, increasing, decreasing, or constant domains. The result is modular with respect to both the properties of the accessibility relation in the Kripke frame and the way domains of individuals change between worlds. Our approach also has a modular metatheory; soundness, completeness and normalization are proved uniformly for every logic in our class. Finally, our work leads to a simple implementation of a modal logic theorem prover in a standard logical framework.

BibTeX: (download)

@ARTICLE{basin98:_label,
  author = {D. Basin and S. Matthews and L. Vigan{\`o}},
  title = {Labelled modal logics: Quantifiers},
  journal = {Journal of Logic, Language, and Information},
  year = {1998},
  volume = {7},
  pages = {237--263},
  number = {3},
  abstract = {
	In previous work [J. Logic Comput. 7 (1997), no. 6, 685--717], we
	gave an approach, based on labelled natural deduction, for formalizing
	proof systems for a large class of propositional modal logics that
	includes K, D, T, B, S4, S4.2, KD45, and S5. Here we extend this
	approach to quantified modal logics, providing formalizations for
	logics with varying, increasing, decreasing, or constant domains.
	The result is modular with respect to both the properties of the
	accessibility relation in the Kripke frame and the way domains of
	individuals change between worlds. Our approach also has a modular
	metatheory; soundness, completeness and normalization are proved
	uniformly for every logic in our class. Finally, our work leads to
	a simple implementation of a modal logic theorem prover in a standard
	logical framework. }
}

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