Part I: Introduction to propositional proof complexity. Frege proofs, resolution, extended Frege proofs, cutting planes proofs and abstract proof systems. Connections to computational complexity. Simulations between proof systems.

Part II: Interpolation Theorems. Interpolation for resolution, monotone interpolatants, lower bounds on proof complexity. Interpolation for cutting planes and monotone real circuits. The disjunction and existence properties for intuitionistic logic are polynomial time. Interpolation and bounded arithmetic and crytographic conjectures. The possible independence of complexity conjectures from arithmetic; natural proofs.

Part III: Algebraic proof systems. The Nullstellensatz proof system and the polynomial calculus (the Grobner basis proof system). Lower bounds on degree.