•  
    • Dmitry Sokolov
    • (EPFL)
    • Top-down depth-4 circuit lower bounds
    • Abstract:
    • In this talk, we present a top-down lower-bound method for depth-4 boolean circuits. In particular, we give a new proof of the well-known result that the parity function requires depth-4 circuits of size exponential in n^{1/3}. Our proof is an application of robust sunflowers and block unpredictability. Joint work with Mika Göös, Artur Riazanov and Anastasia Sofronova
    • 05.06.23   16:00
    • Leonardo Coregliano
    • (IAS Princeton)
    • Continuous combinatorics
    • Abstract:
    • The field of continuous combinatorics is the study of (large, dense) combinatorial structures using tools typically associated with continuous objects, such as tools from analysis, topology or measure theory. The field started under the name of "graph limits" since the main object of study were graphons, i.e., limits of graphs. Since then, several other limits have been constructed for all sorts of combinatorial objects (e.g., digraphs, hypergraphs, permutations, etc.) and even general limits were provided through the unifying theory of flag algebras.

      However, the limits constructed in the theory of flag algebras are of an algebraic/syntactic nature, due to the minimalist nature of the theory (as opposed to the more semantic/geometric nature of the previous ad hoc limits of the literature). In this talk, I will present the semantic/geometric counterpart to flag algebras: the theory of theons. I will also give a couple of examples of proofs both within continuous combinatorics and of applications that use its tools.

      This talk is based on joint work with Alexander A. Razborov.

    • 22.05.23   16:00
    • Emil Jeřábek
    • (IM CAS)
    • A simplified lower bound on intuitionistic implicational proofs
    • Abstract:
    • Unlike classical Frege systems, we know exponential lower bounds for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubes (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that disjunction is essential for these lower bounds, but Jerabek (2017) adapted them to the implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon-Boppana).

      I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene's slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege.

      I will also mention a tangentially related problem about classical Frege systems.

      One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also exponential lower bounds on constant-depth Frege), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon-Boppana circuit lower bound.

       

    • 15.05.23   16:00
    • Amirhossein Akbar Tabatabai
    • (University of Groningen)
    • Unearthing the Feasible World: A Proposal
    • Abstract:
    • The decades-long practice of complexity theory and bounded arithmetic provided some strong clues for the existence of an alternative yet rich feasible world, where for instance all the functions are feasible and the polynomially and exponentially bounded sets are the new finite and infinite, respectively. The situation is similar to the so-called computable and continuous worlds whose traces first unearthed in constructive mathematics and later realized by the forcing-style model constructions that elevated to a general and conceptual theory called the topos theory. In this talk, imitating the main ideas of topos theory, we propose a program to provide a general machinery for the feasible forcing in order to prove some independence results for weak arithmetic, on the one hand and find a conceptual understanding of the low complexity computation, on the other. As we will see, any fulfillment of that proposal needs a certain (geometric) form of structural theory and one canonical base model. We will report some of our partial results to find these two ingredients. For the first, we will present our structural theory for the low complexity versions of the inductive objects like the natural numbers, binary strings, ordinals and sets. For the latter, we will explain our imitation of Hyland's construction of the computable world (effective topos) for the feasible functions and the problematic role of the intuitionistic implication there that leads to our general theory of implication and its inherent non-geometricity. Despite what it appears at the first glance, we will not assume any familiarity with category theory and topos theory and the talk will be rather informal in this respect.
    • 10.05.23   16:00
    • Pavel Pudlák
    • (IM CAS)
    • Some remarks on Herbrand's Theorem
    • Abstract:
    • In [3] I proved Proposition 4.3 about the impossibility of certain forms of the formulas in Herbrand's Theorem. This is seemingly in contradiction with Theorem 6 of Buss, Kolodzieczyk and Thapen [1], and a more recent Theorem 3.2 of Li and Oliveira of [2]. Nevertheless, all theorems hold true. In the lecture I will explain the differences and prove my Proposition with an explicit formula, which is not in [3].

      [1] Buss, Kolodzieczyk and Thapen: Fragments of approximate counting, JSL 79. [2] Li, Igor Carboni Oliveira: Unprovability of strong complexity lower bounds in bounded arithmetic. ECCC~TR23-022. [3] P. Pudlak: Consistency and games - in search of new combinatorial principles. Proc. Logic Colloquium'03.

    • 24.04.23   16:00
    • Ilario Bonacina
    • (Universitat Politčcnica de Catalunya )
    • Polynomial Calculus for MaxSAT
    • Abstract:
    • MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem.

      Weighted Polynomial Calculus is a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in N or Z. We show the soundness and completeness of these systems via an algorithmic procedure.

      Weighted Polynomial Calculus, with weights in N and coefficients in F_2, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in Z, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

       

    • 17.04.23   16:00

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

  •