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.

Interactive theorem proving for the working logician
Jeremy Avigad
Carnegie Mellon University
Monday, 7. December 2020 - 15:30 to 17:00
Over the last few decades, computational proof assistants have made it possible to construct formal axiomatic derivations of increasing complexity. They are now used to verify that hardware and software designs meet their specifications, as well as to verify the correctness of mathematical proofs. The practice has taken root and promises to play an important role in mathematics and computer science.

In this talk, I will survey the technology, with an emphasis on formal mathematics. I will then discuss aspects of interactive theorem proving that may be of interest to the working logician, and places where a better theoretical understanding can lead to progress. Specifically, I'll discuss the need for practical foundations, search procedures, decision procedures, and proof systems.

Automating tree-like resolution in time n^o(log n/ log log n) is ETH-hard
Susanna F. de Rezende
IM CAS
Monday, 30. November 2020 - 15:30 to 17:00
It is known that tree-like resolution is automatable in time n^O(log n). In this talk we will show that under ETH tree-like resolution is not automatable in time n^o(log n/ log log n). We will also provide an alternative, arguably simpler proof of the result of Alekhnovich and Razborov (SIAM J. Comput. 2008) that unless the fixed parameter hierarchy collapses, tree-like resolution is not automatable in polynomial time. The proof builds on a joint work with Mika Göös, Jakob Nordström, Toni Pitassi, Robert Robere and Dmitry Sokolov (ECCC 2020), which presents a simplification of the breakthrough result of Atserias and Müller (JACM 2020).

QBF Solving and Calculi, Overview
Mikolas Janota
CIIRC
Monday, 23. November 2020 - 15:30 to 17:00
Quantified Boolean Formulas (QBFs) enrich the SAT problem with quantifiers taking the problem from NP to PSPACE. Recent years have seen a number of novel approaches to QBF solving. At the same time, QBF calculi were developed to match the solvers. However, there are calculi with no solving counterparts.

In this talk I will overview the two prominent paradigms in QBF solving: conflict-driven and expansion-based. I will also discuss the connection between solving and the existing proof systems as well as challenges for future research.

A lower bound for Polynomial Calculus with extension rule
Yaroslav Alekseev
Chebyshev Laboratory, St Petersburg State University
Monday, 16. November 2020 - 15:30 to 17:00
In this talk we consider an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations of exponential bit size over rationals in this system. Part and Tzameret proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of the binary value principle. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of the binary value principle.

Pages