Fall school - Prague 2009

Syllabus

This web page gives a brief syllabus for tutorials at the Fall school, and also lists a few prerequisites. More details may be added later on, as well as the actual schedulle of talks.

Sam Buss's lectures

I plan to lecture in part on my joint work with Beckmann on relativized PLS for fragments of bounded arithmetic.

Other topics I will cover include Paris-Wilkie translations and bounded depth Frege systems.

Prerequisites:

Understanding bounded arithmetic up through
(a) Witnessing theorems for S^i_2, and
(b) Witnessing theorem for T^1_2 based on PLS functions.
Basics of proof complexity. Frege systems and bounded depth Frege systems.
Other background material: Basics of first order logic up through completeness, incompleteness and cut elimination.
Basics of complexity up through the polynomial time hierarchy.

Source material for the first items:
  • My thesis up through Chapter 6, avaliable online.
  • Krajicek's book Bounded Arithmetic, Propositional Logic and Complexity Theory.
  • First 35 pages of my survey article "Bounded Arithmetic and Propositional Proof Complexity", available online.

    Ran Raz's lectures

    I will talk about algebraic circuits. The first hour will be introductory. The second will cover some of the classical staff, e.g. Strassen's lower bound of n log n for circuit size. The third will probably be about multilinear complexity, probably my proof for superpolynomial lower bounds for multilinear formulas for determinant and permanent, and the forth will probably be about problems that imply lower bounds for general circuits and formulas.

    No prerequisites.

    Pavel Pudlak's lectures

    "Lower bounds on proofs in algebraic and integer linear programing proof systems"

    We shall survey these proof systems focusing on the feasible interpolation property which in some cases enables one to prove lower bounds. We shall present some open problems suitable for further research.

    Neil Thapen's lectures

    "NP search problems for the bounded arithmetic hierarchy"

    I will present the main result of the paper "The provably total search problems of bounded arithmetic" by Alan Skelley and myself, where we characterize the provable NP search problems of the kth level of the bounded arithmetic hierarchy in terms of the "game induction principle" about long sequences of k-turn games. The bulk of the tutorials will involve showing how first-order bounded arithmetic proofs can be translated into large, uniform propositional proofs in a certain proof system, and how soundness for these propositional proofs can be witnessed by long sequences of games. Depending on the time available I will go on to talk about some applications and possible extensions to stronger theories.

    Prerequisites:

    I will assume that the audience knows the basics of:
    1. The polynomial time hierarchy.
    2.NP search problems and reductions between search problems.
    Remark: There will be one introductory lecture by Jan Krajicek covering basics of this material but it cannot harm to look at it in advance.
    3. The bounded arithmetic hierarchy, formalization of polynomial time computation, sequent calculus
    4. Propositional proof systems, resolution and bounded depth Frege, translations from first-order into propositional proofs.

    A possible reference for 2 is the introduction of "The complexity of the parity argument and other inefficient proofs of existence" Papadimitriou, 1991.
    Possible references for 3 and 4 are Buss' two sections in the "Handbook of Proof Theory", in particular 1.2.14 (Tait calculus), 1.3-1.3.4 (resolution), 2.4 (structure of LK proofs); and Buss' survey article "Bounded arithmetic and propositional proof complexity" (1997), in particular sections 1,2,3 (but not the details of the witnessing proof), 4, 5, 6.4.