
Frege system
F_d versus F_{d+1} โ โ โ
Author(s): Krajicek
Problem Find a constant
such that for any
there is a sequence of tautologies of depth
that have polynomial (or quasi-polynomial) size proofs in depth
Frege system
but requires exponential size
proofs.






Keywords: Frege system; short proof
