Hypersequent rules with restricted contexts for propositional modal logics

DOI10.1016/j.tcs.2016.10.004zbMath1402.03076OpenAlexW2535990237MaRDI QIDQ344801

Björn Lellmann

Publication date: 24 November 2016

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2016.10.004

zbMATH Keywords

modal logiccut eliminationdecidabilityHilbert axiomshypersequentsstructural proof theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Rooted hypersequent calculus for modal logic \textsf{S5}, Intermediate logics admitting a structural hypersequent calculus, Complexity of the universal theory of residuated ordered groupoids, Natural deduction calculi for classical and intuitionistic S5, Through an Inference Rule, Darkly, BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS, Multicomponent proof-theoretic method for proving interpolation properties, Complexity of the universal theory of modal algebras

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The proof by cases property and its variants in structural consequence relations
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Prefixed tableaus and nested sequents
• Eliminability of cut in hypersequent calculi for some modal logics of linear frames
• Cut elimination in coalgebraic logics
• The bounded proof property via step algebras and step frames
• Proof analysis in modal logic
• Towards a semantic characterization of cut-elimination
• Deep sequent systems for modal logic
• Gentzen calculi for modal propositional logic
• Cut-free sequent calculi for some tense logics
• Display logic
• Untersuchungen über das logische Schliessen. I
• First-order modal logic
• Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions
• Cut-free tableau calculi for some propositional normal modal logics
• A finite model construction for coalgebraic modal logic
• Focused and Synthetic Nested Sequents
• Structural Extensions of Display Calculi: A General Recipe
• Bounded Proofs and Step Frames
• Hypersequent and Labelled Calculi for Intermediate Logics
• Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5
• Constructing Cut Free Sequent Systems with Context Restrictions Based on Classical or Intuitionistic Logic
• The Logic of Obligation as Weakest Permission
• Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
• Automated Support for the Investigation of Paraconsistent and Other Logics
• Proof Search in Nested Sequent Calculi
• A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5
• Alternation
• Logic Programming with Focusing Proofs in Linear Logic
• Unification in intuitionistic logic
• Hypersequent Calculi for Godel Logics -- a Survey
• From Frame Properties to Hypersequent Rules in Modal Logics
• Admissible Rules of Modal Logics