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迭代扩展动作逻辑的证明系统,该迭代被视为无穷乘法合取。我们证明了切割可容许性,并为可证性谓词建立了复杂度界限。