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.

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.

Iterated multiplication in VTC^0, Part 2

Emil Jeřábek
IM CAS
Monday, 2. November 2020 - 15:30 to 17:00
Basic arithmetic operations +, -, *, / belong to the complexity class TC^0, and it is a natural question what can be proved about them in the corresponding theory of arithmetic VTC^0. It has been known that the theory VTC^0 + IMUL including an axiom expressing the totality of iterated multiplication \prod_{i=0}^n X_i proves quite a lot: it can formalize root finding for constant-degree polynomials, and as a consequence, it proves the RSUV-translation of IOpen, and more generally, of induction and minimization for sharply bounded formulas in Buss's language.

This left open the problem whether IMUL is itself provable in VTC^0, which effectively calls for the formalization of the TC^0 iterated multiplication algorithm due to Hesse, Allender, and Barrington.

Even though the analysis of the HAB algorithm is in principle fairly elementary, it has some peculiar features that make its formalization quite challenging: in particular, it suffers from serious "chicken or... more

Iterated multiplication in VTC^0

Emil Jeřábek
IM CAS
Monday, 26. October 2020 - 15:30 to 17:00
Basic arithmetic operations +, -, *, / belong to the complexity class TC^0, and it is a natural question what can be proved about them in the corresponding theory of arithmetic VTC^0. It has been known that the theory VTC^0 + IMUL including an axiom expressing the totality of iterated multiplication \prod_{i=0}^n X_i proves quite a lot: it can formalize root finding for constant-degree polynomials, and as a consequence, it proves the RSUV-translation of IOpen, and more generally, of induction and minimization for sharply bounded formulas in Buss's language.

This left open the problem whether IMUL is itself provable in VTC^0, which effectively calls for the formalization of the TC^0 iterated multiplication algorithm due to Hesse, Allender, and Barrington.

Even though the analysis of the HAB algorithm is in principle fairly elementary, it has some peculiar features that make its formalization quite challenging: in particular, it suffers from serious "chicken or... more

Pages