# 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