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