一句话：为双向模态 μ-演算引入非良基与循环矢列证明系统，证明其可靠完备，并推出 Craig 插值与 Beth 可定义性。
双向模态 μ-演算是在标准单向 μ-演算上加入反向模态的扩展。论文为该逻辑提出两种新的矢列式证明演算：允许无限分支的非良基系统，以及带标注的有限循环版本；二者均包含分析性切规则，并借助迹原子在证明论中应用 Vardi 的双向自动机。作者证明两个系统的可靠性与完备性，随后利用循环演算证明该逻辑关于命题和模态均具有局部 Craig 插值性质。证明方法是将 Maehara 方法适配到循环证明系统，并由此推出 Beth 可定义性。
The two-way modal μ-calculus is the extension of the (standard) one-way μ-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style proof calculi: a non-wellfounded system admitting infinite branches and a finitary, cyclic version of this that employs annotations.As is common in sequent systems for two-way modal logics, our calculi feature an analytic cut rule. What distinguishes our approach is the use of so-called trace atoms, which serve to apply Vardi’s two-way automata in a proof-theoretic setting.We prove soundness and completeness for both systems and subsequently use the cyclic calculus to show that the two-way μ-calculus has the (local) Craig interpolation property, with respect to both propositions and modalities. Our proof uses a version of Maehara’s method adapted to cyclic proof systems. As a corollary we prove that the two-way μ-calculus also enjoys Beth’s definability property.