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

Item

ITEM ACTIONSEXPORT

Released

Report

Natural deduction for non-classical logics

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-006
(Any fulltext), 11KB

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

Basin, D., Matthews, S., & Viganò, L.(1996). Natural deduction for non-classical logics (MPI-I-1996-2-006). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-9FE5-A
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 correctness and proof normalization. We have implemented our work in the Isabelle Logical Framework.