In four talks I plan to cover some basic, both classical as well as recent, concepts of proof complexity. An approximate outline is:
(1) Cook-Reckhow definition, lengths of proofs, link to the NP versus coNP problem. Polynomial simulation, optimal proof systems. An overview of known lower bounds.
(2) Theories being "uniform" proof systems. Translations of arithmetical proofs into propositional proofs. Interpretation of lower bounds as constructions of models of bounded arithmetic theories.
(3) Proof complexity of (propositional) resolution. The size-width tradeoff, feasible interpolation, infinitary characterizations of hard tautologies.
(4) Hard tautologies: combinatorial principles, consistency statements, proof complexity generators.
- http://www.math.cas.cz/~krajicek/biblio.html - Relevant lecture notes and expository papers can be found