Abstract:

Labelled Non-Classical Logics

Luca Viganò


The subject of the book is the development and investigation of a framework for the modular and uniform 
presentation and implementation of non-classical logics, in particular modal and relevance logics. Logics are 
presented as labelled deduction 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 not only to establish 
advantages and limitations of our approach with respect to related ones, but also to give, by means of a 
substructural analysis, a new proof-theoretic method for investigating decidability and complexity of (some of) 
the logics we consider. All of our deduction systems have been implemented in the generic theorem prover 
Isabelle, thus providing a simple and natural environment for interactive proof development.