×

Natural deduction for non-classical logics. (English) Zbl 0954.03010

Summary: 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 have implemented our work in the Isabelle Logical Framework.

MSC:

03B22 Abstract deductive systems
03B35 Mechanization of proofs and logical operations
03B60 Other nonclassical logic
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03F05 Cut-elimination and normal-form theorems

Software:

Isabelle
PDFBibTeX XMLCite
Full Text: DOI