Logical aspects of complexity theory
Course code: tba (winter semester of 2011/12)
Pavel Pudlak
Time and place: see the special semester page.
Proof complexity studies problems of computational complexity from the point of view of logic and analogous problems concerning complexity in logic. In this lecture we will focus on the problem how to obtain efficient computations from proofs. We will study proofs in weak arithmetics formalized in first order logic, as well as proofs in various proof systems for propositional logic. The typical examples of theorems that we will prove are the so called witnessing theorems and theorems about feasible interpolation. We will also study sentences unprovable in weak arithmetics.References:
J. Krajicek: "Bounded arithmetic, propositional logic, and complexity theory", Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, (1995).
J. Krajicek: "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic", J. of Symbolic Logic, 62(2), (1997), pp.457-486.
J. Krajicek and P. Pudlak: "Some consequences of cryptographical conjectures for $S^1_2$ and $EF$". Information and Computation, Vol. 140 (1), (1998), pp.82-94.
P. Pudlak: On the complexity of propositional calculus. Sets and Proofs, Invited papers from Logic Colloquium'97, Cambridge Univ. Press 1999, pp. 197-218.
S. Buss, P. Pudlak: On the computational content of intuitionistic propositional proofs Annals of Pure and Applied Logic 109 (2001), pp. 49-64.
N. Thapen and A. Skelley, "The provably total search problems of bounded arithmetic", (preprint)