Propositional proof complexity is the study of the resources that are needed to prove formulas in propositional logic. Originally developed as an approach to the P vs NP problem, nowadays proof complexity has got a life of its own, with one salient application being unconditional lower bounds for search algorithms. In this talk we will discuss some proof systems with such applications, namely resolution, polynomial calculus, and cutting planes; and review what are they, which complexity measures we can associate, interesting upper and lower bounds, and if time permits some open problems.
