@inproceedings{46de053bbe05471c9f583039727d0f0f,
title = "Improved second-order quantifier elimination in modal logic",
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. {\textcopyright} 2008 Springer-Verlag Berlin Heidelberg.",
keywords = "Computer Science, Artificial Intelligence",
author = "Schmidt, {Renate A.}",
note = "Schmidt, Renate A. 9 BERLIN BIL89; 11th European Conference on Logics in Artificial Intelligence, JELIA 2008 ; Conference date: 01-07-2008",
year = "2008",
doi = "10.1007/978-3-540-87803-2_31",
language = "English",
isbn = "9783540878025",
volume = "5293",
series = "Lecture Notes in Computer Science and Lecture Notes in Artificial Intelligence",
publisher = "Springer Nature",
pages = "375--388",
editor = "H{\"o}lldobler, {Steffen } and Lutz, {Carsten } and Wansing, {Heinrich }",
booktitle = "Logics in Artificial Intelligence",
address = "United States",
}