I will present some views on the structure of proof complexity and possible research directions, illustrating them by some theorems and problems.

Chair: Pavel Pudlak, Neil Thapen

More information on the old seminar web page. The programme is announced via the mailing list.

Charles University

Monday, 23. April 2018 - 14:00 to 15:30

I will present some views on the structure of proof complexity and possible research directions, illustrating them by some theorems and problems.

IM CAS

Monday, 16. April 2018 - 14:00 to 15:30

In the 3rd part we will show how to reduce the disjoint NP pairs of the games we introduced in the 2nd part to the canonical pairs of bounded depth Frege systems. To this end we will use the proof system equivalent to bounded depth Frege introduced in the 1st part. Given a refutation of A(x) & B(y) in this system, we will define a game and show that a satisfying assignment for A(x) (resp. B(y)) can be transformed into a positional winning strategy for Player I (resp. II).

Sapienza University of Rome

Monday, 9. April 2018 - 14:00 to 15:30

Hindman's Finite Sums Theorem states that any finite coloring of the positive integers admits an infinite sequence such that any sum of finitely many distinct elements from that sequence has the same color. Some interesting open problems exist related to this theorem both in Combinatorics and in Computable or Reverse Mathematics. The best lower and upper bound known locate the strength of the theorem between the Halting Set and Arithmetical Truth, leaving a huge gap in-between. These bounds, due to Blass, Hirst and Simpson, have not been improved since the Eighties. Hindman, Leader and Strauss asked in 2003 whether there exists a proof of the restriction of Hindman's Theorem to sums of one or two elements that does not prove the full theorem. The question is still open and can be made precise in the context of Computable or Reverse Mathematics. We report on recent results on the strength of restrictions of Hindman's Theorem. For example we show that the known lower... more

Universitat Politècnica de Catalunya

Monday, 26. March 2018 - 14:00 to 15:30

I will start with a (partial) survey of some recent results on the proof complexity of the graph isomorphism problem with a surprising outcome: for certifying that two graphs are non isomorphic, Polynomial Calculus over the reals, Sherali-Adams, and Sums-of-Squares proofs are equally powerful (or weak). I will try to convey why I think this outcome is surprising. Then I will link this topic to the area of perfect strategies in quantum information games. We show that there are graphs that are quantum isomorphic but not classically isomorphic, and a complete characterization of the Boolean constraint languages that admit instances that are quantum but not classically realizable.