English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

SCAN is complete for all Sahlqvist formulae

MPS-Authors
/persons/resource/persons44660

Hustadt,  Ullrich
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45401

Schmidt,  Renate A.
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45565

Struth,  Georg
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Goranko, V., Hustadt, U., Schmidt, R. A., & Vakarelov, D. (2004). SCAN is complete for all Sahlqvist formulae. In Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra (pp. 149-162). Berlin, Germany: Springer.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2B32-6
Abstract
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.