On the computational complexity of cut-reduction
Logic in Computer Science
2007-12-11 v1 Computational Complexity
Abstract
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.
Cite
@article{arxiv.0712.1499,
title = {On the computational complexity of cut-reduction},
author = {Klaus Aehlig and Arnold Beckmann},
journal= {arXiv preprint arXiv:0712.1499},
year = {2007}
}
Comments
41 pages, technical report (CS, Swansea University)