DIMACS Summer School on Applied Logic
Tutorial on Proof Complexity and Feasible Arithmetic
Tentative Schedule and Syllabus
Monday, August 21
9:30-10:30 Basic Bounded arithmetic up to 1st Witnessing theorem.
11:00-12:00 Bounded arithmetic, continuation.
1:30-2:30 Basic Proof complexity and polynomial simulations for Frege, EF
3:00-4:30 Basic proof complexity, continuation.
Tuesday, August 22
9:30-10:30 Bounded Arithmetic continuation
11:00-12:00 Bounded Arithmetic continuation
1:30-3:00 Proof complexity: polynomial simulations and upper bounds
3:30-4:45 Bounded Arithmetic <-> Proof Complexity Translations
Wednesday, August 23
9:30-10:30 Bounded Arithmetic, conclusion
11:00-12:00 Resolution Lower bounds
1:30-2:30 Resolution Lower bounds, continuation.
2:45-3:45 Bounded-depth Frege lower bounds, introduction
4:00-5:00 Informal Rump Session
Thursday, August 24
9:30-10:30 Proof of bounded-depth Frege lower bounds--the Switching Lemmas
11:00-12:00 Conclusion of proof of PHP lower bound.
1:30-2:30 Additional Axioms in Bounded-depth Frege
3:00-4:45 Cutting Planes/Interpolation
Friday, August 25
9:30-10:30 Natural Proofs
11:00-12:00 Natural Proofs, continuation
1:30-3:00 Nullstellensatz Proofs
3:30-4:30 Informal Rump Session