We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Our super-polynomial separation between resolution and cut-free sequent calculus only applies when clauses are seen as disjunctions of unbounded arity; our examples have linear size cut-free sequent calculus proofs writing, in a particular way, their clauses using binary disjunctions. Interestingly, this shows that the complexity of sequent calculus depends on how disjunctions are represented.
Logic seminar
usually takes place each Monday at 16:00 in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.
A super-polynomial separation between resolution and cut-free sequent calculus
Theodoros Papamakarios
University of Chicago
Monday, 4. October 2021 - 16:00 to 17:30
LEARN-Uniform Circuit Lower Bounds and Provability in Bounded Arithmetic
Marco Carmosino
Boston University
Monday, 14. June 2021 - 15:45 to 17:15
We investigate randomized LEARN-uniformity, which captures the power of randomness and equivalence queries (EQ) in the construction of Boolean circuits for an explicit problem. This is an intermediate notion between P-uniformity and non-uniformity motivated by connections to learning, complexity, and logic. Building on a number of techniques, we establish the first unconditional lower bounds against LEARN-uniform circuits. For example:
For each k >= 1, there is a language L in NP such that circuits for L of size O(n^k) cannot be learned in deterministic polynomial time with access to n^o(1) EQs.
We employ such results to investigate the (un)provability of non-uniform circuit upper bounds (e.g., Is NP contained in SIZE[n^3]?) in theories of bounded arithmetic. Some questions of this form have been addressed in recent papers of Krajicek-Oliveira (2017), Muller-Bydzovsky (2020), and Bydzovsky-Krajicek-Oliveira (2020) via a mixture of techniques from proof theory, complexity... more
A Diagonalization-Based Approach to Proof Complexity
Iddo Tzameret
Imperial College London
Monday, 7. June 2021 - 15:45 to 17:15
We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.
We use the approach to give an explicit sequence of CNF formulas phi_n such that VNP \neq VP iff there are no polynomial-size IPS proofs for the formulas phi_n. This provides the first natural equivalence between proof complexity lower bounds and standard algebraic complexity lower bounds. Our proof of this fact uses the implication from IPS lower bounds to algebraic complexity lower bounds due to Grochow and Pitassi together with a diagonalization argument: the formulas phi_n themselves assert the non-existence of short IPS proofs for formulas encoding VNP \neq VP at a different input length. Our result also has meta-mathematical implications: it gives evidence for the difficulty of proving strong lower bounds for IPS within IPS.
For any... more
Introduction to homotopy type theory
Valery Isaev
JetBrains research
Monday, 24. May 2021 - 15:45 to 17:15
Homotopy type theory (HoTT) is a new field of mathematics that blends logic, homotopy theory, and the theory of programming languages. In this talk, I will describe all the components of HoTT including necessary type theoretic construction. I will compare this theory with more traditional set theories like ZFC and show how homotopy theoretic constructions such as spheres and homotopy groups are defined in HoTT. I will also show how to work with such a theory in a proof assistant by providing examples of discussed concepts. Finally, I will discuss one of the open problems in the field.