slideshow 3

Logic seminar

Feasible interpolation and (semi-)algebraic proof systems

Tuomas Hakoniemi
Universitat Politècnica de Catalunya


Monday, 15. February 2021 - 15:30 to 17:00
Zoom meeting 472 648 284 - - contact to join
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.