We consider modal logic extended with the well-known temporal operator `eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof.

翻译：我们考虑模态逻辑扩展了著名的时态算子"最终"，并为捕捉该片段的循环矢推演提供了切割消去过程。这项工作展示了归约性切割消去方法对循环演算的适应性。值得注意的是，所提算法适用于循环证明，并直接输出无切割的循环证明，无需借助中间机制来规范化最终证明。