•  
    • Fedor Part
    • (Royal Holloway, University of London)
    • Lower Bounds for Resolution with Linear Equations over a Ring
    • Abstract:
    • The proof system Res(lin_R) is an extension of Resolution in which proof lines are disjunctions of linear equations over a ring R. If R is a finite field GF(p), Res(lin_R) can be viewed as a "minimal" fragment of bounded depth Frege system with counting gates AC^0[p]-Frege (and similarly, for R the integers and the TC^0-Frege), for which no nontrivial lower bound is known. Recent suggested approaches for obtaining lower bounds against Res(lin_GF(2)) refutations include feasible interpolation and combinatorial techniques. In this talk we explore and develop further the combinatorial approach for various rings R. In particular, we prove an exponential-size dag-like Res(lin_F) lower bound for the Subset Sum principle with large coefficients, as well as establish a host of new tree-like lower bounds and separations over different fields. Based on a joint work with Iddo Tzameret.
    • 17.12.18   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • DRAT proofs without new variables
    • Abstract:
    • The DRAT proof system is used by modern SAT solvers to witness that a CNF is unsatisfiable. The full system allows you to freely introduce new variables, and is as strong as extended resolution. I will discuss some upper and lower bounds on a restricted system, in which you cannot introduce new variables. This is ongoing work with Sam Buss.
    • 10.12.18   14:00
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • Semi-analytic rules and uniform interpolation
    • Abstract:
    • In her recent works, Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform interpolation property of the super-intuitionistic logic that the calculus captures. In this talk, we will generalize this relationship to also cover the substructural setting on the one hand and a much more powerful class of rules on the other. The resulted relationship then provides a uniform method to establish uniform interpolation property for the logics FL_e, FL_{ew}, CFL_e, CFL_{ew}, IPC, CPC and their K and KD-type modal extensions. More interestingly though, on the negative side, we will show that no extension of FL_e can enjoy a certain natural type of terminating sequent calculus unless it has the uniform interpolation property. It excludes almost all super-intutionistic logics and the logics K4 and S4 from having such a reasonable calculus.
    • 19.11.18   14:00
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • Semi-analytic Rules and Craig Interpolation
    • Abstract:
    • In one of her recent works, Iemhoff introduced the notion of a centered axiom and a centered rule as the building blocks for a certain form of sequent calculus which she calls a centered proof system. She then showed how the existence of a terminating centered system implies the uniform interpolation property for the logic that the calculus captures. In this paper we first generalize her centered rules to semi-analytic rules, a dramatically powerful generalization, and then we will show how the semi-analytic calculi consisting of these rules together with our generalization of her centered axioms, lead to the feasible Craig interpolation property. Using this relationship, we first present a uniform method to prove interpolation for different logics from sub-structural logics FL_e, FL_{ec}, FL_{ew} and IPC to their appropriate classical and modal extensions, including the intuitionistic and classical linear logics. Then we will use our theorem negatively, first to show that so many sub-structural logics including $\L_n$, $G_n$, $BL$, $R$ and $RM^e$ and almost all super-intutionistic logics (except at most seven of them) do not have a semi-analytic calculus. To investigate the case that the logic actually has the Craig interpolation property, we will first define a certain specific type of semi-analytic calculus which we call PPC systems and we will then present a sound and complete PPC calculus for classical logic. However, we will show that all such PPC calculi are exponentially slower than the classical Hilbert-style proof system (or equivalently LK+Cut). We will then present a similar exponential lower bound for a certain form of complete PPC calculi, this time for any super-intuitionistic logic.
    • 12.11.18   14:00
    • Ilario Bonacina
    • (Universitat Politčcnica de Catalunya)
    • Clique is Hard on Average for Regular Resolution
    • Abstract:
    • Deciding whether a graph G with n vertices has a k-clique is one of the most basic computational problems on graphs. In this talk we show that certifying k-clique-freeness of Erdos-Renyi random graphs is hard for regular resolution. More precisely we show that, for k
    • 22.10.18   14:00
    • Navid Talebanfard
    • (Institute of Mathematics)
    • Structure in Proof Complexity: The Case of Tseitin and Tree Decompositions
    • Abstract:
    • One of the main difficulties of proving lower bounds in proof complexity is that we cannot (seemingly) make structural assumptions about the proof and thus our argument should work against any conceivable proof (which may not even exist). I will survey a few old results showing that in some cases it is possible to prove structural properties of proofs of specific formulas or minimal proofs of arbitrary formulas. Then I will give a more direct proof of our result with Nicola Galesi and Jacobo Toran showing that the minimum width of Tseitin formulas is the same in general and regular resolution.
    • 24.09.18   14:00
    • Nicola Galesi
    • (Sapienza University of Rome)
    • Resolution and the binary encoding of combinatorial principles
    • Abstract:
    • We investigate the size complexity of proofs in RES(s) -- an extension of Resolution working on s-DNFs instead of clauses -- for families of contradictions given in the unusual binary encoding. A motivation of our work is to approach size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the k-Clique principle, whose Resolution complexity is still unknown. The approach is justified by the observation that for a large class of combinatorial principles short RES(log n) refutations for the binary encoding are obtained from short Resolution refutations of the unary encoding, in particular for the k-Clique principle. In the talk we show a n^{Omega(k)} lower bound for the size of refutations of the binary k-Clique Principle in RES(log log n). This improves a result of Lauria, Pudlák, Rödl and Thapen, who proved the lower bound for Resolution, that is RES(1). Resolution lower bounds for the (unary) k-Clique principle are known only when refutations are either treelike or read-once. The result is part of a larger work investigating the complexity of proofs in RES(s) for binary encodings of combinatorial principles, written jointly with Stefan Dantchev and Barnaby Martin and available at https://arxiv.org/abs/1809.02843
    • 17.09.18   14:00
    • Pavel Hrubes
    • (Institute of Mathematics)
    • An interesting (?) problem equivalent to Continuum Hypothesis
    • Abstract:
    • I will discuss a problem which came up in the context of machine learning, and which ended up being undecidable in ZFC. The flavor is similar to the so-called Axioms of Symmetry of Freiling. Based on a work with B. Shai-David, S. Moran, A. Shpilka, A. Yehudayoff.
    • 04.06.18   14:00
    • Emil Jerabek
    • (Institute of Mathematics)
    • Rigid models of Presburger arithmetic
    • Abstract:
    • While all first-order theories have plenty of models with many automorphisms (e.g., saturated), models with few automorphisms are harder to come by, and their existence varies with the theory. In the extreme case of rigid models (= with no nontrivial automorphism), some theories have no rigid models at all (such as divisible ordered abelian groups), while e.g. Peano arithmetic has many: every model of PA has a rigid elementary end-extension of the same cardinality. In this talk, we will give a complete description of rigid models of Presburger arithmetic Th(Z,+,
    • 28.05.18   14:00
    • Arnold Beckmann
    • (Swansea University)
    • Hyper Natural Deduction
    • Abstract:
    • We introduce Hyper Natural Deduction as an extension of Gentzen's Natural Deduction system by communication like rules. The motivation is to obtain a natural deduction like system which is equivalent to Avron's Hypersequent Calculus for Goedel-Dummett Logic, and which permits natural conversion rules for normalisation as an extension of the well-known conversion rules for Natural Deduction. The ultimate goal of this project is to establish a Curry-Howard correspondence to some (yet to be found) model of parallel computation. An additional aim is to shed further light on Avron's suggestion [in A. Avron: Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence, 4(1991), 225-248] that a hypersequent can be thought of as a multiprocess. This is joint work with Norbert Preining, supported by a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award #IE130639.
    • 21.05.18   14:00
    • Jan Krajíček
    • (Charles University)
    • Proof Complexity Catch 22
    • Abstract:
    • I will present some views on the structure of proof complexity and possible research directions, illustrating them by some theorems and problems.
    • 23.04.18   14:00
    • Pavel Pudlák
    • (IM CAS)
    • A proof system polynomially equivalent to bounded depth Frege, part 3
    • Abstract:
    • In the 3rd part we will show how to reduce the disjoint NP pairs of the games we introduced in the 2nd part to the canonical pairs of bounded depth Frege systems. To this end we will use the proof system equivalent to bounded depth Frege introduced in the 1st part. Given a refutation of A(x) & B(y) in this system, we will define a game and show that a satisfying assignment for A(x) (resp. B(y)) can be transformed into a positional winning strategy for Player I (resp. II).
    • 16.04.18   14:00
    • Lorenzo Carlucci
    • (Sapienza University of Rome)
    • On the strength of some natural restrictions of Hindman's Theorem
    • Abstract:
    • Hindman's Finite Sums Theorem states that any finite coloring of the positive integers admits an infinite sequence such that any sum of finitely many distinct elements from that sequence has the same color. Some interesting open problems exist related to this theorem both in Combinatorics and in Computable or Reverse Mathematics. The best lower and upper bound known locate the strength of the theorem between the Halting Set and Arithmetical Truth, leaving a huge gap in-between. These bounds, due to Blass, Hirst and Simpson, have not been improved since the Eighties. Hindman, Leader and Strauss asked in 2003 whether there exists a proof of the restriction of Hindman's Theorem to sums of one or two elements that does not prove the full theorem. The question is still open and can be made precise in the context of Computable or Reverse Mathematics. We report on recent results on the strength of restrictions of Hindman's Theorem. For example we show that the known lower bound for the full theorem already holds for its restrictions to sums of one or two elements. We furthermore discuss some "weak yet strong" variants admitting both a significant lower bound and a much lower upper bound than the upper bound known on the full theorem. We also discuss connections with the Increasing Polarized Ramsey's Theorem and highlight the role of a sparsity condition on the solution set, which we call partness. Part of the work presented is joint with Kolodziejczyk, Lepore and Zdanowski.
    • 09.04.18   14:00
    • Albert Atserias
    • (Universitat Politčcnica de Catalunya)
    • Locally consistent equations, the structure of solution spaces, and quantum information games
    • Abstract:
    • I will start with a (partial) survey of some recent results on the proof complexity of the graph isomorphism problem with a surprising outcome: for certifying that two graphs are non isomorphic, Polynomial Calculus over the reals, Sherali-Adams, and Sums-of-Squares proofs are equally powerful (or weak). I will try to convey why I think this outcome is surprising. Then I will link this topic to the area of perfect strategies in quantum information games. We show that there are graphs that are quantum isomorphic but not classically isomorphic, and a complete characterization of the Boolean constraint languages that admit instances that are quantum but not classically realizable.
    • 26.03.18   14:00
    • Pavel Pudlák
    • (IM CAS)
    • A proof system polynomially equivalent to bounded depth Frege, part 2
    • Abstract:
    • Our proof system is based on deep inferences rules. The only nonstructural rules of the system are resolution and the rule dual to resolution. The system is inspired by the proof system of Skelley and Thapen that they used to characterize provably total functions in Bounded Arithmetic. Our aim is to use the system to find a combinatorial characterization of canonical pairs of Bounded depth Frege systems.
    • 19.03.18   14:00
    • Pavel Pudlák
    • (IM CAS)
    • A proof system polynomially equivalent to bounded depth Frege
    • Abstract:
    • Our proof system is based on deep inferences rules. The only nonstructural rules of the system are resolution and the rule dual to resolution. The system is inspired by the proof system of Skelley and Thapen that they used to characterize provably total functions in Bounded Arithmetic. Our aim is to use the system to find a combinatorial characterization of canonical pairs of Bounded depth Frege systems.
    • 12.03.18   14:00
    • Amir Tabatabai
    • (AVCR and Charles University)
    • Proof mining in bounded arithmetic, part 3
    • Abstract:
    • A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.
    • 05.03.18   14:00
    • Amir Tabatabai
    • (AVCR and Charles University)
    • Proof mining in bounded arithmetic, part 2
    • Abstract:
    • A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.
    • 19.02.18   14:00
    • Amir Tabatabai
    • (AVCR and Charles University)
    • Proof mining in bounded arithmetic
    • Abstract:
    • A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.
    • 05.02.18   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Semantic cutting planes with small coefficients
    • Abstract:
    • Cutting planes (CP) is a proof system whose lines are linear integral inequalities. It was shown recently by Filmus, Hrubes and Lauria that a semantic version of CP (that is, allowing any sound rule) is exponentially stronger than usual CP. I will discuss some upper bounds on the refutational and implicational completeness of CP, and show from these that semantic CP can be simulated by CP, if we only consider semantic refutations with very small coefficients. Joint work with Massimo Lauria.
    • 15.01.18   14:00

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

  •