# Logic seminar

usually takes place each Monday at 14:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen
More information on the old seminar web page. The programme is announced via the mailing list.

### Clique is Hard on Average for Regular Resolution

##### Ilario Bonacina
Universitat Politècnica de Catalunya
Monday, 22. October 2018 - 14:00 to 15:30
Deciding whether a graph G with n vertices has a k-clique is one of the most basic computational problems on graphs. In this talk we show that certifying k-clique-freeness of Erdos-Renyi random graphs is hard for regular resolution. More precisely we show that, for k<<\sqrt{n}, regular resolution asymptotically almost surely requires length n^{\Omega(k)} to establish that an Erdos-Renyi random graph (with appropriate edge density) does not contain a k-clique. This asymptotically optimal result implies unconditional lower bounds on the running time of several state-of-the-art algorithms used in practice. This talk is based on on a joint work with A. Atserias, S. De Rezende, M. Lauria, J. Nordström and A. Razborov.

### Structure in Proof Complexity: The Case of Tseitin and Tree Decompositions

##### Navid Talebanfard
Institute of Mathematics
Monday, 24. September 2018 - 14:00 to 15:30
One of the main difficulties of proving lower bounds in proof complexity is that we cannot (seemingly) make structural assumptions about the proof and thus our argument should work against any conceivable proof (which may not even exist). I will survey a few old results showing that in some cases it is possible to prove structural properties of proofs of specific formulas or minimal proofs of arbitrary formulas. Then I will give a more direct proof of our result with Nicola Galesi and Jacobo Toran showing that the minimum width of Tseitin formulas is the same in general and regular resolution.

### Resolution and the binary encoding of combinatorial principles

##### Nicola Galesi
Sapienza University of Rome
Monday, 17. September 2018 - 14:00 to 15:30
We investigate the size complexity of proofs in RES(s) -- an extension of Resolution working on s-DNFs instead of clauses -- for families of contradictions given in the unusual binary encoding. A motivation of our work is to approach size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the k-Clique principle, whose Resolution complexity is still unknown. The approach is justified by the observation that for a large class of combinatorial principles short RES(log n) refutations for the binary encoding are obtained from short Resolution refutations of the unary encoding, in particular for the k-Clique principle. In the talk we show a n^{Omega(k)} lower bound for the size of refutations of the binary k-Clique Principle in RES(log log n). This improves a result of Lauria, Pudlák, Rödl and Thapen, who proved the lower bound for Resolution, that is RES(1). Resolution lower bounds for the (unary) k-... more

### An interesting (?) problem equivalent to Continuum Hypothesis

##### Pavel Hrubes
Institute of Mathematics
Monday, 4. June 2018 - 14:00 to 15:30
I will discuss a problem which came up in the context of machine learning, and which ended up being undecidable in ZFC. The flavor is similar to the so-called Axioms of Symmetry of Freiling. Based on a work with B. Shai-David, S. Moran, A. Shpilka, A. Yehudayoff.