Computer Science/Discrete Mathematics Seminar II

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.