slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, normally in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

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

Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
Susanna F. de Rezende
Institute of Mathematics
Monday, 24. February 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 joint work with Jakob Nordström, Kilian Risse and Dmitry Sokolov.

Proof complexity of logics of bounded branching, Part 2
Emil Jeřábek
Institute of Mathematics
Monday, 3. February 2020 - 13:30 to 15:00
We revisit the problem of Frege and extended Frege (EF) lower bounds for transitive modal logics. Hrubes proved an exponential lower bound on the number of lines in Frege proofs, or equivalently, on the size of EF proofs, for some basic modal logics such as K, K4, S4, and GL. This was extended by Jerabek to an exponential separation between EF and substitution Frege (SF) systems for all transitive logics of unbounded branching.

On the other hand, for typical logics of bounded width, the EF and SF systems are p-equivalent, and they are in a certain sense p-equivalent to the classical EF system, for which we do not know any lower bounds, and even candidate hard tautologies are scarce.

The main ingredients in all the lower bounds above (as well as similar bounds for superintuitionistic logics) were variants of the feasible disjunction property (DP), playing a role similar to feasible interpolation in classical proof systems.

This raises the question what happens for... more

Proof complexity of logics of bounded branching
Emil Jeřábek
Institute of Mathematics
Monday, 27. January 2020 - 13:30 to 15:00
We revisit the problem of Frege and extended Frege (EF) lower bounds for transitive modal logics. Hrubes proved an exponential lower bound on the number of lines in Frege proofs, or equivalently, on the size of EF proofs, for some basic modal logics such as K, K4, S4, and GL. This was extended by Jerabek to an exponential separation between EF and substitution Frege (SF) systems for all transitive logics of unbounded branching.

On the other hand, for typical logics of bounded width, the EF and SF systems are p-equivalent, and they are in a certain sense p-equivalent to the classical EF system, for which we do not know any lower bounds, and even candidate hard tautologies are scarce.

The main ingredients in all the lower bounds above (as well as similar bounds for superintuitionistic logics) were variants of the feasible disjunction property (DP), playing a role similar to feasible interpolation in classical proof systems.

This raises the question what happens for... more

Pages