Abstract
We have shown how our framework provides a basis for new proof-theoretical method for establishing decidability and bounding the complexity of some non-classical logics, and, as examples, we have given PSPACE decision procedures for the propositional modal logics K, T, K4 and S4. We establish these bounds by combining restrictions on the structural rules of our labelled sequent systems with an analysis of the accessibility relation of the corresponding Kripke frames. Furthermore, we have shown that as a by-product of our analysis we can obtain justifications (and in some cases refinements) of the rules of standard sequent systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Viganò, L. (2000). Discussion. In: Labelled Non-Classical Logics. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-3208-5_13
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3208-5_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4962-2
Online ISBN: 978-1-4757-3208-5
eBook Packages: Springer Book Archive