V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov (2003): ``SCAN is complete for all Sahlqvist formulae.'' In R. Berghammer and B. Möller, editors, Proceedings of the 7th International Seminar on Relational Methods in Computer Science (RelMiCS-7) [Bad Malente, Germany, 12-17 May 2003], pp. 230-241. Christian-Albrechts-Universität Kiel.
Abstract, BibTeX, PDF.

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.