Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR03-034 | 17th March 2003 00:00

Height restricted constant depth LK

RSS-Feed




TR03-034
Authors: Arnold Beckmann
Publication: 13th May 2003 15:06
Downloads: 3056
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint