__Journal article:__

** Samuel R. Buss.
"Bounded Arithmetic and Propositional Proof Complexity."
in **

** Download article: postscript or PDF. **

** Abstract: **This is a survey of basic facts about
bounded arithmetic and about the relationships between bounded arithmetic and
propositional proof complexity. We introduce the theories $S^i_2$ and $T^i_2$ of bounded
arithmetic and characterize their proof theoretic strength and their provably total
functions in terms of the polynomial time hierarchy. We discuss other axiomatizations of
bounded arithmetic, such as minimization axioms. It is shown that the bounded arithmetic
hierarchy collapses if and only if bounded arithmetic proves that the polynomial hierarchy
collapses. We discuss Frege and extended
Frege proof length, and the two translations from bounded arithmetic proofs into
propositional proofs. We present some theorems on bounding the lengths of propositional
interpolants in terms of cut-free proof length and in terms of the lengths of resolution
refutations. We then define the Razborov-Rudich notion of natural proofs of $P\not=\NP$
and discuss Razborov's theorem that certain fragments of bounded arithmetic cannot prove
superpolynomial lower bounds on circuit size, assuming a strong cryptographic conjecture.
Finally, a complete presentation of a proof of the theorem of Razborov is given..

__Related slides presentation:__

** Samuel R. Buss
"Bounded Arithmetic and Propositional Proofs."
NATO International Summer School on Logic of Computation.
Marktoberdorf, Germany. July-August 1995.
Five hours of lectures.**

** Download slides: postscript or PDF.**