arnold beckmann's pages
On the computational complexity of cut-reduction
Author: Klaus T Aehlig and Arnold Beckmann
Title: On the computational complexity of cut-reduction
Proceedings: Logic in Computer Science, 2008. LICS '08.
23rd Annual IEEE Symposium on 24-27 June 2008
Pages: 284 - 293
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 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.