Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR16-144 | 30th December 2016 21:36

Expander Construction in VNC${}^1$

RSS-Feed




Revision #2
Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky
Accepted on: 30th December 2016 21:36
Downloads: 246
Keywords: 


Abstract:

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [Annals of Mathematics, 2002], and show that this analysis can be formalized in the bounded-arithmetic system $VNC^1$ (corresponding to the ``$NC^1$ reasoning''). As a corollary, we prove the assumption made by Jerabek [Annals of Pure and Applied Logic, 2011] that a construction of certain bipartite expander graphs can be formalized in $VNC^1$. 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 [Journal of Computer and System Sciences, 2002].



Changes to previous version:

Corrected some typos and minor errors.


Revision #1 to TR16-144 | 13th October 2016 15:02

Expander Construction in VNC${}^1$





Revision #1
Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky
Accepted on: 13th October 2016 15:02
Downloads: 239
Keywords: 


Abstract:

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [Annals of Mathematics, 2002], and show that this analysis can be formalized in the bounded-arithmetic system $VNC^1$ (corresponding to the ``$NC^1$ reasoning''). As a corollary, we prove the assumption made by Jerabek [Annals of Pure and Applied Logic, 2011] that a construction of certain bipartite expander graphs can be formalized in $VNC^1$. 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 [Journal of Computer and System Sciences, 2002].



Changes to previous version:

Corrected some errors, and added some references (updating the related work).


Paper:

TR16-144 | 15th September 2016 23:01

Expander Construction in VNC${}^1$





TR16-144
Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky
Publication: 15th September 2016 23:02
Downloads: 464
Keywords: 


Abstract:

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [Annals of Mathematics, 2002], and show that this analysis can be formalized in the bounded-arithmetic system $VNC^1$ (corresponding to the ``$NC^1$ reasoning''). As a corollary, we prove the assumption made by Jerabek [Annals of Pure and Applied Logic, 2011] that a construction of certain bipartite expander graphs can be formalized in $VNC^1$. 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 [Journal of Computer and System Sciences, 2002].



ISSN 1433-8092 | Imprint