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 ... more >>>