We introduce a cyclic proof system for the two-way alternation-free modal $\mu$-calculus. The system manipulates one-sided Gentzen sequents and locally deals with the backwards modalities by allowing analytic applications of the cut rule. The global effect of backwards modalities on traces is handled by making the semantics relative to a specific strategy of the opponent in the evaluation game. This allows us to augment sequents by so-called trace atoms, describing traces that the proponent can construct against the opponent's strategy. The idea for trace atoms comes from Vardi's reduction of alternating two-way automata to deterministic one-way automata. Using the multi-focus annotations introduced earlier by Marti and Venema, we turn this trace-based system into a path-based system. We prove that our system is sound for all sequents and complete for sequents not containing trace atoms.

翻译：我们引入了一种针对双向交替无模态μ-演算的循环证明系统。该系统操作单侧根岑序列，并通过对偶规则的分析性应用局部处理反向模态。反向模态在迹上的全局效应通过使语义相对于评估博弈中对手的特定策略来应对。这使我们能够通过所谓的迹原子扩充序列，描述支持者可以针对对手策略构造的迹。迹原子的思想源自瓦尔迪将交替双向自动机简化为确定性单向自动机的方法。利用马尔蒂和韦内马先前引入的多焦点标注，我们将这一基于迹的系统转化为基于路径的系统。我们证明该系统对所有序列是可靠的，且对不含迹原子的序列是完备的。