SCAN is complete for all Sahlqvist formulae

Goranko, V., Hustadt, U., Schmidt, R. A. and Vakarelov, D. (2004)

In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science 3051, Springer, 149-162. 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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 12 Jun 07
Copyright © 2004 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk