Extending Action Logic with Omega Iteration

Abstract

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.

technical report, draft