No feasible interpolation for TC0-Frege proofs

Maria Luisa Bonet, Toniann Pitassi, Ran Raz

Research output: Contribution to journalConference article

16 Scopus citations

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).

Original languageEnglish (US)
Pages (from-to)254-263
Number of pages10
JournalAnnual Symposium on Foundations of Computer Science - Proceedings
StatePublished - Dec 1 1997
Externally publishedYes
EventProceedings of the 1997 38th IEEE Annual Symposium on Foundations of Computer Science - Miami Beach, FL, USA
Duration: Oct 20 1997Oct 22 1997

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Fingerprint Dive into the research topics of 'No feasible interpolation for TC<sup>0</sup>-Frege proofs'. Together they form a unique fingerprint.

  • Cite this