Basic concepts of computational complexity theory. Definability in first-order logic.
Finite model theory. Proof complexity and SAT algorithms.
Herbrand's theorem and witnessing theorems.
The course maps connections between mathematical logic and computational complexity theory.
The course may not be taught every academic year.