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.

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.

Semi-analytic Rules and Craig Interpolation

Raheleh Jalali Keshavarz
Institute of Mathematics
Monday, 12. November 2018 - 14:00 to 15:30
In one of her recent works, Iemhoff introduced the notion of a centered axiom and a centered rule as the building blocks for a certain form of sequent calculus which she calls a centered proof system. She then showed how the existence of a terminating centered system implies the uniform interpolation property for the logic that the calculus captures. In this paper we first generalize her centered rules to semi-analytic rules, a dramatically powerful generalization, and then we will show how the semi-analytic calculi consisting of these rules together with our generalization of her centered axioms, lead to the feasible Craig interpolation property. Using this relationship, we first present a uniform method to prove interpolation for different logics from sub-structural logics FL_e, FL_{ec}, FL_{ew} and IPC to their appropriate classical and modal extensions, including the intuitionistic and classical linear logics. Then we will use our theorem negatively, first to show that so many sub... more