No feasible interpolation for TC/sup 0/-Frege proofs
No feasible interpolation for TC/sup 0/-Frege proofs
复制标题
TC/sup 0/-Frege 证明没有可行的插值
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
R. Raz
中科院分区：
文献类型：
--
作者：
Maria Luisa Bonet;T. Pitassi;R. Raz
插值方法是证明命题证明系统下界的主要工具之一。不严格地说，如果一个人可以证明一个特定的证明系统具有可行的插值属性，那么一般的约简可以（通常）被应用于证明系统的下界，有时假设（通常是适度的）复杂性理论假设。在本文中，我们表明，这种方法不能用来获得下界的Frege系统，甚至TC/sup 0/-Frege系统。更具体地说，我们表明，除非因式分解是可行的，既不弗雷格也不TC/sup 0/-弗雷格有可行的插值属性。为了进行我们的论点，我们展示了如何进行证明的许多基本公理/定理的算术多项式大小TC/sup 0/-弗雷格。特别是，我们展示了如何进行证明的中国剩余定理，这可能是独立的利益。作为一个推论，我们得到TC/sup 0/-弗雷格以及任何证明系统，多项式模拟它，是不自动化（根据硬度假设）。
The interpolation method has been one of the main tools for proving lower bounds for propositional proof systems. Loosely speaking, if one can prove that a particular proof system has the feasible interpolation property, then a generic reduction can (usually) be applied to prove lower bounds for the proof system, sometimes assuming a (usually modest) complexity-theoretic assumption. In this paper, we show that this method cannot be used to obtain lower bounds for Frege systems, or even for TC/sup 0/-Frege systems. More specifically, we show that unless factoring is feasible, neither Frege nor TC/sup 0/-Frege has the feasible interpolation property. In order to carry out our argument, we show how to carry out proofs of many elementary axioms/theorems of arithmetic in polynomial-size TC/sup 0/-Frege. In particular, we show how to carry out the proof for the Chinese Remainder Theorem, which may be of independent interest. As a corollary, we obtain that TC/sup 0/-Frege as well as any proof system that polynomially simulates it, is not automatizable (under a hardness assumption).