Gentzen calculi for modal propositional logic

DOI10.1007/978-90-481-9670-8zbMath1232.03007OpenAlexW570944246MaRDI QIDQ987853

Publication date: 16 August 2010

Published in: Trends in Logic -- Studia Logica Library (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-90-481-9670-8

zbMATH Keywords

modal logic proof theory sequent systems Gödel-Löb provability logic tree-hypersequents tree-model property

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items (44)

The Došen square under construction: a tale of four modalities ⋮ Algebra, Proof Theory and Applications for a Logic of Propositions, Actions and Adjoint Modal Operators ⋮ Linear Nested Sequents, 2-Sequents and Hypersequents ⋮ Natural deduction calculi and sequent calculi for counterfactual logics ⋮ Hypersequent rules with restricted contexts for propositional modal logics ⋮ Labeled sequent calculi for modal logics and implicit contractions ⋮ Towards a proof theory for quantifier macros ⋮ Sequent systems for negative modalities ⋮ LINEAR TIME IN HYPERSEQUENT FRAMEWORK ⋮ Provability multilattice logic ⋮ A Sound Interpretation of Leśniewski's Epsilon in Modal Logic KTB ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ Varieties of Relevant S5 ⋮ A novel approach to equality ⋮ Logical multilateralism ⋮ Sequent Calculi for Orthologic with Strict Implication ⋮ Nested sequents for intermediate logics: the case of Gödel-Dummett logics ⋮ Cut Elimination Theorem for Non-Commutative Hypersequent Calculus ⋮ Proof theory for functional modal logic ⋮ Anything goes ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ Hypersequent Calculi for S5: The Methods of Cut Elimination ⋮ Eliminability of cut in hypersequent calculi for some modal logics of linear frames ⋮ A Critical Overview of the Most Recent Logics of Grounding ⋮ Through an Inference Rule, Darkly ⋮ Non-classical elegance for sequent calculus enthusiasts ⋮ Proofs and countermodels in non-classical logics ⋮ Hypersequent and display calculi -- a unified perspective ⋮ A survey of nonstandard sequent calculi ⋮ HARMONIC INFERENTIALISM AND THE LOGIC OF IDENTITY ⋮ A cut-free sequent calculus for defeasible erotetic inferences ⋮ Subformula property for some modal logics ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ The logicality of equality ⋮ The bounded proof property via step algebras and step frames ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ A general proof certification framework for modal logic ⋮ Sequent calculi for global modal consequence relations ⋮ An analytic calculus for the intuitionistic logic of proofs ⋮ Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus ⋮ Modal multilattice logics with Tarski, Kuratowski, and Halmos operators ⋮ On Blass translation for Leśniewski's propositional ontology and modal logics ⋮ CUT-FREE COMPLETENESS FOR MODULAR HYPERSEQUENT CALCULI FOR MODAL LOGICS K, T, AND D

This page was built for publication: Gentzen calculi for modal propositional logic