Proof complexity

Spring 2005, code TIN068,
Czech title: Dukazova slozitost

Extent: 2/0, an exam at the end of the course.

Time and place: Wednesday 15.00 - 16.30, MU (Zitna 25, Praha 1), seminar room on the 3rd floor.

Lectures will be in English as a courtesy to our foreign students and postdocs.
Lecturer: Jan Krajicek

Proof complexity is an area connecting mathematical logic with computational complexity theory. Fundamental open problems are the relations between the classes P, NP, and coNP. A particular problem (the main problem in proof complexity) is this: Does there exists a propositional proof system in which every tautology has a short (polynomial or at least sub-exponential in size) proof? A general proof system is simply a non-deterministic algorithm accepting exactly propositional tautologies (one can interpret all usual propositional calculi in this way). This question is equivalent to the problem whether the class NP is closed under the complementation. The goal is to show that no such proof system exists: We want to prove lower bounds on the lengths of proofs (i.e. on the non-deterministic time) in all possible proof systems.
We will cover basic information about proof systems, some of the main lower bounds, and constructions of a selection of interesting short proofs and proof simulations. The lecture will be largely combinatorial but, if time permits, we shall also cover some deeper links with logic (in particular, to the so called bounded arithmetic).


I shall expect that the participants of the course are familiar with basic concepts of mathematical logic and of computational complexity theory on an undergraduate level (e.g., formal logical systems, p-time computations, NP-completeness, boolean circuits).


Lecture notes containing most of the material to be covered. Additional material.

Interested to attend?

If you are potentially interested to attend the lectures, send me an email ( - we shall negotiate (at the beginning of the semester) a suitable time schedule via email.