•  
    • Ján Pich
    • (University of Oxford)
    • Towards P != NP from Extended Frege lower bounds
    • Abstract:
    • We prove that if conditions I-II (below) hold and there is a sequence of Boolean functions $f_n$ hard to approximate by p-size circuits such that p-size circuit lower bounds for $f_n$ do not have p-size proofs in Extended Frege system EF, then $P \ne NP$.

      I. $S^1_2$ proves that there is a function $g\in E$ hard to approximate by subexponential-size circuits.

      II. (Learning from the non-existence of OWFs.) $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits learning p-size circuits over the uniform distribution, with membership queries.

      Here, $S^1_2$ is Buss's theory of bounded arithmetic formalizing p-time reasoning.

      Further, we show that any of the following assumptions implies that $P \ne NP$, if EF is not p-bounded:

      1. (Feasible anticheckers.) $S^1_2$ proves that a p-time function generates anticheckers for SAT.

      2. (Witnessing $NP\not\subseteq P/poly$.) $S^1_2$ proves that a p-time function witnesses an error of each p-size circuit which fails to solve SAT.

      3. (OWFs from $NP\not\subseteq P/poly$ & hardness of E.) Condition I holds and $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits computing SAT.

      The results generalize to stronger theories and proof systems.

      This is joint work with Rahul Santhanam.

       

    • 12.12.22   16:00
    • Moritz Müller
    • (University of Passau)
    • On the parameterized complexity of Delta-0 truth
    • Abstract:
    • We consider the problem, given a ?0 formula ?(x) and a natural number n in unary, whether ?(n) is true. We are interested in instances of the problem where n is much bigger than ?. More precisely, we consider the parameterized problem with parameter |?|. We show unconditionally that this problem does not belong to the parameterized version of AC0. We also show that certain natural upper bounds on the parameterized complexity of the problem imply separations of classical complexity classes. These results are obtained by an analysis of a parameterized halting problem. A related problem concerns the provability of the MRDP theorem in bounded arithmetic.
    • 21.11.22   16:00
    • Martin Suda
    • (CVUT)
    • Integrating Machine Learning into Saturation-based ATPs
    • Abstract:
    • Applying the techniques of machine learning (ML) promises to dramatically improve the performance of modern automatic theorem provers (ATPs) and thus to positively impact their applications. The most successful avenue in this direction explored so far is machine-learned clause selection guidance, where we learn to recognize and prefer for selection clauses that look like those that contributed to a proof in past successful runs. In this talk I present Deepire, an extension of the ATP Vampire where clause selection is guided by a recursive neural network (RvNN) for classifying clauses based solely on their derivation history.
    • 14.11.22   16:00
    • Emil Jeřábek
    • (IM CAS)
    • Elementary analytic functions in VTC^0, Part 2
    • Abstract:
    • It is known that rational approximations of elementary analytic functions (exp, log, trigonometric and hyperbolic functions, and their inverse functions) are computable in the complexity class TC^0. In this talk, we will show how to formalize their construction and basic properties in the correspoding arithmetical theory VTC^0, working with completions of fraction fields of models of VTC^0. As a consequence, we will show that every countable model of VTC^0 is an exponential integer part of a real-closed exponential field, using a recursive saturation argument.
    • 24.10.22   16:00
    • Emil Jeřábek
    • (IM CAS)
    • Elementary analytic functions in VTC^0
    • Abstract:
    • It is known that rational approximations of elementary analytic functions (exp, log, trigonometric and hyperbolic functions, and their inverse functions) are computable in the complexity class TC^0. In this talk, we will show how to formalize their construction and basic properties in the correspoding arithmetical theory VTC^0, working with completions of fraction fields of models of VTC^0. As a consequence, we will show that every countable model of VTC^0 is an exponential integer part of a real-closed exponential field, using a recursive saturation argument.
    • 17.10.22   16:00
    • Chris Lambie-Hanson
    • (IM CAS)
    • Compactness and incompactness in set theory, with applications to uncountable graphs
    • Abstract:
    • (Joint seminar with set theory group) The study of compactness phenomena at uncountable cardinals has been a central line of research in combinatorial set theory since the mid-twentieth century. In the first part of this talk, we will give a broad overview of this area of research and survey some of its most prominent results. We will then look at a few recent results concerning compactness phenomena for uncountable graphs. We first look at possible generalizations of the de Bruijn-Erdos compactness theorem for chromatic numbers to uncountable cardinalities, in particular showing that consistently there are large uncountable graphs witnessing extreme failures of compactness for, e.g., the property of having a countable chromatic number. We then turn to the study of the structure of the collections of finite subgraphs of uncountably chromatic graphs, answering a question of Erdos, Hajnal, and Szemeredi about the growth rates of chromatic numbers in such collections of finite subgraphs.
    • 26.09.22   16:00
    • Rahul Santhanam
    • (University of Oxford)
    • On the Conjectures of Razborov and Rudich
    • Abstract:
    • We say that Rudich's Conjecture holds for a propositional proof system Q if there are no efficient Q-proofs of random truth table tautologies. We say that Razborov's Conjecture holds for a propositional proof system Q if there are no efficient Q-proofs of any truth table tautologies. A fundamental task in proof complexity and the meta-mathematics of circuit lower bounds is to understand for which Q these conjectures hold. We show various results about these conjectures, including evidence for their difficulty.

      Based on joint work with Jan Pich.

    • 23.05.22   16:00
    • Leszek Kołodziejczyk
    • (University of Warsaw)
    • In search of the first-order part of Ramsey's theorem for pairs
    • Abstract:
    • Reverse mathematics studies the logical strength of mathematical theorems formalized as statements in the language of second-order arithmetic (which is a two-sorted language with one sort of variables for natural numbers and another for sets of natural numbers). The strength is usually measured in terms of implications between the theorems and some set existence axioms, but it also makes sense to ask about the first-order consequences of a theorem, that is, what statements about natural numbers it implies.

      In recent decades, a particularly interesting case study has been provided by RT^2_2: Ramsey's theorem for pairs and two colours. RT^2_2 and its variants are anomalous in the sense of not being equivalent to any of the typical set existence axioms considered in reverse mathematics, or to each other. Characterizing the first-order part of RT^2_2 is a long-standing and highly interesting open problem. Methods used to make progress on this problem have typically been based on some combination of recursion theory and nonstandard models of arithmetic, with the latter playing an increasingly important role.

      I will briefly discuss some major results on the first-order part of RT^2_2 obtained over the years and then talk about some more recent work related to the problem that I have been involved in (jointly with Marta Fiori Carones, Kasia Kowalik, Keita Yokoyama and Tin Lok Wong).

    • 16.05.22   16:00
    • Yoriyuki Yamagata
    • (AIST)
    • On proving consistency of equational theories in Bounded Arithmetic
    • Abstract:
    • We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.
    • 09.05.22   11:00
    • Pavel Pudlák
    • (IM CAS)
    • From Peano Arithmetic to propositional calculus and back
    • Abstract:
    • In the first half of my talk I will mention the history of our logic group in our institute and how we gradually moved from studying metamathematics of Peano Arithmetic to weak fragments, and eventually to proof complexity of propositional logic. In the second part I will talk about my project to define a hierarchy of propositional proof systems indexed by ordinals up to epsilon_0 with the aim to prove that they characterize the proof system associated with Peano Arithmetic.
    • 02.05.22   16:00
    • Leroy Chew
    • (TU Wien)
    • Simulations in QBF Proof Complexity
    • Abstract:
    • Quantified Boolean Formulas (QBF) extend propositional formulas with Boolean quantifiers. Solving a QBF is PSPACE complete, and QBFSAT is seen as a natural extension of the SAT problem. Just as propositional proof complexity underlies the theory behind SAT solving, QBF proof complexity underlies the theory behind QBF solving. Here we will focus on the relative strengths of QBF proof systems via p-simulation.

      On the surface QBF proof systems seem harder to compare to one another since they vary considerably in how they deal with quantification. In particular there's a vast difference between theory systems that generalise from propositional logic, the proof systems that capture the process of CDCL solving and the proof systems that capture the expansion and CEGAR based solvers. And many results do formally show an incomparability in the proof complexity between different systems as we suspect. However, there are a few non-obvious cases where a simulation is possible. In this talk we will examine the landscape of simulation in QBF, looking at the results over the last decade, as well as our own recent work with simulations based on strategy extraction and propositionalisation. We will interpret the theoretical and practical importance of these results.

    • 25.04.22   16:00
    • Azza Gaysin
    • (Charles University)
    • Proof complexity of CSP on algebras with linear congruence, Part 2
    • Abstract:
    • CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It says that for each fixed target structure, CSP is either NP-complete or p-time. Zhuk's algorithm for the p-time case of the problem eventually leads to algebras with linear congruence.

      We show that Zhuk's algorithm for algebras with linear congruence can be formalized in the theory V^1. Thus, using known methods of proof complexity, Zhuk's algorithm for negative instances of the problem can be augmented by extra information: it not only rejects X that cannot be homomorphically mapped into A but produces a certificate - a short extended Frege (EF) propositional proof - that this rejection is correct.

    • 11.04.22   16:00
    • Azza Gaysin
    • (Charles University)
    • Proof complexity of CSP on algebras with linear congruence
    • Abstract:
    • CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It says that for each fixed target structure, CSP is either NP-complete or p-time. Zhuk's algorithm for the p-time case of the problem eventually leads to algebras with linear congruence.

      We show that Zhuk's algorithm for algebras with linear congruence can be formalized in the theory V^1. Thus, using known methods of proof complexity, Zhuk's algorithm for negative instances of the problem can be augmented by extra information: it not only rejects X that cannot be homomorphically mapped into A but produces a certificate - a short extended Frege (EF) propositional proof - that this rejection is correct.

    • 04.04.22   16:00
    • David Fernández-Duque
    • (Ghent University and Czech Academy of Sciences)
    • A Walk with Goodstein
    • Abstract:
    • The classical Goodstein process is based on writing numbers in "normal form" in terms of addition and exponentiation with some base k. By iteratively changing base and subtracting one, one obtains very long sequences of natural numbers which eventually terminate. The latter is proven by comparing base-k normal forms with Cantor normal forms for ordinals, and in fact this proof relies heavily on the notion of normal form. The question then naturally arises: what if we write natural numbers in an arbitrary fashion, not necessarily using normal forms? What if we allow not only addition and exponentiation, but also multiplication for writing numbers?

      A "Goodstein walk" is any sequence obtained by following the standard Goodstein process but arbitrarily choosing how each element of the sequence is represented. As it turns out, any Goodstein walk is finite, and indeed the longest possible Goodstein walk is given by the standard normal forms. In this talk we sketch a proof of this fact and discuss how a similar idea can be applied to other variants of the Goodstein process, including those based on the Ackermann function.

      Joint work with A. Weiermann

    • 21.03.22   16:00
    • Erfan Khaniki
    • (Institute of Mathematics)
    • Nisan-Wigderson generators in Proof Complexity: New lower bounds
    • Abstract:
    • A map g:{0,1}^n --> {0,1}^m (m>n) is a hard proof complexity generator for a proof system P iff for every string b in {0,1}^m\Rng(g) the formula \tau_b(g), naturally expressing b \not \in Rng(g), requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is the Nisan-Wigderson generator. Razborov (Annals of Mathematics 2015) conjectured that if A is a suitable matrix and f is a NP \cap CoNP function hard-on-average for P/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege. In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.
    • 14.03.22   16:00
    • Robert Robere
    • (McGill University)
    • On Semi-Algebraic Proofs and Algorithms
    • Abstract:
    • We discuss a new characterization of the Sherali-Adams proof system, a standard propositional proof system considered in both proof complexity and combinatorial optimization, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula F if and only if there is an ? > 0 and a degree-d conical junta J such that viol(x) ? ? = J, where viol(x) counts the number of falsified clauses of F on an input x. This result implies that the linear separation complexity, a complexity measure recently studied by Hrubes (and independently by de Oliveira Oliveira and Pudlak under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs, sharpening a feasible interpolation result of Hakoniemi. On the lower-bound side, we prove a separation between the conical junta degree of viol(x) - 1 and Resolution width; since Sherali-Adams can simulate Resolution this also separates the conical junta degree of viol(x) - 1 and viol(x) - ? for arbitrarily small ? > 0. Finally, by applying known lifting theorems, we can translate this separation into separations between extension complexity and monotone circuit complexity.

      This talk is based on joint work with Noah Fleming, Mika Goos, and Stefan Grosser.

    • 07.03.22   16:00
    • Dmitry Sokolov
    • (St Petersburg State University and PDMI RAS)
    • Resolution, Heavy Width and Pseudorandom Generators
    • Abstract:
    • Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson we call a pseudorandom generator hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement that b is outside of the image for any string b \in {0, 1}^m.

      In ABRW04 the authors suggested the "functional encoding" of the considered statement for Nisan--Wigderson generator that allows the introduction of "local" extension variables and gave a lower bound on the length of Resolution proofs if the number of extension variables is bounded by the n^2 (where n is the number of inputs of the PRG).

      In this talk, we discuss a "heavy width" measure for Resolution that allows us to show a lower bound on the length of Resolution proofs of the considered statement for the Nisan--Wigderson generator with a superpolynomial number of local extension variables. It is a solution to one of the open problems from ABRW04.

    • 21.02.22   16:00
    • Michal Garlik
    • (St. Petersburg Department of Steklov Institute of Mathematics and Euler International Mathematical Institute)
    • A revision of the width method
    • Abstract:
    • We consider a framework for proving lower bounds on the length of proofs in logical calculi that can be seen as a generalization of the game framework in which Pudlák presented Haken's lower bound for resolution. Our framework, while still requiring some notion of width, can be applied in a way that avoids the use of the random restriction technique. As an example, we demonstrate this for resolution, obtaining a proof in which the calculations are very simple.
    • 10.01.22   16:00

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

  •