Citations of:
Elementary Canonical Formulae: A Survey on Syntactic, Algorithmic, and Modeltheoretic Aspects
In Renate Schmidt, Ian PrattHartmann, Mark Reynolds & Heinrich Wansing (eds.), Advances in Modal Logic, Volume 5. Kings College London Publ.. pp. 1751 (2005)
Add citations
You must login to add citations.


Sahlqvist formulas are a syntactically specified class of modal formulas proposed by Hendrik Sahlqvist in 1975. They are important because of their firstorder definability and canonicity, and hence axiomatize complete modal logics. The firstorder properties definable by Sahlqvist formulas were syntactically characterized by Marcus Kracht in 1993. The present paper extends Kracht's theorem to the class of ‘generalized Sahlqvist formulas' introduced by Goranko and Vakarelov and describes an appropriate generalization of Kracht formulas. 

The previously introduced algorithm \sqema\ computes firstorder frame equivalents for modal formulae and also proves their canonicity. Here we extend \sqema\ with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of firstorder logic with monadic least fixedpoints \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid mucalculus. In particular, we prove that (...) 

