• Luca Viganò


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.


Modal Logic Decision Procedure Accessibility Relation Propositional Variable Relevance Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 2000

Authors and Affiliations

  • Luca Viganò
    • 1
  1. 1.Institut für InformatikAlbert-Ludwigs-Universität FreiburgFreiburg im BreisgauGermany

Personalised recommendations