V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov (2004): ``SCAN is complete for all Sahlqvist formulae.'' In R. Berghammer, B. Möller, and G. Struth, editors, Revised Selected Papers of the 7th International Seminar on Relational Methods in Computer Science and the 2nd International Workshop on Applications of Kleene Algebra [Bad Malente, Germany, 12-17 May 2003], pp. 149-162. LNCS 3051, Springer.
Abstract, BibTeX, PDF.

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. [an error occurred while processing this directive]