__Preprint:__

** Samuel R. Buss.
"Bounded Arithmetic and Constant Depth Frege Proofs."
In **

** Download journal article version: postscript
or PDF. **

__Abstract__ We discuss the Paris-Wilkie
translation from bounded arithmetic proofs to bounded depth propositional
proofs in both relativized and non-relativized forms. We describe normal forms
for proofs in bounded arithmetic, and a definition of Σ'-depth
for PK-proofs that makes the translation from bounded arithmetic to
propositional logic particularly transparent. Using this, we give new proofs of
the witnessing theorems for S^1_2 and T^1_2; namely, new proofs that the
$\Sigma^b_1$-definable functions of~ S^1_2 are polynomial time computable and
that the $\Sigma^b_1$-definable functions of T^1_2 are in Polynomial Local
Search (PLS). Both proofs generalize to $\Sigma^b_i$-definable functions of
S^i_2 and T^i_2. ** **

__Conference Presentation:__

** Samuel R. Buss.
"Bounded Arithmetic and Bounded Depth Propositional Proofs."
Takeuti Symposium
Symposium on Mathematical Logic '03
Kobe, Japan, December 2003.**

** Workshop on Complexity Theory
Banff International Research Station (BIRS)
Banff, Canada, July 2004. **

** Download slides from conference presentation:
postscript or PDF. **