2026-07-24T18:14:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8187 2024-03-06T10:39:19Z ddc:004 open_access

Expander Construction in VNC1 Buss, Sam Kabanets, Valentine Kolokolova, Antonina Koucky, Michal expander graphs bounded arithmetic alternating log time sequent calculus monotone propositional logic 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^1 (corresponding to the "NC^1 reasoning"). As a corollary, we prove the assumption made by Jerabek (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 (2002). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sam Buss and Valentine Kabanets and Antonina Kolokolova and Michal Koucky 2017 Is Part Of LIPIcs, Volume 67, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITCS.2017.31 urn:nbn:de:0030-drops-81871 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2017.31 eng https://creativecommons.org/licenses/by/3.0/legalcode