文章基本信息

标题：Theories for Subexponential-size Bounded-depth Frege Proofs
本地全文：下载
作者：Kaveh Ghasemloo ; Stephen A. Cook
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：23
页码：296-315
DOI：10.4230/LIPIcs.CSL.2013.296
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system. We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon 0.
关键词：Computational Complexity Theory; Proof Complexity; Bounded Arithmetic; NC1-Frege; AC0- Frege