Improved Second-Order Quantifier Elimination in Modal Logic

Schmidt, R. A. (2008)

In Hölldobler, S. and Lutz, C. and Wansing, H. (eds), Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Artificial Intelligence, Vol. 5293, Springer, 375-388. BiBTeX, DOI Link.

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.

Long version
Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified:
Copyright © 2008 Renate A. Schmidt, School of Computer Science, Man Univ,