CSDM: A Survey of Lower Bounds for the Resolution Proof System

The Resolution proof system is among the most basic and popular for proving propositional tautologies, and underlies many of the automated theorem proving systems in use today. I'll start by defining the Resolution system, and its place in the proof-complexity picture. A large body of work, starting in the 1960s, aimed to prove that some tautologies (represented as a disjunctive normal form formulae on n Boolean variables) require exp(n) size Resolution proofs. I will describe two different methods to prove such lower bounds and illustrate how to use them to get such exponential lower bounds on natural tautologies, such as the Pigeonhole Principle and the fact that no k-colorable graph can have a (k+1) clique. No special background will be assumed.