On the Computational Complexity of Cut-Reduction

Using appropriate notation systems for proofs, cutreduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Klaus Aehlig, Arnold Beckmann
• Keywords: Appropriate Notation Systems, Computer Science, Explicit Bounds, LICS 2008, Suitable Notation