Preprint:

    Sam Buss, Valentine Kabanets, Antonina Kolokolova and Michal Koucký
    "Expander Construction in VNC1"
    Full-length preprint, September 2016 (revised February 2017).
    Extended abstract, in Proceedings, 8th Conference on Innovations in Computer Science (ITCS), 2017.

    Download full-length preprint.

Abstract: We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [2002], and show that this analysis can be formalized in the bounded-arithmetic system VNC1 (corresponding to the "NC1$ reasoning"). As a corollary, we prove the assumption made in Jerabek [2011] that a construction of certain bipartite expander graphs can be formalized in VNC1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlak [2002].

    Also available: extended abstract. To appear in in Proceedings, 8th Conference on Innovations in Computer Science (ITCS), 2017.

Related talk at Prague Workshop on Bounded Arithmetic, November 2, 2017.
    Talk slides.

Back to Sam Buss's publications page.