•  
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles, Part 4
    • Abstract:
    • I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 16.12.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles, Part 3
    • Abstract:
    • I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 09.12.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles, Part 2
    • Abstract:
    • I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 02.12.19   13:30
    • Albert Atserias
    • (Universitat Politčcnica de Catalunya)
    • Automating Resolution Is NP-Hard
    • Abstract:
    • We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, we show that it is NP-hard to distinguish between formulas that have Resolution refutations of polynomial length and those that do not have subexponential length refutations. This also implies that Resolution is not automatizable in subexponential time or quasi-polynomial time unless NP is included in SUBEXP or QP, respectively. This is joint work with Moritz Müller
    • 25.11.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles
    • Abstract:
    • In the present talk I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 18.11.19   13:30
    • Moritz Müller
    • (Universitat Politčcnica de Catalunya)
    • Forcing with partial structures
    • Abstract:
    • Define a finitary combinatorial principle to be a first-order sentence which is valid in the finite but falsifiable in the infinite. We aim to compare the strength of such principles over bounded arithmetics. We distinguish “weak” and “strong” principles based on their behaviour with respect to finite structures that are only partially defined. We show that over relativized T^1_2 “weak” principles do not imply “strong” ones. The proof applies a general forcing method to produce models of relativized T^1_2.
    • 13.11.19   14:00
    • Pavel Pudlák
    • (Institute of Mathematics)
    • The symmetric calculus and monotone interpolation, Part 2
    • Abstract:
    • In this talk I will say a little bit more about the topic that I presented this spring. First I will ask and explain the problem whether the symmetric calculus simulates Frege systems. Then I show how one can strengthen the characterization of the canonical and interpolation pairs. The result can be viewed as monotone interpolation by certain generalizations of monotone Boolean circuits, called bounded depth game schemas. I will also show simulations of point-line game schemas by depth-2 games and vice versa.
    • 11.11.19   13:30
    • Pavel Pudlák
    • (Institute of Mathematics)
    • The symmetric calculus and monotone interpolation
    • Abstract:
    • In this talk I will say a little bit more about the topic that I presented this spring. First I will ask and explain the problem whether the symmetric calculus simulates Frege systems. Then I show how one can strengthen the characterization of the canonical and interpolation pairs. The result can be viewed as monotone interpolation by certain generalizations of monotone Boolean circuits, called bounded depth game schemas. I will also show simulations of point-line game schemas by depth-2 games and vice versa.
    • 04.11.19   13:30
    • Ján Pich
    • (Institute of Mathematics)
    • Why are Proof Complexity Lower Bounds Hard?
    • Abstract:
    • We formalize and study the question of whether there are inherent difficulties to showing lower bounds on propositional proof complexity. We establish the following unconditional result: Propositional proof systems cannot efficiently show that truth tables of random Boolean functions lack polynomial size non-uniform proofs of hardness. Assuming a conjecture of Rudich, propositional proof systems also cannot efficiently show that random k-CNFs of linear density lack polynomial size non-uniform proofs of unsatisfiability. Since the statements in question assert the average-case hardness of standard NP problems (MCSP and 3-SAT respectively) against co-nondeterministic circuits for natural distributions, one interpretation of our result is that propositional proof systems are inherently incapable of efficiently proving strong complexity lower bounds in our formalization. Another interpretation is that an analogue of the Razborov-Rudich 'natural proofs' barrier holds in proof complexity: under reasonable hardness assumptions, there are natural distributions on hard tautologies for which it is infeasible to show proof complexity lower bounds for strong enough proof systems. For the specific case of the Extended Frege (EF) propositional proof system, we show that at least one of the following cases holds: (1) EF has no efficient proofs of superpolynomial circuit lower bound tautologies for any Boolean function or (2) There is an explicit family of tautologies of each length such that under reasonable hardness assumptions, most tautologies are hard but no propositional proof system can efficiently establish hardness for most tautologies in the family. Thus, under reasonable hardness assumptions, either the Circuit Lower Bounds program toward complexity separations cannot be implemented in EF, or there are inherent obstacles to implementing the Cook-Reckhow program for EF. This is a joint work with Rahul Santhanam.
    • 21.10.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Lengths of proofs for Presburger arithmetic
    • Abstract:
    • Speedups (i.e., differences in the lengths of shortest proofs of the same sentences) between various theories in the language of first-order arithmetic and richer languages is a relatively well-studied phenomenon. There are three typical orders of speedup that occur in natural examples: non-recursive speedups, at most polynomial speedups, and speedups of the order of the super-exponentiation function exp*(0)=1, exp*(x+1)=exp(exp*(x)). In the present talk I will compare this situation to what happens over the language of Presburger arithmetic. We consider theories that are complete in the language of Presburger arithmetic and for them the usual quantifier elimination algorithm guarantees that any formula of the length n has a proof of the length ?exp(exp(exp(P(n)))). This shows that speedups in this setting are at most triple-exponential. An important tool for proving non-polynomial speedups for first-order theories is Friedman-Pudlak finite version of Gödel's second-incompleteness theorem. In this talk I'll show how to adopt it to the case of theories in the language of Presburger arithmetic. This yields the result that if T is a system in the language of PA and T?Con(U), then T has at least exponential speedup over U in the language of Presburger arithmetic. Also I'll show that even very weak theories in the language of Peano arithmetic, for example I??, have at least exponential speedups over the standard axiomatization of Presburger arithmetic.
    • 07.10.19   13:30
    • Jannik Vierling
    • (TU Wien)
    • Clause Set Cycles and Induction
    • Abstract:
    • The subject of automated inductive theorem (AITP) proving focuses on the development of procedures that find proofs by induction and their efficient implementation. AITP is of particular relevance to the formal verification of hardware and software. This subject is characterized by a great variety of approaches that are often only empirically studied and their theoretical properties are therefore often unclear. We aim at studying existing approaches to automated inductive theorem proving by applying results from mathematical logic in order to gain a better understanding of the various methods and to explore the relations between them. In this talk I will present the notion of clause set cycles — an abstraction of the n-clause calculus introduced by Kersani and Peltier in 2013. I will explain this formalism in terms of theories of induction and discuss how the study of this formalism is related to subtheories of Presburger arithmetic.
    • 30.09.19   13:30
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • An exponential lower bound for lengths of proofs in substructural logics
    • Abstract:
    • In this talk, we will investigate the lengths of proofs in the usual Gentzen calculus for the substructural logic FL_e. We will present a sequence of tautologies of the system and show any short proof for them implies a short proof for Hrubes' formulas for intuitionistic logic, hence the exponential lower bound follows. We will then conclude that this lower bound also applies to any proof system for a logic between FL_e and IPC.
    • 23.09.19   13:30
    • Nicola Galesi
    • (University of Rome Sapienza)
    • Bounded-depth Frege complexity of Tseitin formulas for all graphs
    • Abstract:

    • We prove that Tseitin formulas Ts(G), for an undirected graph G, require proofs of size 2^{tw(G)^{\Omega(1/d)}} in depth d-Frege systems for d<{K \log n}/{\log \log n}, where tw(G) is the treewidth of G and K a constant. If time will allow, we prove tightness of the lower bound. Namely, that for large enough d, there are depth d-Frege proofs for Ts(G) of size 2^{\tw(G)^{\O(1/d)}} \poly(|Ts(G)|).This is a joint work with Dmitry Itsykson, Artur Riazanov and Anastasia Sofronova

    • 16.09.19   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Complexity of admissible rules with parameters
    • Abstract:
    • A rule \phi_1, ..., \phi_k / \psi is admissible in a (nonclassical) propositional logic L if the set of L-tautologies is closed under substitution instances of the rule. We are particularly interested in the set-up with parameters (constants), which are required to be preserved by substitutions. In this talk, we shall study basic properties of admissibility with parameters in a class of well-behaved transitive modal logics (i.e., extensions of K4). The main goal is a classification of the computational complexity of admissibility (and the closely related problem of unifiability) with parameters based on semantic properties of logics.
    • 27.05.19   13:00
    • Pavel Pudlák
    • (Mathematical Institute)
    • Propositional proofs and monotone computations
    • Abstract:
    • One of the major discoveries of Stephen Cook is that lower bounds on the lengths of proofs in the propositional calculus can be used to prove independence results. This stimulated research into proving lower bounds for various propositional proof systems. Later it was shown that one can use lower bounds on the size of monotone circuits to prove lower bounds on propositional proofs. New models of monotone computations have been proposed recently that potentially may give us lower bounds for more propositional proof systems that we have so far. In this talk we will survey some results that connect lower bounds on monotone computations in various models with lower bounds on the lengths of proofs in proof systems.
    • 20.05.19   13:00
    • Martin Maxa
    • (Charles University)
    • Feasible incompleteness
    • Abstract:
    • We will present finite counterparts to the well-known theorems that are connected to the foundations of mathematics such as Godel's incompleteness theorems or Lob's theorem. Their finite versions go already beyond famous open problems in computational theory, for example P != NP. Beside the finite version of Godel's second incompleteness theorem, we will present also the finite version of Godel's first incompleteness theorem and we will prove that they are equivalent. We will also state a conjecture that could be called a finite version of Lob's theorem.
    • 13.05.19   13:00
    • Jan Bydžovský
    • (Vienna Technical University)
    • Consistency of circuit lower bounds
    • Abstract:
    • Let T be a strong enough universal theory in language L (containing the symbol '<') and let A(x) be a Sigma^b_2 L-formula. What are the sufficient and possibly useful conditions to derive that 1) T+"A(x) fails for some x" is consistent, 2) T+"A(x) fails for infinitely many x" is consistent, 3) T+"A(x) fails for all but finitely many x" is consistent? I will prove a theorem giving such conditions and use the conditions for 1) and 2) respectively to prove that two formalization of the statement    "for every natural number k, there is a polynomial-time computable Boolean-function which is not computable by circuits of size O(n^k)"   one given by Krajicek and Oliveira in [1] and another one given by Bydzovsky and Muller in [2] are both consistent with the theory PV. Time permitting, I will comment on the possible consistency of the scheme    "for every natural number k, there is a polynomial-time computable Boolean-function which is not computable by circuits of size O(n^k) on all but finitely many lengths"   and on obstacles that appears when one wants to replace PV with S^1_2 or some other non-universal theory. Some preliminary knowledge of the definition of an ultrapower and the statement of the Herbrand theorem are welcome but I will briefly remind those at the beginning.   [1] https://www.karlin.mff.cuni.cz/~krajicek/unprov.pdf [2] https://www.cs.upc.edu/~moritz/ultra_M_30_5.pdf
    • 29.04.19   13:00
    • Fedor Part
    • (JetBrains)
    • A first order theory for constant degree Sum of Squares , Part 2
    • Abstract:
    • The Unique Games Conjecture (UGC) predicts that a certain universal algorithm achieves an optimal approximation for a large class of NP optimization problems. This algorithm can be seen as a proof searching procedure for the constant degree Sum-of-Squares (SoS) proof system, which is automatizable via semidefinite programming. The actual strength of this algorithm and, possibly, the fate of UGC depend on what is derivable in constant degree SoS. In some cases one can argue that the SoS algorithm achieves a bound on an instance by taking some known "ZFC" proof that the optimum meets the bound and trying to redo the proof in constant degree SoS. For example, for the integrality gap instance for LP and SDP hierarchies, that is based on Frankl-Rodl graphs, one can show that the SoS algorithm meets the bound on the size of a maximal independent set, guaranteed by the the Frankl-Rodl theorem, by proving the theorem in constant degree SoS. In this talk, we will present work in progress on the conceptual analysis of the reasoning constant degree SoS is capable of. In particular, we will sketch the definition of a first-order theory, which under propositional translation corresponds to constant degree SoS. This is joint work with Neil Thapen and Iddo Tzameret.
    • 15.04.19   13:00
    • Fedor Part
    • (JetBrains)
    • A first order theory for constant degree Sum of Squares
    • Abstract:
    • The Unique Games Conjecture (UGC) predicts that a certain universal algorithm achieves an optimal approximation for a large class of NP optimization problems. This algorithm can be seen as a proof searching procedure for the constant degree Sum-of-Squares (SoS) proof system, which is automatizable via semidefinite programming. The actual strength of this algorithm and, possibly, the fate of UGC depend on what is derivable in constant degree SoS. In some cases one can argue that the SoS algorithm achieves a bound on an instance by taking some known "ZFC" proof that the optimum meets the bound and trying to redo the proof in constant degree SoS. For example, for the integrality gap instance for LP and SDP hierarchies, that is based on Frankl-Rodl graphs, one can show that the SoS algorithm meets the bound on the size of a maximal independent set, guaranteed by the the Frankl-Rodl theorem, by proving the theorem in constant degree SoS. In this talk, we will present work in progress on the conceptual analysis of the reasoning constant degree SoS is capable of. In particular, we will sketch the definition of a first-order theory, which under propositional translation corresponds to constant degree SoS. This is joint work with Neil Thapen and Iddo Tzameret.
    • 08.04.19   13:00
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • An Exponential Lower Bound for Proofs in Focused Calculi
    • Abstract:
    • In her recent paper, Iemhoff introduced a special form of sequent-style rules and axioms, which she called focused, and studied the relationship between the focused proof systems, the systems only consisting of this kind of rules and axioms, and the uniform interpolation of the logic that the system captures. Subsequently, as a negative consequence of this relationship, she excludes almost all super-intuitionistic logics from having these focused proof systems. In this talk, we will strengthen this negative result to show that even in the cases that these systems exist, their proof-length would computationally explode. More precisely, we will first introduce two natural subclasses of focused rules, called PPF and MPF rules. Then, we will introduce some CPC-valid (IPC-valid) sequents with polynomially short tree-like proofs in the usual Hilbert- style proof system, or equivalently LK + Cut, that have exponentially long proofs in the systems only consisting of PPF (MPF) rules.
    • 27.03.19   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Polynomial calculus space and resolution width, part II
    • Abstract:
    • Let w(F) be the width needed to refute a CNF F in resolution. It is well known that the space needed to refute F in resolution is lower bounded by w(F), and it has been open whether something similar holds for polynomial calculus (PCR).  We show, by a novel 'forcing' argument, that the space needed to refute F in PCR is lower bounded by the square root of w(F). Joint work with Nicola Galesi and Leszek Kolodziejczyk. ** Please notice the earlier starting time - 13:00 **  
    • 04.03.19   13:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Polynomial calculus space and resolution width
    • Abstract:
    • Let w(F) be the width needed to refute a CNF F in resolution. It is well known that the space needed to refute F in resolution is lower bounded by w(F), and it has been open whether something similar holds for polynomial calculus (PCR).  We show, by a novel 'forcing' argument, that the space needed to refute F in PCR is lower bounded by the square root of w(F). Joint work with Nicola Galesi and Leszek Kolodziejczyk.
    • 25.02.19   14:00

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

  •