top

Natural deduction for non-classical logics

D. Basin, S. Matthews, and L. Viganò. Natural deduction for non-classical logics. Studia Logica, 60(1):119–160, 1998.

Download: [pdf] 

Abstract:

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and proof normalization. We implement our work in the Isabelle logical framework.

BibTeX: (download)

@ARTICLE{basin98:_natur,
  author = {D. Basin and S. Matthews and L. Vigan{\`o}},
  title = {Natural deduction for non-classical logics},
  journal = {Studia Logica},
  year = {1998},
  volume = {60},
  pages = {119--160},
  number = {1},
  abstract = {
	We present a framework for machine implementation of families of non-classical
	logics with Kripke-style semantics. We decompose a logic into two
	interacting parts, each a natural deduction system: a base logic
	of labelled formulae, and a theory of labels characterizing the properties
	of the Kripke models. By appropriate combinations we capture both
	partial and complete fragments of large families of non-classical
	logics such as modal, relevance, and intuitionistic logics. Our approach
	is modular and supports uniform proofs of soundness, completeness
	and proof normalization. We implement our work in the Isabelle logical
	framework. }
}

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