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 22 articles , 1 standard article )
Showing results 1 to 20 of 22.
Sorted by year (- 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)
- Bezhanishvili, Nick; Ghilardi, Silvio: The bounded proof property via step algebras and step frames (2014)
- 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)
- Conradie, Willem; Palmigiano, Alessandra: Algorithmic correspondence and canonicity for distributive modal logic (2012)
- Schmidt, Renate A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction (2012)
- Broersen, Jan: Deontic epistemic stit logic distinguishing modes of mens rea (2011)
- Dunin-Kȩplicz, Barbara; Nguyen, Linh Anh; Szałas, Andrzej: Converse-PDL with regular inclusion axioms: a framework for MAS logics (2011)
- Conradie, Willem; Goranko, Valentin; Vakarelov, Dimitar: Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA (2010)
- Broersen, Jan: A complete STIT logic for knowledge and action, and some of its applications (2009)
- Conradie, Willem: Completeness and correspondence in hybrid logic via an extension of SQEMA (2009)
- Conradie, Willem; Goranko, Valentin; Vakarelov, Dimiter: Algorithmic correspondence and completeness in modal logic. III. Extensions of the algorithm SQEMA with substitutions (2009)
- Kikot, Stanislav: An extension of Kracht’s theorem to generalized Sahlqvist formulas (2009)
- Conradie, Willem; Goranko, Valentin: Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA. (2008)
- Schmidt, Renate A.: Improved second-order quantifier elimination in modal logic (2008)
- Szałas, Andrzej: Towards incorporating background theories into quantifier elimination (2008)
- Gabbay, Dov M.; Szałas, Andrzej: Second-order quantifier elimination in higher-order contexts with applications to the semantical analysis of conditionals (2007)
- Conradie, Willem; Goranko, Valentin; Vakarelov, Dimiter: Algorithmic correspondence and completeness in modal logic. I: The core algorithm SQEMA (2006)
- Conradie, Willem; Goranko, Valentin; Vakarelov, Dimiter: Algorithmic correspondence and completeness in modal logic. II: Polyadic and hybrid extensions of the algorithm SQEMA (2006)