A cut-free CoS system for S5

Dear all,

attached is a paper (draft) I've written lately on the technical
results of my master thesis (completed last October in Dresden,
supervised by Charles Stewart). It is entitled "a system of deep
inference for the modal logic S5" and presents a cut-admissible system
for S5 in the calculus of structures. A short elaboration on the
importance and consequences of deep inference in modal systems is
given in the introduction.

I am planning to apply the final corrections/changes and submit it for
publication by the end of next week. Comments/suggestions/corrections
are more than welcome.

Regards,
Phiniki