Sciweavers

Share
SIAMCOMP
2000

On Interpolation and Automatization for Frege Systems

9 years 5 months ago
On Interpolation and Automatization for Frege Systems
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). W...
Maria Luisa Bonet, Toniann Pitassi, Ran Raz
Added 19 Dec 2010
Updated 19 Dec 2010
Type Journal
Year 2000
Where SIAMCOMP
Authors Maria Luisa Bonet, Toniann Pitassi, Ran Raz
Comments (0)
books