双向无交替 μ-演算的聚焦式证明

我们为双向无交替模态 μ-演算引入了一个循环证明系统。该系统操作单侧 Gentzen 相继式，并通过允许割规则的解析性应用来局部处理向后模态。向后模态在迹上的全局效应通过使语义相对于评估博弈中对手的特定策略来处理。这使我们能够用所谓的迹原子扩充相继式，以描述主张者针对对手策略可构造的迹。迹原子的思想源于 Vardi 将交替双向自动机归约为确定性单向自动机的工作。利用 Marti 和 Venema 早先引入的多聚焦标注，我们将这一基于迹的系统转化为基于路径的系统。我们证明了我们的系统对所有相继式是可靠的，并对不含迹原子的相继式是完备的。