SCAN Is Complete for All Sahlqvist Formulae

  • V. Goranko
  • U. Hustadt
  • R. A. Schmidt
  • D. Vakarelov
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)


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.


Modal Logic Maximal Chain Modal Formula Empty Clause Inference Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bibel, W., Schmitt, P.H. (eds.): Automated Deduction – A Basis for Applications, vol. I-III. Kluwer, Dordrecht (1998)Google Scholar
  2. 2.
    Blackburn, P., de Rijke, M., Venema, V.: Modal Logic. Cambridge Univ. Press, Cambridge (2001)zbMATHGoogle Scholar
  3. 3.
    Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford Logic Guides, vol. 35. Clarendon Press, Oxford (1997)zbMATHGoogle Scholar
  4. 4.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Doherty, P., Lukaszewics, W., Szalas, A.: Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning 18(3), 297–336 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Engel, T.: Quantifier Elimination in Second-Order Predicate Logic. MSc thesis, Saarland University, Saarbrücken, Germany (1996)Google Scholar
  7. 7.
    Fermüller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Handbook of Automated Reasoning, pp. 1791–1849. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  8. 8.
    Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. South African Computer Journal 7, 35–43 (1992)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Jónsson, B.: On the canonicity of Sahlqvist identities. Studia Logica 53, 473–491 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Kracht, M.: How completeness and correspondence theory got married. In: Diamonds and Defaults, pp. 175–214. Kluwer, Dordrecht (1993)Google Scholar
  12. 12.
    Nonnengart, A.: Strong skolemization. Research Report MPI-I-96-2-010, Max- Planck-Institut für Informatik, Saarbrücken (1996)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335–367. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  15. 15.
    Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Szałas, A.: On the correspondence between modal and classical logic: An automated approach. Journal of Logic and Computation 3(6), 605–620 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • V. Goranko
    • 1
  • U. Hustadt
    • 2
  • R. A. Schmidt
    • 3
  • D. Vakarelov
    • 4
  1. 1.Rand Afrikaans UniversitySouth Africa
  2. 2.University of LiverpoolUK
  3. 3.University of ManchesterUK
  4. 4.Sofia UniversityBulgaria

Personalised recommendations