Sequent Calculi for the Modal -Calculus over S5
Luca Alberucci · Journal of Logic and Computation · 2009
We present two sequent calculi for the modal µ-calculus over S5 and prove their completeness by using classical methods.One sequent calculus has an analytical cut rule and could be used for a decision procedure the other uses a modified version of the induction rule.We also provide a completeness theorem for Kozen's Axiomatization over S5 without using the completeness result established by Walukiewicz for the modal µ-calculus over arbitrary models.