Paper  abstract   bibtex   

@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.}
}