Abstract
Whereas for classical logic it seems to be an extremely difficult problem, for some non-classical logics it is possible to prove exponential lower bounds on the lengths of proofs in (system based on axioms and derivation rules). For some modal logics recently such unconditional lower bounds have been proved. For intuitionistic logic we have only results based on unproven assumptions.