Title :
No feasible interpolation for TC0-Frege proofs
Author :
Bonet, Martia Luisa ; Pitassi, Toniann ; Raz, Ran
Author_Institution :
Dept. de Llenguatges i Sistemes Inf., Univ. Politecnica de Catalunya, Barcelona, Spain
Abstract :
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 TC0-Frege systems. More specifically, we show that unless factoring is feasible, neither Frege nor TC0-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 TC0 -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 TC0-Frege as well as any proof system that polynomially simulates it, is not automatizable (under a hardness assumption)
Keywords :
computational complexity; interpolation; theorem proving; Chinese Remainder Theorem; TC0-Frege proofs; complexity-theoretic assumption; feasible interpolation; hardness assumption; lower bounds; proof systems; Arithmetic; Artificial intelligence; Boolean functions; Business process re-engineering; Circuits; Computer science; Interpolation; Large scale integration; Polynomials; Radio access networks;
Conference_Titel :
Foundations of Computer Science, 1997. Proceedings., 38th Annual Symposium on
Conference_Location :
Miami Beach, FL
Print_ISBN :
0-8186-8197-7
DOI :
10.1109/SFCS.1997.646114