A cut-free Gentzen formulation of the modal logic S5

DOI10.1093/JIGPAL/8.5.629MaRDI QIDQ4511541zbMATH OpenOpenAlexFDO

Authors Torben Braüner

Publication date 28 February 2001

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/8.5.629

zbMATH Keywords

modal logiccut-eliminationGentzen systemS5

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 3871327
• A cut-free simple sequent calculus for modal logic S5
• Hypersequent calculi for S5: the methods of cut elimination
• Cut free sequent calculus for logic S5\(_n\)(ED)
• scientific article; zbMATH DE number 4108725

Cited in

(19)

• Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
• A deep inference system for the modal logic S5
• scientific article; zbMATH DE number 1222706 (Why is no real title available?)
• Why does the proof-theory of hybrid logic work so well?
• scientific article; zbMATH DE number 3871327 (Why is no real title available?)
• The multiplicative-additive Lambek calculus with subexponential and bracket modalities
• Hypersequent calculi for S5: the methods of cut elimination
• Rooted hypersequent calculus for modal logic \textsf{S5}
• Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere
• On a multilattice analogue of a hypersequent S5 calculus
• scientific article; zbMATH DE number 5521794 (Why is no real title available?)
• A cut-free simple sequent calculus for modal logic S5
• Cut-free completeness for modular hypersequent calculi for modal logics K, T, and D
• Varieties of Relevant S5
• scientific article; zbMATH DE number 4010486 (Why is no real title available?)
• scientific article; zbMATH DE number 4116498 (Why is no real title available?)
• Proof analysis in modal logic
• Non-labelled sequent calculi of public announcement expansions of \textbf{K45} and \textbf{S5}
• Full classical S5 in natural deduction with weak normalization

This page was built for publication: A cut-free Gentzen formulation of the modal logic S5

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4511541)