Proof Complexity Generators
=======================
We shall discuss in detail the current search for tautologies that
have no short proofs even in strong propositional proof systems like
Extended-Frege. The particular tautologies we shall discuss are
obtained from any polynomial map g (more exactly, from P/poly map
g); they express that a string is not in the range of g. The
ultimate goal is to deduce the hardness of these formulas for at
least Extended-Frege from some general, plausible computational
hardness hypothesis (a family of tautologies is said to be "hard for
a proof system P" if the tautologies in the family have no
polynomial-size proofs).
 
This talk mainly follows Jan Krajicek's paper: "Dual weak pigeonhole
principle, pseudo-surjective functions, and provability of circuit
lower bounds", Journal of Symbolic Logic, 69(1), pp. 265