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

{"_id":"8p95vy5vh9xrkinQ7","bibbaseid":"goranko-hustadt-schmidt-vakarelov-scaniscompleteforallsahlqvistformulae-2004","author_short":["Goranko, V.","Hustadt, U.","Schmidt, R.","Vakarelov, D."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Goranko"],"firstnames":["Valentin"],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["Renate"],"suffixes":[]},{"propositions":[],"lastnames":["Vakarelov"],"firstnames":["Dimiter"],"suffixes":[]}],"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":[{"propositions":[],"lastnames":["Berghammer"],"firstnames":["Rudolf"],"suffixes":[]},{"propositions":[],"lastnames":["Möller"],"firstnames":["Bernhard"],"suffixes":[]},{"propositions":[],"lastnames":["Struth"],"firstnames":["Georg"],"suffixes":[]}],"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.","bibtex":"@INPROCEEDINGS{Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003,\n AUTHOR = {Goranko, Valentin and Hustadt, Ullrich and \n Schmidt, Renate and Vakarelov, Dimiter},\n TITLE = {{SCAN} is complete for all Sahlqvist formulae},\n BOOKTITLE = {Revised Selected Papers of the 7th International \n Seminar on Relational Methods in Computer Science and the\n 2nd International Workshop on Kleene Algebra\n [Bad Malente, Germany, 12-17 May 2003]},\n EDITOR = {Berghammer, Rudolf and M{\\\"o}ller, Bernhard\n and Struth, Georg},\n PAGES = {149-162},\n PUBLISHER = {Springer},\n ADDRESS = {},\n PADDRESS = {Berlin},\n PYEAR = {2004},\n YEAR = {2004},\n CADDRESS = {Bad Malente, Germany},\n CYEAR = {2003},\n CMONTH = may # {~12-17},\n SERIES = {LNCS},\n VOLUME = {3051},\n URL = {Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003.pdf},\n ABSTRACT = {SCAN is an algorithm for reducing existential\n second-order logic formulae to equivalent simpler formulae, often\n first-order logic formulae. It is provably impossible for such a\n reduction to first-order logic to be successful for every second-order\n logic formula which has an equivalent first-order formula. In this\n paper we show that SCAN successfully computes the first-order\n equivalents of all Sahlqvist formulae in the classical (multi-)modal\n language.}\n}\n","author_short":["Goranko, V.","Hustadt, U.","Schmidt, R.","Vakarelov, D."],"editor_short":["Berghammer, R.","Möller, B.","Struth, G."],"key":"Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003","id":"Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003","bibbaseid":"goranko-hustadt-schmidt-vakarelov-scaniscompleteforallsahlqvistformulae-2004","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Goranko+Hustadt+Schmidt+Vakarelov@RSRelMiCSIWAKA2003.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["scan","complete","sahlqvist","formulae","goranko","hustadt","schmidt","vakarelov"],"title":"SCAN is complete for all Sahlqvist formulae","year":2004}