一句话：通过无割矢列演算与到单调 μ-演算的翻译，证明 Parikh 博弈逻辑及其 Hilbert 公理系统的完备性。
博弈逻辑是 Parikh 在 1980 年代提出的命题动态逻辑推广，用于推理确定型二人博弈中玩家可强制实现的结果，其语义从 Kripke 模型推广到单调邻域模型。Parikh 的 PDL 风格 Hilbert 系统可靠性容易证明，但完备性长期未决。本文为博弈逻辑引入无割矢列演算，并给出两个操作带标注公式的无割矢列演算：一个针对博弈逻辑，一个针对单调 μ-演算（在单调邻域模型上解释的多模态 μ-演算）。作者证明这些系统可靠且完备，进而得到 Parikh 公理系统的完备性。方法沿用 Afshari 与 Leigh (LICS 2017) 的思路，通过系统间证明变换获得完备性，关键是保有效性的从博弈逻辑到单调 μ-演算的翻译。
Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone μ -calculus, the variant of the polymodal μ -calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone μ -calculus.