Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
From MaRDI portal
Publication:5310652
DOI10.2168/LMCS-2(1:5)2006zbMath1126.03018OpenAlexW2950450725MaRDI QIDQ5310652
Willem Conradie, Dimiter Vakarelov, Valentin F. Goranko
Publication date: 11 October 2007
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2168/lmcs-2(1:5)2006
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)
Related Items (32)
Converse-PDL with regular inclusion axioms: a framework for MAS logics ⋮ A STIT logic for reasoning about social influence ⋮ Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications ⋮ Formalized soundness and completeness of epistemic logic ⋮ Algebraic modal correspondence: Sahlqvist and beyond ⋮ Unnamed Item ⋮ Intermediate logics admitting a structural hypersequent calculus ⋮ Algebraic proof theory for substructural logics: cut-elimination and completions ⋮ Algorithmic correspondence and canonicity for distributive modal logic ⋮ DOING WITHOUT ACTION TYPES ⋮ The Ackermann approach for modal logic, correspondence theory and second-order reduction ⋮ Discrete dualities for \(n\)-potent MTL-algebras and 2-potent BL-algebras ⋮ Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA ⋮ Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm \textsf{PEARL} ⋮ Probabilistic stit logic and its decomposition ⋮ Algorithmic correspondence for intuitionistic modal mu-calculus ⋮ Second-order quantifier elimination in higher-order contexts with applications to the semantical analysis of conditionals ⋮ Probabilistic Stit Logic ⋮ Epistemic logic meets epistemic game theory: a comparison between multi-agent Kripke models and type spaces ⋮ Deontic epistemic stit logic distinguishing modes of mens rea ⋮ Algorithmic correspondence and canonicity for non-distributive logics ⋮ Elementary canonical formulae: extending Sahlqvist's theorem ⋮ A Complete STIT Logic for Knowledge and Action, and Some of Its Applications ⋮ The bounded proof property via step algebras and step frames ⋮ Unnamed Item ⋮ IV. Semantic extensions of SQEMA ⋮ Towards incorporating background theories into quantifier elimination ⋮ Completeness and Correspondence in Hybrid Logic via an Extension of SQEMA ⋮ On the strength and scope of DLS ⋮ COMPLETE ADDITIVITY AND MODAL INCOMPLETENESS ⋮ Unnamed Item ⋮ Algorithmic Correspondence for Relevance Logics I. The Algorithm $$\mathsf {PEARL}$$
Uses Software
This page was built for publication: Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
