SCAN is complete for all Sahlqvist formulae. Goranko, V., Hustadt, U., Schmidt, R., & Vakarelov, D. In Berghammer, R., Möller, B., & Struth, G., editors, *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]*, volume 3051, of *LNCS*, pages 149-162, 2004. Springer.

Paper abstract bibtex

Paper abstract bibtex

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.

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

Downloads: 0

{"_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}