On the computational complexity of cut-reduction

Klaus Aehlig, Arnold Beckmann

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation sys…