G3i 演算的 G4i 类似物
The G4i analogue of a G3i calculus
AI总结：
本文提出一种为一大类直觉主义模态逻辑构造终止分析演算的方法，将 Dyckhoff 针对直觉主义命题逻辑的 G4ip 工作扩展至直觉主义模态逻辑，修正了早期版本的定理错误。
摘要：
本文提供了一种为一大类直觉主义模态逻辑获取终止的分析演算的方法。对于给定的具有无切演算 G（该演算是 G3ip 的扩展）的逻辑 L，该方法生成一个终止的分析演算，该演算是 G4ip 的扩展且与 G 等价。G4ip 由 Dyckhoff 于 1992 年提出，作为直觉主义命题逻辑的演算 G3ip 的终止类似物。因此，本文可视为将 Dyckhoff 的工作扩展至直觉主义模态逻辑的成果。（这是 2026 年 8 月 21 日的修正版本，修正了早期 arXiv 版本中定理 3.4 的错误）
英文摘要：
This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic L with a cut-free calculus G that is an extension of G3ip the method produces a terminating analytic calculus that is an extension of G4ip and equivalent to G. G4ip has been introduced by Dyckhoff in 1992 as a terminating analogue of the calculus G3ip for intuitionistic propositional logic. Thus this paper can be viewed as an extension of Dyckhoff's work to intuitionistic modal logic. (This is a corrected version (21 August 2026) of an earlier arXiv version that contained a mistake in Theorem 3.4.)
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
