On the Automatizability of Polynomial Calculus.

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 extends to Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Comput. 38(4):1347–1363, ). [ABSTRACT FROM AUTHOR]