The seminar studies this semester "Logic and Computational Complexity".
The literature is listed by the topics we plan to look at and it may
grow as we progress.
Most material can be found also in
the book
available at my page: references below to Chpt.x or Sec.y
refer to chapters and sections in this book.
In particular, logic and complexity theory background can be found in Sections 1.1-1.3
there.
You may also get an overall idea of the general area from
the syllabus page of a related course
(the course will
advanced though; here we look at some simple cases).
Fagin's theorem, spectra
A chapter from E.Graedel's book or
M.Otto's
lecture notes (Chpt.6 there).
Sec.1.2.
Herbrand's theorem, the KPT theorem, the Student-Teacher game
Sec.12.2 and
an expository article.
Total NP search problems
Original sources: Papadimitriou
and Johnson -
Papadimitriou - Yannakakis.
Proof systems and algorithms
Sections 5.1-5.2: resolution and the relations between R^* and DPLL procedures.
Section 5.3:
read-once branching programs and regular resolution proofs.
HW: a branching program that cannot be
decorated as a resolution refutation.
Section
6.3: integer linear programming and the cutting plane method and proof system.
Quantitative Godel's theorem and optimal proof systems
For the bounds:
Pudlak's paper.
Links with optimal proof systems:
paper or Section 21.3.
