SQEMA
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 firstorder 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 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA. Zbl 1181.03007 Conradie, Willem; Goranko, Valentin 
2008

all
top 5
Referenced by 37 Authors
all
top 5