slideshow 3

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.

Polynomial calculus space and resolution width

Neil Thapen
Institute of Mathematics
Monday, 25. February 2019 - 14:00 to 15:30
Let w(F) be the width needed to refute a CNF F in resolution. It is well known that the space needed to refute F in resolution is lower bounded by w(F), and it has been open whether something similar holds for polynomial calculus (PCR).  We show, by a novel 'forcing' argument, that the space needed to refute F in PCR is lower bounded by the square root of w(F). Joint work with Nicola Galesi and Leszek Kolodziejczyk.

Lower Bounds for Resolution with Linear Equations over a Ring

Fedor Part
Royal Holloway, University of London
Monday, 17. December 2018 - 14:00 to 15:30
The proof system Res(lin_R) is an extension of Resolution in which proof lines are disjunctions of linear equations over a ring R. If R is a finite field GF(p), Res(lin_R) can be viewed as a "minimal" fragment of bounded depth Frege system with counting gates AC^0[p]-Frege (and similarly, for R the integers and the TC^0-Frege), for which no nontrivial lower bound is known.

Recent suggested approaches for obtaining lower bounds against Res(lin_GF(2)) refutations include feasible interpolation and combinatorial techniques. In this talk we explore and develop further the combinatorial approach for various rings R. In particular, we prove an exponential-size dag-like Res(lin_F) lower bound for the Subset Sum principle with large coefficients, as well as establish a host of new tree-like lower bounds and separations over different fields. Based on a joint work with Iddo Tzameret.

DRAT proofs without new variables

Neil Thapen
Institute of Mathematics
Monday, 10. December 2018 - 14:00 to 15:30

The DRAT proof system is used by modern SAT solvers to witness that a CNF is unsatisfiable. The full system allows you to freely introduce new variables, and is as strong as extended resolution. I will discuss some upper and lower bounds on a restricted system, in which you cannot introduce new variables. This is ongoing work with Sam Buss.

Semi-analytic rules and uniform interpolation

Raheleh Jalali Keshavarz
Institute of Mathematics
Monday, 19. November 2018 - 14:00 to 15:30

In her recent works, Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform interpolation property of the super-intuitionistic logic that the calculus captures. In this talk, we will generalize this relationship to also cover the substructural setting on the one hand and a much more powerful class of rules on the other. The resulted relationship then provides a uniform method to establish uniform interpolation property for the logics FL_e, FL_{ew}, CFL_e, CFL_{ew}, IPC, CPC and their K and KD-type modal extensions. More interestingly though, on the negative side, we will show that no extension of FL_e can enjoy a certain natural type of terminating sequent calculus unless it has the uniform interpolation property. It excludes almost all super-intutionistic logics and the logics K4 and S4 from having such a reasonable calculus.