Item

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