SQEMA
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.
Keywords for this software
References in zbMATH (referenced in 39 articles , 1 standard article )
Showing results 1 to 20 of 39.
Sorted by year (- Conradie, Willem; Palmigiano, Alessandra: Algorithmic correspondence and canonicity for non-distributive logics (2019)
- Conradie, Willem; Palmigiano, Alessandra; Zhao, Zhiguang: Sahlqvist via translation (2019)
- Holliday, Wesley H.; Litak, Tadeusz: Complete additivity and modal incompleteness (2019)
- Lauridsen, Frederik M.: Intermediate logics admitting a structural hypersequent calculus (2019)
- Conradie, Willem; Palmigiano, Alessandra; Sourabh, Sumit: Algebraic modal correspondence: Sahlqvist and beyond (2017)
- Conradie, Willem; Robinson, Claudette: On Sahlqvist theory for hybrid logics (2017)
- Frittella, Sabine; Palmigiano, Alessandra; Santocanale, Luigi: Dual characterizations for finite lattices via correspondence theory for monotone modal logic (2017)
- Ma, Minghui; Zhao, Zhiguang: Unified correspondence and proof theory for strict implication (2017)
- Palmigiano, Alessandra; Sourabh, Sumit; Zhao, Zhiguang: Jónsson-style canonicity for ALBA-inequalities (2017)
- Palmigiano, Alessandra; Sourabh, Sumit; Zhao, Zhiguang: Sahlqvist theory for impossible worlds (2017)
- Düntsch, Ivo; Orłowska, Ewa; van Alten, Clint: Discrete dualities for (n)-potent MTL-algebras and 2-potent BL-algebras (2016)
- Galeazzi, Paolo; Lorini, Emiliano: Epistemic logic meets epistemic game theory: a comparison between multi-agent Kripke models and type spaces (2016)
- Georgiev, Dimiter T.: Deterministic SQEMA and application for pre-contact logic (2016)
- Lorini, Emiliano; Sartor, Giovanni: A STIT logic for reasoning about social influence (2016)
- Conradie, Willem; Fomatati, Yves; Palmigiano, Alessandra; Sourabh, Sumit: Algorithmic correspondence for intuitionistic modal mu-calculus (2015)
- Wernhard, Christoph: Second-order quantifier elimination on relational monadic formulas -- a basic method and some less expected applications (2015)
- Bezhanishvili, Nick; Ghilardi, Silvio: The bounded proof property via step algebras and step frames (2014)
- Broersen, Jan: Probabilistic stit logic and its decomposition (2013)
- Lorini, Emiliano; Troquard, Nicolas; Herzig, Andreas; Broersen, Jan: Grounding power on actions and mental attitudes (2013)
- Ciabattoni, Agata; Galatos, Nikolaos; Terui, Kazushige: Algebraic proof theory for substructural logics: cut-elimination and completions (2012)