Efficient loop-check for multimodal KD45n logic

Abstract

We introduce sequent calculus for multi-modal logic KD45_n which uses efficient loop-check. Efficiency of the used loop-check is obtained by using marked modal operator square_i 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.