•  
    • Sam Buss
    • (University of California, San Diego)
    • Propositional branching program proofs and logics for L and NL
    • Abstract:
    • 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.
    • 14.12.20   15:30
    • Jeremy Avigad
    • (Carnegie Mellon University)
    • Interactive theorem proving for the working logician
    • Abstract:
    • 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.

    • 07.12.20   15:30
    • Susanna F. de Rezende
    • (IM CAS)
    • Automating tree-like resolution in time n^o(log n/ log log n) is ETH-hard
    • Abstract:
    • 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).
    • 30.11.20   15:30
    • Mikolas Janota
    • (CIIRC)
    • QBF Solving and Calculi, Overview
    • Abstract:
    • 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.
    • 23.11.20   15:30
    • Yaroslav Alekseev
    • (Chebyshev Laboratory, St Petersburg State University)
    • A lower bound for Polynomial Calculus with extension rule
    • Abstract:
    • 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.
    • 16.11.20   15:30
    • Emil Jeřábek
    • (IM CAS)
    • Iterated multiplication in VTC^0, Part 2
    • Abstract:
    • 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 egg"-type problems (the analysis heavily uses various iterated products and divisions, whose existence in VTC^0 a priori requires the very IMUL axiom we'd like to prove). In this talk, we will show that IMUL is, after all, provable in VTC^0. We will outline the main challenges and ways how to get around them. As a byproduct, we will obtain a well-behaved \Delta_0 definition of modular exponentiation in the theory I\Delta_0 + WPHP(\Delta_0).
    • 02.11.20   15:30
    • Emil Jeřábek
    • (IM CAS)
    • Iterated multiplication in VTC^0
    • Abstract:
    • 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 egg"-type problems (the analysis heavily uses various iterated products and divisions, whose existence in VTC^0 a priori requires the very IMUL axiom we'd like to prove). In this talk, we will show that IMUL is, after all, provable in VTC^0. We will outline the main challenges and ways how to get around them. As a byproduct, we will obtain a well-behaved \Delta_0 definition of modular exponentiation in the theory I\Delta_0 + WPHP(\Delta_0).
    • 26.10.20   15:30
    • Erfan Khaniki
    • (IM CAS)
    • Not all Kripke models of HA are locally PA
    • Abstract:
    • Let K be an arbitrary Kripke model of Heyting Arithmetic, HA. For every node k in K, we can view the classical structure of k, m_k, as a model of some classical theory of arithmetic. Let T be a classical theory in the language of arithmetic. We say K is locally T, iff for every k in K, m_k models T. A well-studied question in the model theory of HA is the following question: Is every Kripke model of HA locally PA? We answer this question negatively by constructing a Kripke model of HA which is not locally B\Sigma_1.
    • 12.10.20   16:00
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Globalisers
    • Abstract:
    • A globaliser of a c.e. first-order theory T is a c.e. theory U such that U is locally interpretable in T and any c.e. theory V locally interpretable in T is globally interpretable in U. From standard results about reflexive theories (e.g. PA, ZF, ZFC) it follows that any reflexive theory is its own globaliser. In recent years Albert Visser proved that Robinson's arithmetic R is its own globaliser. And that there is a globaliser for any sequential c.e. theory T.  In the present talk I would give two proofs of a new result that for any c.e. theory T there is a globaliser. The talk is based on two papers in preparation. One is joint with Albert Visser and the other is joint with Yong Cheng.
    • 13.07.20   13:30
    • Michal Garlík
    • (Polytechnic University of Catalonia)
    • Feasible disjunction property and k-DNF resolution
    • Abstract:
    • We discuss feasible disjunction property and reflection principles for propositional proof systems. For every integer $k \geq 2$, we show that $k$-DNF resolution does not have the feasible disjunction property. This contrasts with the case $k = 1$ (the usual resolution). Time permitting, we look at some consequences.
    • 29.06.20   15:15
    • Ján Pich
    • (University of Oxford)
    • Consistency of Nondeterministic Circuit Upper Bounds
    • Abstract:
    • We show unconditionally that Jeřábek's theory of approximate counting APC_1 formalizing probabilistic poly-time reasoning cannot prove, for any non-deterministic poly-time machine M, that M is inapproximable by co-nondeterministic circuits of sub-exponential size. We also show several related results concerning worst-case and zero-error average case lower bounds for various versions of the Minimum Circuit Size Problem against co-nondeterministic circuits.   This is joint work with Rahul Santhanam.
    • 15.06.20   13:30
    • Leszek Kolodziejczyk
    • (University of Warsaw)
    • The logical strength of Büchi's decidability theorem
    • Abstract:
    • 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's theorem also turn out to be either equivalent to, or provable from, Sigma^0_2 induction.
    • 25.05.20   13:30
    • Susana F. de Rezende
    • (IM CAS)
    • Automating Algebraic Proof Systems is NP-Hard
    • Abstract:
    • 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.
    • 11.05.20   13:30
    • Iddo Tzameret
    • (Royal Holloway, University of London)
    • Semi-Algebraic Proofs, IPS lower bounds and the tau-Conjecture
    • Abstract:
    • 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, for sufficiently strong systems.

      Joint work with Yaroslav Alekseev, Dima Grigoriev and Edward A. Hirsch. See full version here: https://eccc.weizmann.ac.il/report/2019/142/download

    • 04.05.20   13:30
    • Pavel Pudlák
    • (IM CAS)
    • Reflection principles in the propositional calculus, Part 2
    • Abstract:
    • 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.
    • 27.04.20   13:30
    • Azza Gaysin
    • (Charles University)
    • H-Coloring Dichotomy in Proof Complexity
    • Abstract:
    • The H-Coloring problem can be considered as an example of the computational problem from a huge class of constraint satisfaction problems (CSP): an H-Coloring of a graph G is just a homomorphism from G to H. The dichotomy theorem for H-Coloring was proved by Hell and Nešetřil (an analogous theorem for all CSPs was recently proved by Zhuk and Bulatov) and it says that for each H the problem is either p-time decidable or NP-complete. Since negations of unsatisfiable instances of CSP can be expressed as propositional tautologies, it seems to be natural to investigate the proof complexity of CSP. We show that the decision algorithm in the p-time case of the H-Coloring can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have short proofs in propositional proof system R^*(log). We complement this upper bound result by a lower bound result for the special example of NP-complete case of the H-Coloring, using the known results about proof complexity of the Pigeonhole Principle
    • 20.04.20   13:30
    • Pavel Pudlák
    • (IM CAS)
    • Reflection principles in the propositional calculus.
    • Abstract:
    • 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. ** Location: https://us02web.zoom.us/j/472648284 **
    • 14.04.20   13:30
    • Erfan Khaniki
    • (Institute of Mathematics)
    • On the proof complexity of Resolution over Polynomial Calculus
    • Abstract:
    • The refutation system Res_R(PC_d) is a natural extension of the Resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called Res_R(lin). One of the important open problems in Proof Complexity is proving lower bounds for Res_R(lin) when R is a finite field such as F_2. Interestingly, Res_{F_2}(lin) is fairly strong, and there is no known nontrivial lower bound for it, but for Res^*_R(lin) (tree-like Res_R(lin)) we know exponential lower bounds for every finite field. For the stronger systems Res_R(PC_d) and Res_R^*(PC_d) for d>1 on finite ring R, there is no known lower bounds. In this talk, we prove a size-width relation for Res_R(PC_d) and Res^*_R(PC_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for Res and Res^* using extension variables. As a by product, we get the following new lower bounds for every finite field F: 1. We prove a nontrivial lower bound for Res_F(PC_d) for fixed d: a nearly quadratic lower bound for mod q Tseitin formulas (char(F) is not equal to q). 2. We also prove superpolynomial and exponential lower bounds for Res^*_F(PC_d) where d is not too large with respect to n for the following principles: a. mod q Tseitin formulas (char(F) is not equal to q), b. Random k-CNFs.
    • 30.03.20   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Proof-theoretic analysis of some impredicative theories, Part 2
    • Abstract:
    • In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.
    • 23.03.20   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Proof-theoretic analysis of some impredicative theories
    • Abstract:
    • In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.
    • 09.03.20   13:30
    • Susanna F. de Rezende
    • (Institute of Mathematics)
    • Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs, Part 2
    • Abstract:
    • In this talk, we will present Razborov's pseudo-width method and explain how it can be extended to obtain exponential resolution lower bounds for the weak pigeonhole principle (PHP) and perfect matching formulas over highly unbalanced, sparse expander graphs. Our result establishes strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking other longstanding open problems for resolution and other proof systems. This is joint work with Jakob Nordström, Kilian Risse and Dmitry Sokolov.
    • 02.03.20   13:30
    • Susanna F. de Rezende
    • (Institute of Mathematics)
    • Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
    • Abstract:
    • In this talk, we will present Razborov's pseudo-width method and explain how it can be extended to obtain exponential resolution lower bounds for the weak pigeonhole principle (PHP) and perfect matching formulas over highly unbalanced, sparse expander graphs. Our result establishes strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking other longstanding open problems for resolution and other proof systems. This is joint work with Jakob Nordström, Kilian Risse and Dmitry Sokolov.
    • 24.02.20   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Proof complexity of logics of bounded branching, Part 2
    • Abstract:
    • We revisit the problem of Frege and extended Frege (EF) lower bounds for transitive modal logics. Hrubes proved an exponential lower bound on the number of lines in Frege proofs, or equivalently, on the size of EF proofs, for some basic modal logics such as K, K4, S4, and GL. This was extended by Jerabek to an exponential separation between EF and substitution Frege (SF) systems for all transitive logics of unbounded branching.

      On the other hand, for typical logics of bounded width, the EF and SF systems are p-equivalent, and they are in a certain sense p-equivalent to the classical EF system, for which we do not know any lower bounds, and even candidate hard tautologies are scarce.

      The main ingredients in all the lower bounds above (as well as similar bounds for superintuitionistic logics) were variants of the feasible disjunction property (DP), playing a role similar to feasible interpolation in classical proof systems.

      This raises the question what happens for logics with bounded branching but unbounded width, such as K4BB_k, S4BB_k, and GLBB_k. In this talk, I will show that while these logics apparently do not have feasible DP as such, they have DP (and more general extension rules) decidable in ZPP^{NP}, and for k=2, even in promise-S_2^P. Moreover, one can also adapt Hrubes's form of "monotone interpolation" to this setting.

      As a consequence, we prove superpolynomial speedup of SF over EF assuming PSPACE \ne NP (possibly exponential under a stronger hypothesis) for all modal logics included in GLBB_2 or S4GrzBB_2, and more generally, for all logics L that, in a certain sense, admit all finite binary trees (with reflexive or irreflexive points as convenient) to appear inside L-frames.

       

    • 03.02.20   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Proof complexity of logics of bounded branching
    • Abstract:
    • We revisit the problem of Frege and extended Frege (EF) lower bounds for transitive modal logics. Hrubes proved an exponential lower bound on the number of lines in Frege proofs, or equivalently, on the size of EF proofs, for some basic modal logics such as K, K4, S4, and GL. This was extended by Jerabek to an exponential separation between EF and substitution Frege (SF) systems for all transitive logics of unbounded branching.

      On the other hand, for typical logics of bounded width, the EF and SF systems are p-equivalent, and they are in a certain sense p-equivalent to the classical EF system, for which we do not know any lower bounds, and even candidate hard tautologies are scarce.

      The main ingredients in all the lower bounds above (as well as similar bounds for superintuitionistic logics) were variants of the feasible disjunction property (DP), playing a role similar to feasible interpolation in classical proof systems.

      This raises the question what happens for logics with bounded branching but unbounded width, such as K4BB_k, S4BB_k, and GLBB_k. In this talk, I will show that while these logics apparently do not have feasible DP as such, they have DP (and more general extension rules) decidable in ZPP^{NP}, and for k=2, even in promise-S_2^P. Moreover, one can also adapt Hrubes's form of "monotone interpolation" to this setting.

      As a consequence, we prove superpolynomial speedup of SF over EF assuming PSPACE \ne NP (possibly exponential under a stronger hypothesis) for all modal logics included in GLBB_2 or S4GrzBB_2, and more generally, for all logics L that, in a certain sense, admit all finite binary trees (with reflexive or irreflexive points as convenient) to appear inside L-frames.

       

    • 27.01.20   13:30

    Pavel Pudlak, Neil Thapen, Jan Krajíček
    organizers

  •