[Proof Complexity] Seminar Fri May 28 at 14:00 CEST with Tuomas Hakoniemi: Feasible interpolation for algebraic proof systems

[Jakob Nordström]

Dear all,

On Friday May 28 at 14:00 CEST we will have a seminar with Tuomas Hakoniemi from Universitat Politècnica de Catalunya in Barcelona titled "Feasible interpolation for algebraic proof systems". Please see the abstract below for more details.

We will meet virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming video seminars can be found at http://www.csc.kth.se/~jakobn/videoseminars/ (an address that should change soonish, but for now it is what it is). In particular, please note that we also have a seminar today Monday at 14:00 CEST with Kilian Risse from KTH Royal Institute of Technology titled "Average-case perfect matching lower bounds from hardness of Tseitin formulas".

If you do not wish to receive these announcements, or receive several copies of them, please send a message to jakob.nordstrom at cs.lth.se.

Best regards,
Jakob Nordström

**********

Friday May 28 at 14:00
Feasible interpolation for algebraic proof systems
(Tuomas Hakoniemi, Universitat Politècnica de Catalunya)

In this talk we present a form of feasible interpolation for two algebraic proof systems, Polynomial Calculus and Sums-of-Squares. We show that for both systems there is a poly-time algorithm that given two sets P(x,z) and Q(y,z) of polynomial equalities, 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). Our proofs are fairly logical in nature, in that they rely heavily on semantic characterizations of resource-bounded refutations to prove the existence of suitable refutations. These semantic existence proofs narrow down the search space for the refutations we are after so that we can actually find them efficiently.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se