文章基本信息

标题：Implicit proofs
本地全文：下载
作者：Jan Krajicek
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2003
卷号：2003
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We describe a general method how to construct from a propositional proof system P a possibly much stronger proof system iP. The system iP operates with exponentially long P-proofs described ``implicitly'' by polynomial size circuits. As an example we prove that proof system iEF, implicit EF, corresponds to bounded arithmetic theory V^1_2 and hence, in particular, polynomially simulates the quantified propositional calculus G and the \Pi^b_1-consequences of S^1_2 proved with one use of exponentiation. Furthermore, the soundness of iEF is not provable in S^1_2. An iteration of the construction yields a proof system corresponding to T_2 + Exp and, in principle, to much stronger theories.
关键词：bounded arithmetic , Extended Frege system , Propositional Proof System