文章基本信息

标题：Expander Construction in VNC1
本地全文：下载
作者：Sam Buss ; Valentine Kabanets ; Antonina Kolokolova 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：67
页码：31:1-31:26
DOI：10.4230/LIPIcs.ITCS.2017.31
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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).
关键词：expander graphs; bounded arithmetic; alternating log time; sequent calculus; monotone propositional logic