slideshow 3

Logic seminar

usually takes place each Monday at 16:00 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.

Arithmetic under negated induction

Tin Lok Wong
National University of Singapore
Monday, 13. December 2021 - 13:00 to 14:30 - contact 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).

Learning algorithms versus automatability of Frege systems

Jan Pich
University of Oxford
Monday, 6. December 2021 - 16:00 to 17:30

Zitna, rear building, ground floor and zoom meeting 472 648 284 - - contact 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

On the Complexity of Algebraic Proofs of Membership in the Complement of an Affine Image of the Boolean Cube

Fedor Part
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.

Average-case hardness of clique

Susanna de Rezende
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.

New developments in reverse mathematics

Damir Dzhafarov
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 - - contact 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.

On the strength of the Sherali-Adams proof system

Ilario Bonacina
UPC Barcelona
Monday, 25. October 2021 - 16:00 to 17:30

IM rear building, first floor *NOT BROADCAST*

This talk is about Sherali-Adams when considered as a propositional proof system. We will present some propositional proof systems equivalent to it and we will prove two results upper-bounding the strength of Sherali-Adams. More precisely, we will prove that (1) depth-2 Frege + PHP p-simulates Sherali-Adams with unary coefficients, and (2) depth-2 Frege +"wtPHP" p-simulates Sherali-Adams (with coefficients in binary). The "wtPHP" is a new combinatorial principle, some sort of "weighted" version of the pigeonhole principle.

This talk is based on a joint work with Maria Luisa Bonet.


  • 4