Title :
On the Computational Complexity of Cut-Reduction
Author :
Aehlig, Klaus ; Beckmann, Arnold
Author_Institution :
Dept. of Comput. Sci., Swansea Univ. Singleton Park, Swansea
Abstract :
Using appropriate notation systems for proofs, cut-reduction 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.
Keywords :
computational complexity; theorem proving; bounded arithmetic; computational complexity; cut-reduction; Arithmetic; Computational complexity; Computer science; Logic; Machinery; Polynomials; Search problems; Writing; Bounded Arithmetic; cut-reduction; proof notations; propositional logic;
Conference_Titel :
Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on
Conference_Location :
Pittsburgh, PA
Print_ISBN :
978-0-7695-3183-0
DOI :
10.1109/LICS.2008.9
