Instantial Neighborhood Logic — tableau, sequent calculus, and interpolation

Instantial Neighborhood Logic (INL) employs a two-sorted operator $\square$. In INL, formula $\square(\alpha_1,\dots,\alpha_j;\alpha_0)$ means, the current point has a neighborhood in which $\alpha_0$ universally holds, and none of $\alpha_1,\dots,\alpha_j$ universally fails. In my talk last year at Tbilisi State University, a tableau system for INL was presented. To continue, in this talk we convert that tableau system to a hyper-sequent calculus, and then to a (normal) sequent calculus G3inl. Based on a splitting version of G3inl, we will explain how Lyndon interpolation theorem of INL is constructively established.