Arnold Beckmann

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