Efficient loop-check for multimodal KD45n logic - Birštunas, Adomas (Lietuvos matematikos rinkinys, 2021)
We introduce sequent calculus for multi-modal logic KD45n which uses efficient loop-check. Efficiency of the used loop-check is obtained by using marked modal operator squarei which is used as an alternative to sequent with histories ([2,3]).We use inference rules with or branches to make all rules invertible or semi-invertible. We showthe maximum height of the constructed derivation tree.  Also polynomial space complexity is proved.
Keywords: sequent calculus; multi-modal logic KD45n; efficient loop-check