swMATH ID: 3056
Software Authors: Conradie, Willem; Goranko, Valentin
Description: Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA. In [{it W. E. Conradie, V. F. Goranko} and {it D. Vakarelov}, Log. Methods Comput. Sci. 2, No. 1, Paper 5 (2006; Zbl 1126.03018)] we introduced the algorithm SQEMA for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. SQEMA is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of SQEMA where that syntactic condition is replaced by a semantic one, viz. downward monotonicity. For the first, and most general, extension SemSQEMA we prove correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae, defined by replacing polarity with monotonicity. By employing a special modal version of Lyndon’s monotonicity theorem and imposing additional requirements on the Ackermann rule we obtain restricted versions of SemSQEMA which guarantee canonicity, too.
Homepage: http://dimiter.slavi.biz/sqema/
Keywords: modal correspondence and completeness; algorithm SQEMA; Sahlqvist formulae; inductive formulae; Lyndon monotonicity; canonicity
Related Software: Epistemic Logic; Archive Formal Proofs; FOL Fitting; Pesca
Referenced in: 39 Publications

Referencing Publications by Year