关于割约化的计算复杂性
On the computational complexity of cut-reduction
摘要：
使用适当的符号系统进行证明，割约简通常可以在这些符号上变得可行，并且可以给出明确的界限。发展一个合适的有界算术的符号系统，并应用这些有界算术，某些这类理论中关于可定义函数的所有已知结果都可以统一地重新得到。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
