slideshow 3

Logic seminar

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*
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.