@INPROCEEDINGS{Schmidt08a,
AUTHOR = {Schmidt, R. A.},
YEAR = {2008}, 
TITLE = {Improved Second-Order Quantifier Elimination in Modal Logic},
EDITOR = {H{\"o}lldobler, S. and Lutz, C. and Wansing, H.},
BOOKTITLE = {Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5293},
PUBLISHER = {Springer},
PAGES = {375--388},
URL = {http://dx.doi.org/10.1007/978-3-540-87803-2_31},
ABSTRACT = {
This paper introduces improvements for second-order quantifier
elimination methods based on Ackermann's Lemma and investigates their
application in modal correspondence theory.
In particular, we define refined calculi and procedures for solving the problem
of eliminating quantified propositional symbols from modal formulae.
We prove correctness results and use the approach to
compute first-order frame correspondence properties for modal axioms
and modal rules.
Our approach can solve two new classes of formulae which have wider
scope than existing classes known to be solvable by second-order quantifier
elimination methods.
}
}