Proof systems for interpretability logics

I will discuss an original family of labelled sequent calculi G3IL* for classical interpretability logics. They are designed on the basis of Verbrugge semantics (a.k.a. generalised Veltman semantics) for the corresponding axiomatic calculi. To my knowledge, this is the most extensive and well-behaving class of analytic proof systems for modal logics of interpretability currently available in the literature. I will address the design choices leading to these sequent calculi and prove (in a modular way) that each of them enjoys excellent structural properties, namely, admissibility of weakening, contraction and, more relevantly, cut.