Introduction to proof complexity - 2015

About the course

This class was taught at the Tokyo Institute of Technologies, while I was there as a visiting professor, hosted by Osamu Watanabe.


A proof is any text that can be easily verified and that convince of the absolute truth of a statement. If a statement has no short proofs, it is essentially indistinguishable from a false one. Proof complexity is the mathematical study of the length of proof, in the sense that study how long a proof must be to prove a propositional statement in particular proof system. This line of research is motivated both by the connections with deep theoretical questions like P vs NP, and by the importance that satisfiability solvers (SAT solvers) have in applications like hardware and software verification, testing, and many more. In the course we will introduce the basic facts of Proof Complexity and we will study the length of proof in the most important proof systems, we will show connections with that SAT solvers.

Lecture Calendar and schedule

Here is the complete calendar of the lectures. Lecture notes follow.

DateTopicLecture note
Oct, 20th (Tue) Proof systems; resolution lecture 1
Oct, 23th (Fri) Resolution lower bound for Pigeohole principlelecture 2
Oct, 27th (Tue) Lower bounds based on resolution widthlecture 3
Nov, 6th (Fri) Polynomial calculus and Proof searchlecture 4
Nov, 10th (Tue) Lower bounds for Polynomial calculuslecture 5
Nov, 13th (Fri) Cutting planes: interpolation and lower boundslecture 6
Nov, 17th (Tue) SAT solvers in theory and practicelecture 7
Nov, 20th (Fri) Space complexity and resolutionlecture 8
Nov, 24th (Tue) Pebbling tautologies and space-length trade-offslecture 9
Nov, 27th (Fri) Extended frege; extracting computation from proofslecture 10

Problem sets

Release dateLecture note
Oct, 27th (Tue) Problem set 1
Nov, 13th (Fri) Problem set 2
Nov, 24th (Tue) Problem set 3