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

in IM, rear building, ground floor

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.