@ARTICLE{Schmidt12a, 
AUTHOR = {Schmidt, R. A.},
YEAR = {2012}, 
TITLE = {The {A}ckermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction},
JOURNAL = {Journal of Applied Logic},
VOLUME = {10}.
NUMBER = {1},
PAGES = {52--74}
DOI = {http://dx.doi.org/10.1016/j.jal.2012.01.001},
ABSTRACT = {
The problem of eliminating second-order quantification over predicate
symbols is in general undecidable.  Since an application of second-order
quantifier elimination is correspondence theory in modal logic,
understanding when second-order quantifier elimination methods succeed
is an important problem that sheds light on the kinds of axioms that are
equivalent to first-order correspondence properties and can be used to
obtain complete axiomatizations for modal logics.  This paper introduces
a substitution-rewrite approach based on Ackermann's Lemma to
second-order quantifier elimination in modal logic.  Compared to related
approaches, the approach includes a number of enhancements: The
quantified symbols that need to be eliminated can be flexibly specified.
The inference rules are restricted by orderings compatible with the
elimination order, which provides more control and reduces
non-determinism in derivations thereby increasing the efficiency and
success rate.  The approach is equipped with a powerful notion of
redundancy, allowing for the flexible definition of practical
simplification and optimization techniques.  We present correctness,
termination and canonicity results, and consider two applications:
(i) computing first-order frame correspondence properties for modal
axioms and rules, and (ii) rewriting second-order modal problems to
equivalent simpler forms.  The approach allows us to define and
characterize two new classes of formulae, which are elementary and
canonical, and subsume the class of Sahlqvist formulae and the class of
monadic inductive formulae.
}
}