slideshow 3

Logic seminar

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

The logical strength of Büchi's decidability theorem

Leszek Kolodziejczyk
University of Warsaw
Monday, 25. May 2020 - 13:30 to 15:00
I will talk about a result obtained a few years ago jointly with Henryk Michalewski, Pierre Pradic and Michał Skrzypczak. Our aim was to describe the strength of axioms needed to prove Büchi's theorem, which says that the monadic second order theory of the natural number order is decidable.

The axiomatic requirements of theorems involving second-order quantification over the naturals, like Büchi's theorem, are commonly studied within a research programme known as reverse mathematics, and often characterized in terms of an equivalence between the theorem and some fragment of so-called second order arithmetic. I plan to give a (brief) introduction to second order arithmetic and to monadic second order logic. Then I will discuss our main result, which says that Büchi's theorem (suitably formulated) is, over the usual base theory considered in reverse mathematics, equivalent to the induction scheme for Sigma^0_2 formulas. Various automata-theoretic statements related to Büchi... more

Automating Algebraic Proof Systems is NP-Hard

Susana F. de Rezende
IM CAS
Monday, 11. May 2020 - 13:30 to 15:00
Recently, Atserias and Müller (FOCS 2019) established that it is NP-hard to find a resolution refutation of an unsatisfiable formula in time polynomial in the size of the shortest such refutation. In this talk, I will present a simplified proof of this result and explain how it can be extended to hold also for Nullstellensatz, Polynomial Calculus, and Sherali–Adams. This is based on joint work with Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere and Dmitry Sokolov.

Semi-Algebraic Proofs, IPS lower bounds and the tau-Conjecture

Iddo Tzameret
Royal Holloway, University of London
Monday, 4. May 2020 - 13:30 to 15:00
We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2014). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes, Shpilka, Tzameret and Wigderson (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning,... more

Reflection principles in the propositional calculus, Part 2

Pavel Pudlák
IM CAS
Monday, 27. April 2020 - 13:30 to 15:00
I will survey some results on the reflection principles for propositional proof systems, show a connection to the recent result on non-automatibility of Resolution and ask several problems.

Pages