Feasible interpolation for polynomial calculus and sums-of-squares

We prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x, z) and Q(y, z) of equality constraints, a refutation Π of P(x, z) ∪ Q(y, z), and any assignment a to the variables z, one can find a refutation of P(x, a) or a refutation of Q(y, a) in time polynomial in the length of the bit-string encoding the refutation Π. For Sums-of-Squares we rely on the use of Boolean axioms, but for Polynomial Calculus we do not assume their presence. Partially funded by European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreement ERC-2014-CoG 648276 (AUTAR) and MICCIN grant TIN2016-76573-C2-1P (TASSAT3).