slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom, normally 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.

On the proof complexity of Resolution over Polynomial Calculus

Erfan Khaniki
Institute of Mathematics
Monday, 30. March 2020 - 13:30 to 15:00
The refutation system Res_R(PC_d) is a natural extension of the Resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called Res_R(lin). One of the important open problems in Proof Complexity is proving lower bounds for Res_R(lin) when R is a finite field such as F_2. Interestingly, Res_{F_2}(lin) is fairly strong, and there is no known nontrivial lower bound for it, but for Res^*_R(lin) (tree-like Res_R(lin)) we know exponential lower bounds for every finite field.

For the stronger systems Res_R(PC_d) and Res_R^*(PC_d) for d>1 on finite ring R, there is no known lower bounds. In this talk, we prove a size-width relation for Res_R(PC_d) and Res^*_R(PC_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for Res and Res^* using extension variables. As a by product, we get the... more

Proof-theoretic analysis of some impredicative theories, Part 2

Fedor Pakhomov
Institute of Mathematics
Monday, 23. March 2020 - 13:30 to 15:00
In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.

Proof-theoretic analysis of some impredicative theories

Fedor Pakhomov
Institute of Mathematics
Monday, 9. March 2020 - 13:30 to 15:00
In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.

Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs, Part 2

Susanna F. de Rezende
Institute of Mathematics
Monday, 2. March 2020 - 13:30 to 15:00
In this talk, we will present Razborov's pseudo-width method and explain how it can be extended to obtain exponential resolution lower bounds for the weak pigeonhole principle (PHP) and perfect matching formulas over highly unbalanced, sparse expander graphs. Our result establishes strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking other longstanding open problems for resolution and other proof systems. This is... more

Pages