Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA

Willem Conradie, Valentin Goranko, Dimiter Vakarelov

Modal formulae express monadic second-order properties on Kripke frames, but in many important cases these have first-order equivalents. Computing such equivalents is important for…