We describe a general method how to construct from
a propositional proof system P a possibly much stronger
proof system iP. The system iP operates with
exponentially long P-proofs described ``implicitly''
by polynomial size circuits.

As an example we prove that proof system iEF, implicit EF,
corresponds to bounded ... more >>>