期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2003
卷号：2003
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：Height restricted constant depth LK is a natural restriction of Gentzen's propositional proof system LK. A sequence of LK-formulas has polylogarithmic-height restricted depth-d-LK proofs iff the n-th formula in the sequence possesses LK-proofs where cut-formulas are of depth d+1 with small bottom fanin and of size quasi-polynomial in n, and the height of the proof tree is bounded polylogarithmic in n. We will proof a separation of polylogarithmic-height restricted depth-d-LK proofs from quasi-polynomial-size tree-like depth-d-LK proofs using the order induction principle. Our lower bounds technique utilizes Hastad's Switching Lemmas to obtain so called "cut-reduction by switching". We will further explain the connection of height restricted constant depth LK to theories of relativized bounded arithmetic. Separations of height restricted constant depth LK in turn yield separations of relativized bounded arithmetic.
