•  
    • Michael Benedikt
    • (University of Oxford)
    • Interpolation for Query Reformulation
    • Abstract:
    • In this talk I will explain query reformulation problems - given a formula Q and a background theory T, the goal is to translate Q, either into another formula or a direct procedural implementation, such that the translation is equivalent to Q according to T, and such that the translation satisfies additional "interface restrictions" - e.g. restrictions on the vocabulary. I will review the approach to solving these problems via interpolation which has been investigated over the last few years, presenting the properties of a proof system and interpolation algorithm we might desire for the application to reformulation. I will then look at some proof methods and associated interpolation algorithms that have been proposed in the past -- via tableaux, resolution, and tree-automata, with some tentative remarks about how these stack up against the requirements.
    • 04.12.17   14:00
    • Wieslaw Kubis
    • (Institute of Mathematics)
    • Weak Fraisse categories and their limits
    • Abstract:
    • I will survey recent developments in the theory of limits of weak amalgamation classes, in the language of category theory, with examples in model theory.
    • 27.11.17   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Bounded arithmetic does not collapse to approximate counting
    • Abstract:
    • We adapt the "fixing lemma", a simple switching lemma used recently to show lower bounds for random resolution, to show that Jerabek's theory of approximate counting does not prove the CPLS principle. This settles an open problem by showing that bounded arithmetic is strictly stronger than approximate counting, if we compare the strength of theories by looking at their \forall \Sigma^b_1 consequences.
    • 20.11.17   14:00
    • Jonathan Verner
    • (Charles University)
    • A Ramsey theorem for Metric spaces
    • Abstract:
    • We use the following variation of the standard Hungarian arrow notation which takes into account additional structure: Let K be a class of structures and kappa,lambda,nu be cardinals. The arrow kappa ->_K (lambda)^1_mu, is shorthand for the statement that for every X in K of size lambda there is a Y in K of size kappa such that for any partition of Y into mu-many pieces one of the pieces contains an isomorphic copy of X. In the talk we will investigate this arrow in the case where K is the class of bounded metric spaces with isomorphic copies being scaled copies. We extend previous work on these questions (e.g. Komjath (1987), Nesetril(2006), Komjath (1987b), Weiss (1990)).
    • 13.11.17   14:00
    • Pavel Pudlák
    • (Institute of Mathematics)
    • Incompleteness in the finite domain, Part 2
    • Abstract:
    • The title is just a new name for what I used to call "feasible incompleteness". In this lecture I will recall some basic old results and mention some new developments in this field.
    • 16.10.17   14:00
    • Pavel Pudlák
    • (Institute of Mathematics)
    • Incompleteness in the finite domain
    • Abstract:
    • The title is just a new name for what I used to call "feasible incompleteness". In this lecture I will recall some basic old results and mention some new developments in this field.
    • 09.10.17   14:00
    • Igor Oliveira
    • (Charles University)
    • Unprovability of circuit upper bounds in Cook's theory PV
    • Abstract:
    • We establish unconditionally that for every integer k>=1 there is a language L in P such that it is consistent with Cook's theory PV that L is not in Size(n^k). Our argument is non-constructive and does not provide an explicit description of this language.
    • 19.04.17   13:30
    • Kateřina Trlifajová
    • (Faculty of Information Technology, Czech Technical University, Prague)
    • Is Bolzano's theory of infinity consistent?
    • Abstract:
    • Bolzano's theory of infinity which is mostly contained in his Paradoxes of Infinity from 1848 is usually considered as a step in a wrong direction. Both Bolzano and Cantor defended actual infinity in mathematics. But while Cantor based his measuring of infinite sets on the one-to-one correspodence Bolzano based it on the part-whole principles: the whole is greater than its part. We'll demonstrate there are several interpretations of Bolzano's theory. Some of them are based on the framework of non-standard analysis. An open question remains: is there a meaningful interpretation without ultrafilters? Consequently, was Cantor's theory of infinite numbers inevitable?
    • 10.04.17   13:30
    • Petr Glivicky
    • (University of Economics & Charles University)
    • Nonstandard methods in Ramsey-type combinatorics, part II
    • Abstract:
    • Recently, nonstandard methods have been successfully applied in many areas of combinatorics. The nonstandard methodology provides an extension of the universe of mathematics by new ideal (nonstandard) objects such as "an infinitely large natural number", "an infinitely small neighborhood of a point", and many more. The rich structure of relations between the original (standard) and the new (nonstandard) objects enables the standard objects and their standard properties to be described and studied by means of nonstandard concepts. It turns out that this nonstandard description is in many cases more elegant and the nonstandard proofs clearer and shorter than their standard alternatives. In this series of two talks, I outline a nonstandard approach to Ramsey-type combinatorics. I prove two nonstandard Ramsey-type principles of the following common form (vaguely): "If, in a coloring of finite subsets of natural numbers, certain nonstandard object (a witness) has a color C, then there is an infinite subset of natural numbers homogeneously having the color C." As applications of these principles I give very short and simple nonstandard proofs of several well-known Ramsey-type combinatorial theorems, including Ramsey's, Hilbert's and Hindmann's theorems. This is joint work with Josef Mlček. In this second talk, I will build up a theory of the infinitely iterated nonstandard extension of the set of natural numbers and I will use it to prove the combinatorial results mentioned above.
    • 31.03.17   13:30
    • Petr Glivicky
    • (University of Economics & Charles University)
    • Nonstandard methods in Ramsey-type combinatorics, part I
    • Abstract:
    • Recently, nonstandard methods have been successfully applied in many areas of combinatorics. The nonstandard methodology provides an extension of the universe of mathematics by new ideal (nonstandard) objects such as "an infinitely large natural number", "an infinitely small neighborhood of a point", and many more. The rich structure of relations between the original (standard) and the new (nonstandard) objects enables the standard objects and their standard properties to be described and studied by means of nonstandard concepts. It turns out that this nonstandard description is in many cases more elegant and the nonstandard proofs clearer and shorter than their standard alternatives. In this series of two talks, I outline a nonstandard approach to Ramsey-type combinatorics. I prove two nonstandard Ramsey-type principles of the following common form (vaguely): "If, in a coloring of finite subsets of natural numbers, certain nonstandard object (a witness) has a color C, then there is an infinite subset of natural numbers homogeneously having the color C." As applications of these principles I give very short and simple nonstandard proofs of several well-known Ramsey-type combinatorial theorems, including Ramsey's, Hilbert's and Hindmann's theorems. This is joint work with Josef Mlček. In this first talk, I will give an "Introduction to nonstandard methods for standard mathematicians". I will build up all the necessary nonstandard concepts and methods from scratch and show some simple yet rather impressive applications and examples. Only the knowledge of very elementary set theory and logic will be assumed.
    • 13.03.17   13:30
    • Nicola Galesi
    • (Sapienza University Rome)
    • Refuting random 3-CNFs using polynomials requires large proof space
    • Abstract:
    • A main tool in proving (space) lower bounds? for refuting random k-CNF formulas is the well-known expansion property of incidence graph of the formula. Nevertheless, for k=3 the expansion is no longer sufficient to prove proof space lower bounds for Polynomial Calculus (PCR), a proof system working with polynomials. In the talk we first give an overview of a general technique for proving prove space lower bounds for random CNFs. Then we present a variant of Hall's theorem stating that in bipartite graphs G=(L, R) with left-degree at most 3, L can be covered by certain families of disjoint paths, provided that L expands in R by a factor of (2 ? ?), for ?
    • 06.03.17   13:30
    • Pavel Hrubeš
    • (Institute of Mathematics)
    • Monotone interpolation and Cutting Planes
    • Abstract:
    • We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept we call an unsatisfiability certificate. This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we prove exponential lower bounds for random (log n)-CNFs, and for the Weak Bit Pigeon Hole Principle.
    • 27.02.17   13:30
    • Dmitry Sokolov
    • (PDMI, Russian Academy of Sciences)
    • On OBDD based proof systems that dynamically change order of variables
    • Abstract:
    • In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deducing of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. In this talk we consider OBDD based proof systems that additionally contain a rule that allows to change the order in OBDDs. At first we consider a proof system OBDD(\land, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separates this proof system from OBDD(\land)-proof system that uses only conjunction rule. We prove two exponential lower bounds on the size of OBDD(\land, reordering)-refutation of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(\land)-proofs and the second one extends the result of Tveretina et. al from OBDD(\land) to OBDD(\land, reordering). Joint work with Dmitry Itsykson, Alexander Knop and Andrey Romashchenko.
    • 30.01.17   13:30
    • Dmitry Sokolov
    • (Russian Academy of Sciences)
    • Dag-like communication
    • Abstract:
    • In this talk we consider a model of dag-like communication complexity (instead of classical one where protocols correspond to trees). We prove an analogue of Karchmer-Wigderson Theorem for this model and boolean circuits. We also consider a relation between this model and communication PLS games proposed by Razborov in 1995 and simplify the proof of Razborov's analogue of Karchmer-Wigderson Theorem for PLS games. We also consider a dag-like analogue of real-valued communication protocols and adapt a lower bound technique for monotone real circuits to prove a lower bound for these protocols. We use real-valued dag-like communication protocols to generalize the ideas of "feasible interpolation" technique, which helps us to prove a lower bound on the Cutting Plane proof system (CP) and adopt it to "random CP" by using recent result of Krajicek. Our notion of dag-like communication games allows us to use a Raz-McKenzie transformation from Goos and Pitassi paper, which yields a lower bound on the real monotone circuit size for the CSPSAT problem.
    • 16.01.17   13:30
    • Massimo Lauria
    • (Universitat Politčcnica de Catalunya)
    • Circular (Yet Sound) Proofs
    • Abstract:
    • We introduce a new way of representing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition proofs are represented in the form of directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is used as a hypothesis of a rule. We call such proofs circular. We show that for all rule-based proofs systems, circular proofs are sound and, obviously, complete. For Frege systems, in which arbitrary propositional formulas are allowed in the proofs, we show that circular proofs can be converted into tree-like ones with at most polynomial overhead. The proof goes by a translation into an arithmetic statement and is thus indirect. For resolution, where the only allowed formulas are clauses, the arithmetic statement becomes a proof in the Sherali-Adams proof system that preserves both length/number-of-monomials and width/degree, up to small factors. Surprisingly, a reverse translation also holds: every Sherali-Adams refutation of a CNF formula translates into a circular resolution refutation of comparable length/number-of-monomials and width/degree. As corollaries we get: 1) polynomial-time algorithms that find circular resolution refutations of constant width, 2) examples showing that circular resolution proofs are sometimes exponentially more succinct than dag-like resolution proofs, and 3) exponentially hard examples for circular resolution.
    • 09.01.17   13:30

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

  •