Auto

Theory Comput Syst DOI 10.1007/s00224-009-9195-5

On the Automatizability of Polynomial Calculus
Nicola Galesi · Massimo Lauria

© Springer Science+Business Media, LLC 2009

Abstract We prove that Polynomial Calculus and Polynomial Calculus with Resolution are not automatizable, unless W [P ]-hard problems are fixed parameter tractable by one-side error randomized algorithms. This extendsto Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Comput. 38(4):1347–1363, 2008). Keywords Automatizability · Polynomial calculus · Proof complexity · Degree lower bound

1 Introduction Automated theorem proving is one of the most important fields investigated both from a theoretical and an applied point of view. It is widely conjectured (butstill far to be proved) that for any proof system we have families of tautologies requiring exponentially long proofs. For several concrete examples (e.g. Resolution) we know such a result (see for Resolution, among many others, [5, 6, 13]). Hence investigating automated theorem proving from a theoretical point of view, we should consider proof searching algorithms for a system S as “efficient” ifon any formula F , they produce a proof of F efficiently in the size of the best proof of A in S. Automatizability is a property for proof systems introduced by Bonet et al. in [8], which captures the discussion above: a proof system S is automatizable if there exists

Research of N. Galesi was supported by La Sapienza research projects: (1) “Algoritmi efficienti su modelli avanzati dicomunicazione e di calcolo” and (2) “Limiti di compressione in combinatoria e complessit computazionale”. Research of M. Lauria was partially founded by the grant #13393 of Templeton Foundation. N. Galesi · M. Lauria ( ) Department of Computer Science, Sapienza—Università di Roma, Roma, Italy e-mail: lauria.massimo@gmail.com

Theory Comput Syst

an algorithm AS such that on any tautology F , AS producesa proof of F in S in time polynomially bounded in the size of the shortest proof of F in S. This definition is interesting since it makes the existence of efficient proof searching algorithms for a specific proof system independent from the existence of hard formulas. Recently the notion of automatizability was improved and tightened for applications. Atserias and Bonet in [4] introduced the notionof weak automatizability of a proof system. S is weakly automatizable if there exists a proof system S that efficiently simulates S and that moreover is automatizable. In general it appears that the stronger the proof system is the lesser is the chance that the proof system is automatizable. Krajícek and Pudlák [17], proved that Extended Frege systems are not automatizable under widely acceptedcryptographic conjectures. They did it by exploiting the connection found by Bonet et al. in [8] that automatizability implies Feasible Interpolation Property [8, 16]. Later [7, 8], extended this result down to bounded-depth Frege but weakening the cryptographic assumption considered. This line of proving non automatizability was not suitable for systems, like Resolution, known to have the FeasibleInterpolation Property. In a major breakthrough Alekhnovich and Razborov [2], proved that even Resolution is not automatizable unless some parameterized complexity assumption, believed to be false, does hold. Polynomial Calculus (shortened as P C) is an algebraic refutational proof system introduced in [9] based on deriving polynomials. In the analysis of the complexity of proofs in P C (see [18]for a survey on algebraic systems) we deal with two parameters: the maximal degree of a polynomial used in the proof, and the number of monomials in the proof (usually referred to as size). It is known (see [9, 18]) that constant degree P C is automatizable. In [9] it is shown an algorithm based on the Gröbner Basis which finds a P C proof of a set of polynomials P over n variables in time nO(d) ,...