On interpolation and automatization for Frege systems

Maria Luisa Bonet, Toniann Pitassi, Ran Raz

Research output: Contribution to journalArticle

80 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 (of Blum integers) 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-sized TC0-Frege. As a corollary, we obtain that TC0-Frege, as well as any proof system that polynomially simulates it, is not automatizable (under the assumption that factoring of Blum integers is hard). We also show under the same hardness assumption that the k-provability problem for Frege systems is hard.

Original languageEnglish (US)
Pages (from-to)1939-1967
Number of pages29
JournalSIAM Journal on Computing
Volume29
Issue number6
DOIs
StatePublished - Apr 1 2000
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Mathematics(all)

Fingerprint Dive into the research topics of 'On interpolation and automatization for Frege systems'. Together they form a unique fingerprint.

  • Cite this