@INPROCEEDINGS{kgc97,
AUTHOR        = {David Basin and Sean Matthews and Luca Vigano},
TITLE         = {A New Method for Bounding the Complexity of Modal Logics},
BOOKTITLE     = {Computational Logic and Proof Theory, 5th Kurt G{\"o}del
Colloquium},
EDITORS       = {Georg Gottlob and Alexander Leitsch and Daniele Mundici},
YEAR          = {1997},
PAGES         = {89--102}
PUBLISHER = "Springer-Verlag",
SERIES = {LNCS},
VOLUME = "1289",
ABSTRACT = {We present a new proof-theoretic approach to bounding the complexity 
of the decision problem for propositional modal logics.  We formalize 
logics in a uniform way as sequent systems and then restrict the 
structural rules for particular systems.  This, combined with an 
analysis of the accessibility relation of the corresponding Kripke 
structures, yields decision procedures with bounded space requirements.  
As examples we give O(n log n) procedures for the modal logics K and T.}
}