Fri Sep 9, 2016
60 Evans Hall, 4:10–6 PM
Sam Buss (UC San Diego)
Frege Proofs, Extended Frege Proofs, and Total NP Search Problems
This talk will discuss some of the fundamental problems of proof complexity and their connection to computational complexity. The talk focuses on the proof complexity of the Frege and extended Frege proof systems for propositional logic. Recent work includes new proofs for the pigeonhole principle (!), Frankl’s theorem, the AB=I theorem, and the Kneser-Lovasz theorem on chromatic numbers. These problems are closely related to Total NP Search Problems (TFNP), a complexity class that lies midway between P and NP. The consistency statements for exponentially large Frege and extended Frege proofs can be used to characterize the provably total functions of second-order theories of bounded arithmetic for polynomial space and exponential time.