slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, normally in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

Automating Algebraic Proof Systems is NP-Hard

Susana F. de Rezende
Monday, 11. May 2020 - 13:30 to 15:00
Recently, Atserias and Müller (FOCS 2019) established that it is NP-hard to find a resolution refutation of an unsatisfiable formula in time polynomial in the size of the shortest such refutation. In this talk, I will present a simplified proof of this result and explain how it can be extended to hold also for Nullstellensatz, Polynomial Calculus, and Sherali–Adams. This is based on joint work with Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere and Dmitry Sokolov.

Semi-Algebraic Proofs, IPS lower bounds and the tau-Conjecture

Iddo Tzameret
Royal Holloway, University of London
Monday, 4. May 2020 - 13:30 to 15:00
We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2014). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes, Shpilka, Tzameret and Wigderson (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning,... more

Reflection principles in the propositional calculus, Part 2

Pavel Pudlák
Monday, 27. April 2020 - 13:30 to 15:00
I will survey some results on the reflection principles for propositional proof systems, show a connection to the recent result on non-automatibility of Resolution and ask several problems.

H-Coloring Dichotomy in Proof Complexity

Azza Gaysin
Charles University
Monday, 20. April 2020 - 13:30 to 15:00
The H-Coloring problem can be considered as an example of the computational problem from a huge class of constraint satisfaction problems (CSP): an H-Coloring of a graph G is just a homomorphism from G to H. The dichotomy theorem for H-Coloring was proved by Hell and Nešetřil (an analogous theorem for all CSPs was recently proved by Zhuk and Bulatov) and it says that for each H the problem is either p-time decidable or NP-complete. Since negations of unsatisfiable instances of CSP can be expressed as propositional tautologies, it seems to be natural to investigate the proof complexity of CSP.

We show that the decision algorithm in the p-time case of the H-Coloring can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have short proofs in propositional proof system R^*(log). We complement this upper bound result by a lower bound result for the special example of NP-complete case of the H-Coloring, using the... more