TY - JOUR
T1 - On interpolation and automatization for Frege systems
AU - Bonet, Maria Luisa
AU - Pitassi, Toniann
AU - Raz, Ran
N1 - Copyright:
Copyright 2005 Elsevier Science B.V., Amsterdam. All rights reserved.
PY - 2000/4
Y1 - 2000/4
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0034478771&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0034478771&partnerID=8YFLogxK
U2 - 10.1137/S0097539798353230
DO - 10.1137/S0097539798353230
M3 - Article
AN - SCOPUS:0034478771
VL - 29
SP - 1939
EP - 1967
JO - SIAM Journal on Computing
JF - SIAM Journal on Computing
SN - 0097-5397
IS - 6
ER -