Abstract
scan is an algorithm for reducing existential second-order logic formulae to equivalent simpler formulae, often first-order logic formulae. It is provably impossible for such a reduction to first-order logic to be successful for every second-order logic formula which has an equivalent first-order formula. In this paper we show that scan successfully computes the first-order equivalents of all Sahlqvist formulae in the classical (multi-)modal language.
This work was supported by EU COST Action 274, and research grants GR/M88761 and GR/R92035 from the UK EPSRC. The first author’s work was supported by research grants from Rand Afrikaans University. Part of the work by the third author was done while on sabbatical leave at the Max-Planck-Institut für Informatik, Germany, in 2002. We would also like the thank the referees for their helpful comments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bibel, W., Schmitt, P.H. (eds.): Automated Deduction – A Basis for Applications, vol. I-III. Kluwer, Dordrecht (1998)
Blackburn, P., de Rijke, M., Venema, V.: Modal Logic. Cambridge Univ. Press, Cambridge (2001)
Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford Logic Guides, vol. 35. Clarendon Press, Oxford (1997)
de Rijke, M., Venema, Y.: Sahlqvist’s Theorem For Boolean Algebras with Operators with an Application to Cylindric Algebras. Studia Logica 54, 61–78 (1995)
Doherty, P., Lukaszewics, W., Szalas, A.: Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning 18(3), 297–336 (1997)
Engel, T.: Quantifier Elimination in Second-Order Predicate Logic. MSc thesis, Saarland University, Saarbrücken, Germany (1996)
Fermüller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Handbook of Automated Reasoning, pp. 1791–1849. Elsevier, Amsterdam (2001)
Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. South African Computer Journal 7, 35–43 (1992)
Goranko, V., Vakarelov, D.: Sahlqvist formulas unleashed in polyadic modal languages. In: Advances in Modal Logic, vol. 3, pp. 221–240. World Scientific, Singapore (2002)
Jónsson, B.: On the canonicity of Sahlqvist identities. Studia Logica 53, 473–491 (1994)
Kracht, M.: How completeness and correspondence theory got married. In: Diamonds and Defaults, pp. 175–214. Kluwer, Dordrecht (1993)
Nonnengart, A.: Strong skolemization. Research Report MPI-I-96-2-010, Max- Planck-Institut für Informatik, Saarbrücken (1996)
Nonnengart, A., Ohlbach, H.J., Szalas, A.: Quantifier elimination for secondorder predicate logic. In: Logic, Language and Reasoning: Essays in honour of Dov Gabbay, Kluwer, Dordrecht (1999)
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335–367. Elsevier, Amsterdam (2001)
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)
Sahlqvist, H.: Completeness and correspondence in the first and second order semantics for modal logics. In: Proc. of the 3rd Scandinavian Logic Symposium, 1973, pp. 110–143. North-Holland, Amsterdam (1975)
Sambin, G., Vaccaro, V.: A new proof of Sahlqvist’s theorem on modal definability and completeness. Journal of Symbolic Logic 54(3), 992–999 (1989)
Szałas, A.: On the correspondence between modal and classical logic: An automated approach. Journal of Logic and Computation 3(6), 605–620 (1993)
van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goranko, V., Hustadt, U., Schmidt, R.A., Vakarelov, D. (2004). SCAN Is Complete for All Sahlqvist Formulae. In: Berghammer, R., Möller, B., Struth, G. (eds) Relational and Kleene-Algebraic Methods in Computer Science. RelMiCS 2003. Lecture Notes in Computer Science, vol 3051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24771-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-24771-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22145-6
Online ISBN: 978-3-540-24771-5
eBook Packages: Springer Book Archive