ECCC-Report TR16-144https://eccc.weizmann.ac.il/report/2016/144Comments and Revisions published for TR16-144en-usFri, 30 Dec 2016 21:36:50 +0200
Revision 2
| Expander Construction in VNC${}^1$ |
Valentine Kabanets,
Sam Buss,
Michal Koucky,
Antonina Kolokolova
https://eccc.weizmann.ac.il/report/2016/144#revision2We 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].Fri, 30 Dec 2016 21:36:50 +0200https://eccc.weizmann.ac.il/report/2016/144#revision2
Revision 1
| Expander Construction in VNC${}^1$ |
Valentine Kabanets,
Sam Buss,
Michal Koucky,
Antonina Kolokolova
https://eccc.weizmann.ac.il/report/2016/144#revision1We 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].Thu, 13 Oct 2016 15:02:15 +0300https://eccc.weizmann.ac.il/report/2016/144#revision1
Paper TR16-144
| Expander Construction in VNC${}^1$ |
Valentine Kabanets,
Sam Buss,
Michal Koucky,
Antonina Kolokolova
https://eccc.weizmann.ac.il/report/2016/144We 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].Thu, 15 Sep 2016 23:02:48 +0300https://eccc.weizmann.ac.il/report/2016/144