Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček

More information on the old seminar web page. The programme is announced via the mailing list.

St. Petersburg Department of Steklov Institute of Mathematics and Euler International Mathematical Institute

Monday, 10. January 2022 - 16:00 to 17:30

in IM, rear building, ground floor - *not broadcast*

We consider a framework for proving lower bounds on the length of proofs in logical calculi that can be seen as a generalization of the game framework in which Pudlák presented Haken's lower bound for resolution. Our framework, while still requiring some notion of width, can be applied in a way that avoids the use of the random restriction technique. As an example, we demonstrate this for resolution, obtaining a proof in which the calculations are very simple.

National University of Singapore

Monday, 13. December 2021 - 13:00 to 14:30

https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join

Arithmetic generally does not admit any non-trivial quantifier elimination. I will talk about one exception, where the negation of an induction axiom is included in the theory. Here the Weak Koenig Lemma from reverse mathematics arises as a model completion.

This work is joint with Marta Fiori-Carones (Novosibirsk), Leszek Aleksander Kolodziejczyk (Warsaw) and Keita Yokoyama (Sendai).

This work is joint with Marta Fiori-Carones (Novosibirsk), Leszek Aleksander Kolodziejczyk (Warsaw) and Keita Yokoyama (Sendai).

University of Oxford

Monday, 6. December 2021 - 16:00 to 17:30

Zitna, rear building, ground floor and zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join

We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system P, we prove that the following statements are equivalent,

1. Provable learning: P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries.

2. Provable automatability: P proves efficiently that P is automatable by non-uniform circuits on propositional formulas expressing p-size circuit lower bounds.

Here, P is sufficiently strong and well-behaved if I.-III. holds: I. P p-simulates Jeřábek's system WF (which strengthens the Extended Frege system EF by a surjective weak pigeonhole principle); II. P satisfies some basic properties of standard proof systems which p-simulate WF; III. P proves efficiently for some Boolean function h that h is hard on average for circuits of subexponential size. For example, if III. holds... more

Institute of Mathematics

Monday, 29. November 2021 - 16:00 to 17:30

*NOT BROADCAST* in IM, rear building, ground floor

For a field F, char(F) > 3, and an affine map A : F^n -> F^m we form a contradiction by picking some b not in A({0,1}^n) and saying Ax = b. This can be written as a system of 0-1 unsatisfiable linear equations over F expressible in the language of algebraic proof systems like Res(lin), NS, PC over F. One may think of these instances as the Subset Sum principle in positive characteristic. I'll suggest some hardness criterions for such instances and prove lower bounds for linear decision trees, tree-like Res(lin) and some restricted dag-like Res(lin) refutations. I'll also discuss work in progress on lower bounds for general dag-like Res(lin) refutations and PC refutations of these instances.

Institute of Mathematics

Monday, 15. November 2021 - 16:00 to 17:30

*NOT BROADCAST* - IM large seminar room, rear building, ground floor

We will start by recalling what is currently known about the hardness of refuting the clique formula on random graphs. We will then sketch some ideas on how to generalize these results to stronger proof systems.

University of Connecticut and Charles University

Monday, 8. November 2021 - 16:00 to 17:30

Zitna, back building, first floor (by offices) and zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join

I will give a brief introduction to reverse mathematics, focusing on computable combinatorics, and survey some recent trends and results in the subject. No prior background beyond basic logic is necessary.