Overview

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.

Full Product Details

Author:   Luca Viganò
Publisher:   Springer
Imprint:   Springer
Edition:   2000 ed.
Dimensions:   Width: 15.60cm , Height: 1.90cm , Length: 23.40cm
Weight:   1.360kg
ISBN:  

9780792377498

ISBN 10:   0792377494
Pages:   292
Publication Date:   31 January 2000
Audience:   College/higher education ,  Professional and scholarly ,  Undergraduate ,  Postgraduate, Research & Scholarly
Format:   Hardback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

1. Introduction.- I Labelled deduction for non-classical logics.- 2. Labelled Natural Deduction Systems for Propositional Modal Logics.- 3. Labelled Natural Deduction Systems for Propositional Non-Classical Logics.- 4. Labelled Natural Deduction Systems for Quantified Modal Logics.- 5. Encoding Labelled Non-Classical Logics in Isabelle.- 6. Labelled Sequent Systems for Non-Classical Logics.- 7. Discussion.- II Substructural and complexity analysis of modal sequent systems.- 8. Introduction and Preliminaries.- 9. Substructural Analysis of S(K).- 10. Substructural Analysis of S(T).- 11. Substructural Analysis of S(K4) and S(S4).- 12. Complexity of Proof Search in K, T, K4 and S4.- 13. Discussion.- 14. Conclusions and Further Research.- References.

Reviews

Author Information

Luca Viganò is an assistant professor at the Institute for Computer Science of the University of Freiburg (Germany). His research focuses on the theory and applications of non-classical logics, of proof development systems, of logical frameworks, and of logics for security.

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions