Conference proceedings article:
Maria Luisa Bonet, Samuel R. Buss, Toniann Pitassi,
"Are There Hard Examples for Frege Systems?"
in Feasible Mathematics II, Birkhauser, 1995,
pp. 31-56.
Download journal article version: postscript or PDF.
Abstract: It is generally conjectured that there is
an exponential separation between Frege and extended Frege systems. This paper reviews and
introduces some candidates for families of combinatorial tautologies for which Frege
proofs might need to be superpolynomially longer than extended Frege proofs. Surprisingly,
we conclude that no particularly good or convincing examples are known. The examples of
combinatorial tautologies that we consider seem to give at most a quasipolynomial speed-up
of extended Frege proofs over Frege proofs, with the sole possible exception of
tautologies based on a theorem of Frankl.
It is shown that Bondy's theorem and a version of the
Kruskal-Katona theorem actually have polynomial-size Frege proofs. Bondy's theorem is
shown to have constant-depth, polynomial-size proofs in Frege+PHP, and to be equivalent in
$I\Delta_0$ to the pigeonhole principle.
Back to Sam Buss's publications page.