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.

Abstract

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.

Date	Topic	Lecture note
Oct, 20th (Tue)	Proof systems; resolution	lecture 1
Oct, 23th (Fri)	Resolution lower bound for Pigeohole principle	lecture 2
Oct, 27th (Tue)	Lower bounds based on resolution width	lecture 3
Nov, 6th (Fri)	Polynomial calculus and Proof search	lecture 4
Nov, 10th (Tue)	Lower bounds for Polynomial calculus	lecture 5
Nov, 13th (Fri)	Cutting planes: interpolation and lower bounds	lecture 6
Nov, 17th (Tue)	SAT solvers in theory and practice	lecture 7
Nov, 20th (Fri)	Space complexity and resolution	lecture 8
Nov, 24th (Tue)	Pebbling tautologies and space-length trade-offs	lecture 9
Nov, 27th (Fri)	Extended frege; extracting computation from proofs	lecture 10

Problem sets

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