Labelled Non-Classical Logics

This title is printed to order. This book may have been self-published. If so, we cannot guarantee the quality of the content. In the main most books will have gone through the editing process however some may not. We therefore suggest that you be aware of this before ordering this book. If in doubt check either the author or publisher’s details as we are unable to accept any returns unless they are faulty. Please contact us if you have any questions.

The subject of this text 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. The text investigates the proof theory of certain systems, and shows them to possess structural properties such as normalization and the subformula property, which are exploited not only to establish advantages and limitations of the book’s approach with respect to related ones, but also to give, by means of a substructural analysis, a proof-theoretic method for investigating decidability and complexity of (some of) the logics considered. All the deduction systems in the book have been implemented in the generic theorem prover Isabelle, thus providing a simple and natural environment for interactive proof development.