Paper announcement: CMDL in CoS

Hi,
Rajeev Gore and I recently wrote a paper on relating display logics
and the calculus of structures. We did a case study on encoding
classical modal display logic (CMDL) of Wansing into CoS.
Through primitive extensions of CMDL, we managed to get a minimal
cut free CoS system for S5.
Details of the paper is given below, including a link to a draft.
Comments and suggestions are most welcome.

-Alwen

--

Classical Modal Display Logic in the Calculus of Structures and
Minimal and Cut-free Deep Inference Calculi for S5
by Rajeev Gore and Alwen Tiu.

Abstract:
We begin by showing how to faithfully encode the Classical Modal
Display Logic (CMDL) of Wansing into the Calculus Of Structures
(CoS) of Guglielmi.  Since every CMDL calculus enjoys
cut-elimination, we obtain a cut-elimination theorem for all
corresponding CoS calculi. We then show how our result leads to a
minimal cut-free CoS calculus for modal logic $\SFive$. As far as we know,
no other existing CoS calculi for $\SFive$ enjoy both these properties
simultaneously.

Link: http://users.rsise.anu.edu.au/~tiu/papers/cmdl.pdf