@INPROCEEDINGS{Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003, AUTHOR = {Goranko, Valentin and Hustadt, Ullrich and Schmidt, Renate and Vakarelov, Dimiter}, TITLE = {{SCAN} is complete for all Sahlqvist formulae}, BOOKTITLE = {Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Kleene Algebra [Bad Malente, Germany, 12-17 May 2003]}, EDITOR = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg}, PAGES = {149-162}, PUBLISHER = {Springer}, ADDRESS = {}, PADDRESS = {Berlin}, PYEAR = {2004}, YEAR = {2004}, CADDRESS = {Bad Malente, Germany}, CYEAR = {2003}, CMONTH = may # {~12-17}, SERIES = {LNCS}, VOLUME = {3051}, URL = {Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003.pdf}, ABSTRACT = {SCAN is an algorithm for reducing 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 successful for every second-order logic formula which has an equivalent first-order formula. In this paper we show that SCAN successfully computes the first-order equivalents of all Sahlqvist formulae in the classical (multi-)modal language.} }