Preprint:

    Sam Buss, Valentine Kabanets, Antonina Kolokolova and Michal Koucký
    "Expander Construction in VNC¹"
    Annals of Pure and Applied Logic 107, 7 (2020) Article 102796 (40 pages).
    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 VNC¹ (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 VNC¹. 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. In Proceedings, 8th Conference on Innovations in Computer Science (ITCS), 2017.

Related talk at Takeuti Symposium on Advances in Logic, September 20, 2018.
    Talk slides.

Back to Sam Buss's publications page.