Expander Construction in VNC1
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F17%3A10368745" target="_blank" >RIV/00216208:11320/17:10368745 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.4230/LIPIcs.ITCS.2017.31" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.ITCS.2017.31</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.ITCS.2017.31" target="_blank" >10.4230/LIPIcs.ITCS.2017.31</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Expander Construction in VNC1
Popis výsledku v původním jazyce
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).
Název v anglickém jazyce
Expander Construction in VNC1
Popis výsledku anglicky
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).
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
—
Návaznosti
R - Projekt Ramcoveho programu EK
Ostatní
Rok uplatnění
2017
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
8th Innovations in Theoretical Computer Science Conference (ITCS 2017)
ISBN
978-3-95977-029-3
ISSN
1868-8969
e-ISSN
neuvedeno
Počet stran výsledku
26
Strana od-do
1-26
Název nakladatele
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Místo vydání
Dagstuhl, Germany
Místo konání akce
Berkeley, CA, USA
Datum konání akce
9. 1. 2018
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—