  Sahlqvist formulas are a syntactically specified class of modal formulas
proposed by Hendrik Sahlqvist in 1975. They are important because of their
first-order definability and canonicity, and hence axiomatize complete modal
logics. The first-order 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.
