Logical aspects of complexity theory
Course code: tba (winter semester of 2011/12)
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.
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),
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.
S. Buss, P. Pudlak: On the computational content of intuitionistic
propositional proofs Annals of Pure and Applied Logic 109 (2001), pp.
N. Thapen and A. Skelley, "The provably total search problems of bounded