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.
Logic seminar
usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, normally in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.
A revision of the width method
Michal Garlik
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*
Arithmetic under negated induction
Tin Lok Wong
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).
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 - 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
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 - 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.