Deep sequent systems for modal logic

DOI10.1007/s00153-009-0137-3zbMath1180.03023OpenAlexW1966647830MaRDI QIDQ834716

Kai Brünnler

Publication date: 27 August 2009

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-009-0137-3

zbMATH Keywords

modal logiccut eliminationnested sequentssubformula propertydeep inference

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Related Items

MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description) ⋮ Label-free natural deduction systems for intuitionistic and classical modal logics ⋮ Nested sequents for intuitionistic modal logics via structural refinement ⋮ Game semantics for constructive modal logic ⋮ Linear Nested Sequents, 2-Sequents and Hypersequents ⋮ Realization Theorems for Justification Logics: Full Modularity ⋮ Uniform interpolation via nested sequents ⋮ A pure view of ecumenical modalities ⋮ Nested Sequent Calculi for Conditional Logics ⋮ Hypersequent rules with restricted contexts for propositional modal logics ⋮ Labeled sequent calculi for modal logics and implicit contractions ⋮ Proof internalization in generalized Frege systems for classical logic ⋮ LINEAR TIME IN HYPERSEQUENT FRAMEWORK ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ An ecumenical notion of entailment ⋮ Disentangling structural connectives or life without display property ⋮ Prefixed tableaus and nested sequents ⋮ FRACTIONAL-VALUED MODAL LOGIC ⋮ Nested sequents for intermediate logics: the case of Gödel-Dummett logics ⋮ Natural deduction calculi for classical and intuitionistic S5 ⋮ Realization for justification logics via nested sequents: modularity through embedding ⋮ Nested sequents for intuitionistic logics ⋮ A fresh view of linear logic as a logical framework ⋮ Maehara-style modal nested calculi ⋮ On Height and Happiness ⋮ Modal interpolation via nested sequents ⋮ Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic ⋮ Proofs and countermodels in non-classical logics ⋮ A generalized proof-theoretic approach to logical argumentation based on hypersequents ⋮ Unnamed Item ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ Focused and Synthetic Nested Sequents ⋮ Supervenience, Dependence, Disjunction ⋮ A general proof certification framework for modal logic ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ Local reductions for the modal cube ⋮ On the proof theory of infinitary modal logic ⋮ CUT-FREE COMPLETENESS FOR MODULAR HYPERSEQUENT CALCULI FOR MODAL LOGICS K, T, AND D

Cites Work

• Proof analysis in modal logic
• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• Cut-free sequent calculi for some tense logics
• Displaying modal logic
• Display logic
• MELL in the calculus of structures
• A deep inference system for the modal logic S5
• A Local System for Classical Logic
• The Method of Tree-Hypersequents for Modal Propositional Logic
• CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Deep sequent systems for modal logic