A Systematic Proof Theory for Several Modal Logics.
Charles H. Stewart III, Phiniki Stouppa · 2004
... This paper introduces a systematic presentation for the systems K, D, M, S4, and S5 in the calculus of structures, a structural proof theory that employs deep inference. Because of this, we are able to axiomatise the modal logics in a manner directly analogous to the Hilbert-Lewis axiomatisation. We show that the calculus possesses a cut-elimination property directly analogous to cut-elimination for the sequent calculus for these systems, and we discuss the extension to several other modal logics