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.

Top-down depth-4 circuit lower bounds

Dmitry Sokolov
EPFL
Monday, 5. June 2023 - 16:00 to 17:30
Large lecture room at Zitna and online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join online
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

Continuous combinatorics

Leonardo Coregliano
IAS Princeton
Monday, 22. May 2023 - 16:00 to 17:30
Online - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join
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... more

A simplified lower bound on intuitionistic implicational proofs

Emil Jeřábek
IM CAS
Monday, 15. May 2023 - 16:00 to 17:30
Large lecture room at Zitna and online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join online
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-... more

Unearthing the Feasible World: A Proposal

Amirhossein Akbar Tabatabai
University of Groningen
Wednesday, 10. May 2023 - 16:00 to 17:30
Konirna seminar room at Zitna and online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join online
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... more

Some remarks on Herbrand's Theorem

Pavel Pudlák
IM CAS
Monday, 24. April 2023 - 16:00 to 17:30
Large lecture room at Zitna and online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join online
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.

Polynomial Calculus for MaxSAT

Ilario Bonacina
Universitat Politècnica de Catalunya
Monday, 17. April 2023 - 16:00 to 17:30
Large lecture room at Zitna and online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join online
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.

 

Pages

  • 1