Loop-free sequent calculus for modal logic K4 - Andirkonis, Julius (Lietuvos matematikos rinkinys, 2009)
In the article, a loop-free calculus for modal logic K4 is presented. The calculus is based on marks and indices method which was first used for logic S4.