@INPROCEEDINGS{GorankoHustadtSchmidtVakarelov04a,
AUTHOR = {Goranko, V. and Hustadt, U. and Schmidt, R. A. and Vakarelov, D.},
YEAR = {2004},
TITLE = {{SCAN} is Complete for All {S}ahlqvist Formulae},
EDITOR = {Berghammer, R. and M{\"o}ller, B. and Struth, G.},
BOOKTITLE = {Relational and {K}leene-Algebraic Methods in Computer Science (RelMiCS 7)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3051},
PUBLISHER = {Springer},
PAGES = {149--162},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/GorankoHustadtSchmidtVakarelov04a.html}},
ABSTRACT = {
SCAN is an algorithm for reducing monadic existential second-order logic
formulae to equivalent simpler formulae, often first-order logic
formulae.  It is provably impossible for such a reduction to first-order
logic to be always successful, even if there is an equivalent
first-order formula for a second-order logic formula.  In this paper we
show that SCAN successfully computes the first-order equivalents of all
Sahlqvist formulae in the classical (multi-)modal language.  
}
}