Glivenkos theorem, finite height, and local tabularity

Glivenkos theorem states that a formula is derivable in classical propositional logic $mathrm{CL}$ iff under the double negation it is derivable in intuitionistic propositional logic $mathrm{IL}$: $mathrm{CL}vdashvarphi$ iff $mathrm{IL}vdash eg egvarphi$. Its analog for the modal logics $mathrm{S5}$ and $mathrm{S4}$ states that $mathrm{S5}vdash varphi$ iff $mathrm{S4} vdash eg Box eg Box varphi$. In Kripke semantics, $mathrm{IL}$ is the logic of partial orders, and $mathrm{CL}$ is the logic of partial orders of height 1. Likewise, $mathrm{S4}$ is the logic of preorders, and $mathrm{S5}$ is the logic of equivalence relations, which are preorders of height 1. In this paper we generalize Glivenkos translation for logics of arbitrary finite height.