[Proof Complexity] Tuomas Hakoniemi seminar on Monday

[thapen]

Dear colleagues,

Tuomas Hakoniemi will give a proof complexity talk in our online logic 
seminar on Monday, at 15:30 Prague time - see the announcement below.

To join go to
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)

Best,

Neil
-----

Feasible interpolation and (semi-)algebraic proof systems

Tuomas Hakoniemi, Universitat Politècnica de Catalunya

Monday, 15. February 2021 - 15:30 to 17:00

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.