Logic seminar

Feasible interpolation and (semi-)algebraic proof systems

In this talk we discuss feasible interpolation for the algebraic and semialgebraic proof systems Polynomial Calculus, Sums-of-Squares and Sherali-Adams. We show that each system admits feasible interpolation in the following form: there is a poly-time algorithm that given two sets P(x,z) and Q(y,z) of polynomial constraints in distinct sequences x,y and z of variables; a refutation of the union of P(x,z) and Q(y,z) and an assignment a to the z variables, outputs either a refutation of P(x,a) or a refutation of Q(y,a). In each case the proof combines a semantic proof of the existence of a suitable resource-bounded refutation of either P(x,a) or Q(y,a) with an efficient proof search algorithm for the said refutations.