slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, normally 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.

Propositional branching program proofs and logics for L and NL

Sam Buss
University of California, San Diego
Monday, 14. December 2020 - 15:30 to 17:00
We introduce systems of propositional logic for reasoning directly with decision trees, non-deterministic decision trees, branching programs and non-deterministic branching programs. These propositional systems allow reasoning about properties in non-uniform logarithmic space and non-deterministic logarithmic space. We also report on work-in-progress to use these propositional proof systems for the bounded arithmetic theories VL and VNL with proof theoretic strength corresponding to logarithmic space and non-deterministic logarithmic space. The talk will start with an overview of the propositional proof systems which are already known to have close correspondences with bounded arithmetic. The new results are joint work with Anupam Das and Alexander Knop.

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