SCAN is complete for all Sahlqvist formulae

V. Goranko, Ullrich Hustadt, R.A. Schmidt, D. Vakarelov

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


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.
Original languageEnglish
Title of host publicationRelational and Kleene-Algebraic Methods in Computer Science
Subtitle of host publication7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised Selected Papers
EditorsRudolf Berghammer, Bernhard Möller, Georg Struth
Place of PublicationHeidelberg
PublisherSpringer Berlin
Number of pages14
ISBN (Electronic)9783540247715
ISBN (Print)9783540221456
Publication statusPublished - 1 Jun 2004

Publication series

NameLecture Notes in Computer Science


  • Modal Logic
  • Maximal Chain
  • Modal Formula
  • Empty Clause
  • Inference Step


Dive into the research topics of 'SCAN is complete for all Sahlqvist formulae'. Together they form a unique fingerprint.

Cite this