Cut-free double sequent calculus for S5

DOI10.1093/jigpal/6.3.505zbMath0910.03013OpenAlexW1980025572MaRDI QIDQ4392661

Andrzej Indrzejczak

Publication date: 19 April 1999

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

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

zbMATH Keywords

modal logiccut-eliminationKripke-style tableauxpropositional S5

Mathematics Subject Classification ID

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

Related Items

A deep inference system for the modal logic S5, From single agent to multi-agent via hypersequents, Rooted hypersequent calculus for modal logic \textsf{S5}, Varieties of Relevant S5, THE LOGIC OF HYPERLOGIC. PART A: FOUNDATIONS, Hypersequent Calculi for S5: The Methods of Cut Elimination, On a multilattice analogue of a hypersequent S5 calculus, Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom