Viganò, Luca

A Framework for Non-Classical Logics

The subject of this work is the development and investigation of a
\emph{framework} for the modular and uniform representation and
implementation of \emph{non-classical logics}, in particular modal and
relevance logics. Logics are presented as labelled natural deduction
(or sequent) systems, which are proved to be sound and complete with respect
to the corresponding Kripke-style semantics. We investigate the proof
theory of our systems, and show them to possess structural properties such
as normalization and the subformula property, which we exploit to establish
not only general advantages and limitations of our approach with respect to
related ones, but also, by means of a substructural analysis, decidability
and complexity results for (some of) the logics we consider. All of our
proof systems have been implemented in the generic theorem prover
Isabelle, thus providing a simple and natural environment for
interactive proof development.