On the Automatizability of Polynomial Calculus

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 extends to 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

• Type: Journal
• Year: 2010
• Where: MST
• Authors: Nicola Galesi, Massimo Lauria
• Keywords: MST 2010, One-side Error, Polynomial Calculus, SIAM J