Phuong Nguyen (Montreal):

Witnessing problems for quantified propositional proof systems
(a talk at the 2010 Fall School)

Given a proof of a tautology in quantified propositional logic of the form \exists x_1 ... x_m B(x_1, ..., x_m) the witnessing problem is to compute some values for x_1 ... x_m that satisfy B. The complexity of this problem depends on the proof system under consideration and the set of formulas B. Typically it is complete for the complexity class definable in the bounded arithmetic theory associated with the proof system. The problem also plays a role in proving the soundness (i.e., the reflection principle) for the proof system. I will survey some results on this problem and related issues, including brief discussion on propositional translations from bounded arithmetic theories to propositional proof systems and proofs of the reflection principles.

Suggested materials:
Krajicek's "Bounded arithmetic, propositional logic, and complexity theory" Chapters 4, 7, 9,
Buss's chapters in "Handbook Proof Theory",
and Chapters 7, 10 in Cook & Nguyen's "Logical Foundations of Proof Complexity".

I assume familiarity with the polynomial time hierarchy and theories of bounded arithmetic.