可证性逻辑 GLB 的子系统 J$_2$ 中的统一性
Unification in subsystem J$_2$ of provability logic GLB
AI总结：
本文推广 S. Ghilardi 的方法应用于双模态可证性逻辑 GLB 的子系统 J$_2$，利用 Kripke 语义描述投影公式，证明其具有有限统一类型，并得出其可容许性问题可判定的结论。
摘要：
我们推广 S. Ghilardi 开发的方法，并将其应用于双模态可证性逻辑 GLB 的子系统 J$_2$。我们用 Kripke 语义描述了 J$_2$ 中的投影公式，并证明逻辑 J$_2$ 具有有限统一类型。作为应用，我们证明了 J$_2$ 的可容许性问题是可判定的。
英文摘要：
We generalize methods, developed by S. Ghilardi, and apply them to a subsystem J$_2$ of bimodal provability logic GLB. We describe projective formulas in J$_2$ in terms of Kripke semantics and prove that logic J$_2$ has finitary unification type. As an application, we show that admissibility problem for J$_2$ is decidable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
