Efficient loop-check for multimodal KD45n logic
Adomas Birštunas
Vilnius University
Published 2021-06-14


sequent calculus
multi-modal logic KD45n
efficient loop-check

How to Cite

Birštunas A. (2021) “Efficient loop-check for multimodal KD45n logic”, Lietuvos matematikos rinkinys, 47(spec.), pp. 351–355. doi: 10.15388/LMR.2007.24227.


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.

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy