License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITCS.2017.31
URN: urn:nbn:de:0030-drops-81871
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/8187/
Go to the corresponding LIPIcs Volume Portal

Buss, Sam ; Kabanets, Valentine ; Kolokolova, Antonina ; Koucky, Michal

Expander Construction in VNC1

pdf-format:
LIPIcs-ITCS-2017-31.pdf (0.6 MB)

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^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).

BibTeX - Entry

@InProceedings{buss_et_al:LIPIcs:2017:8187,
  author =	{Sam Buss and Valentine Kabanets and Antonina Kolokolova and Michal Koucky},
  title =	{{Expander Construction in VNC1}},
  booktitle =	{8th Innovations in Theoretical Computer Science Conference (ITCS 2017)},
  pages =	{31:1--31:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-029-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{67},
  editor =	{Christos H. Papadimitriou},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/8187},
  URN =		{urn:nbn:de:0030-drops-81871},
  doi =		{10.4230/LIPIcs.ITCS.2017.31},
  annote =	{Keywords: expander graphs, bounded arithmetic, alternating log time, sequent calculus, monotone propositional logic}
}

Keywords: expander graphs, bounded arithmetic, alternating log time, sequent calculus, monotone propositional logic
Collection: 8th Innovations in Theoretical Computer Science Conference (ITCS 2017)
Issue Date: 2017
Date of publication: 28.11.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI