Samuel R. Buss.
    "Bounded Arithmetic and Constant Depth Frege Proofs." 
    In Complexity of Computations and Proofs, edited by J. Krajicek,
         Quaderni di matematica, vol 13,
         Dipartimento de Matematica della Seconda Universita di Naoli,
 2004, pp 153-174.

    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

Back to Sam Buss's publications page.