The Resolution proof system

Computer Science/Discrete Mathematics Seminar II
Topic:The Resolution proof system
Speaker:Avi Wigderson
Affiliation:Herbert H. Maass Professor, School of Mathematics
Date:Tuesday, March 22
Time/Room:10:30am - 12:30pm/S-101
Video Link:

The Resolution proof system is perhaps the simplest and most universally used in verification system and automated theorem proving. It was introduced by Davis and Putnam in 1960. The study of its efficiency, both in terms of proof length of natural tautologies and in terms of the complexity of finding short proofs has lead over the decades to a rich understanding which is nonetheless incomplete. I will survey some of the main achievements of this study, and in particular will give a full proof of an exponential lower bound on the Resolution proof length of the pigeonhole principle and other tautologies. While this lecture is a continuation of my exposition of proof complexity, it will be completely independent and will assume nothing from the previous talk.