On the computational complexity of cut-reduction

2007/12/10 by Klaus Aehlig, Aehlig, Klaus, Arnold Beckmann +1
Computer Science · Engineering · #Computational Complexity (cs.CC) #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Manufacturing Process and Optimization

paper · pdf · doi:10.48550/arxiv.0712.1499

openalex publication_date 2007/12/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Untersuchungen �ber das logische Schlie�en. I

Related

• Cut-restriction: from cuts to analytic cuts
• A theory of cut-restriction: first steps
• Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
• On the convergence of reduction-based and model-based methods in proof theory
• Algorithmic Introduction of Quantified Cuts