We present a proof system that extends action logic by omega iteration, which is viewed as infinitary multiplicative conjunction. We prove cut admissibility and establish complexity bounds for the provability predicate.

翻译：我们提出了一种通过Omega迭代扩展动作逻辑的证明系统，该迭代被视为无穷乘法合取。我们证明了切割可容许性，并为可证性谓词建立了复杂度界限。