@inbook{e2fb875f48b54b508fb7c3e3b1ca2662,

title = "SCAN is complete for all Sahlqvist formulae",

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.",

keywords = "Modal Logic, Maximal Chain, Modal Formula, Empty Clause, Inference Step",

author = "V. Goranko and Ullrich Hustadt and R.A. Schmidt and D. Vakarelov",

year = "2004",

month = jun,

day = "1",

language = "English",

isbn = "9783540221456",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin",

pages = "149--162",

editor = "Berghammer, {Rudolf } and M{\"o}ller, {Bernhard } and Struth, {Georg }",

booktitle = "Relational and Kleene-Algebraic Methods in Computer Science",

address = "Germany",

}