We present a syntactic cut-elimination procedure for the alternation-free fragment of the modal mu-calculus. Cut reduction is carried out within a cyclic proof system, where proofs are finitely branching but may be non-wellfounded. The structure of such proofs is exploited to directly transform a cyclic proof with cuts into a cut-free one, without detouring through other logics or relying on intermediate machinery for regularisation. Novel ingredients include the use of multicuts and results from the theory of well-quasi-orders, the later used in the termination argument.

翻译：本文针对交替自由模态μ演算片段提出了一种语法上的消去规则过程。该消减过程在一个循环证明系统中进行，其中证明具有有限分支但可能非良基。通过直接利用此类证明的结构，可将带消去规则的循环证明转化为无消去规则的证明，无需借助其他逻辑系统或依赖正则化的中间机制。本方法的新颖要素包括多重消去规则的使用以及良拟序理论的结果，后者被应用于终止性论证中。