2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/143898Using 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.41 pages, technical report (CS, Swansea University)Logic in Computer ScienceComputational ComplexityF.4.1On the computational complexity of cut-reductiontext