Logic Seminar
The seminar is usually on Mondays, from 13:30 to 15:00. The location is the Institute of Mathematics, Žitná 25, in the lecture hall on the ground floor of the rear building. The programme is announced via the mailing list.
Monday 10th June, 1:30pm - Mikoláš Janota, "On Propositional QBF Expansions and Q-Resolution"Quantified Boolean formulas (QBFs) naturally extend propositional logic with quantification and thus providing higher expressivity at the cost of higher complexity---deciding a QBF is PSPACE-complete. Just as resolution serves as a basis of modern SAT solvers, Q-resolution is the basis for DPLL-based QBF solvers. However, there are competitive QBF solvers that solve a given formula by eliminating all but one quantifier, which is solved by a SAT solver. Inspired by this approach, we define a proof system for QBF, which expands all universal quantifiers by rewriting them to conjunctions. The resulting formula is then refuted by propositional resolution.
We will show that such system p-simulates tree Q-resolution. In the opposite direction we will show that Q-resolution p-simulates a certain fragment of our proof system. We conclude by showing certain formulas that hint towards an incomparability of the two systems.
The logic seminar is intended for people doing research in mathematical logic, including doctoral students. Talks are given by regular participants and guests on their own work as well as on interesting recent developments in the field. The prevailing themes in recent years are proof complexity, bounded arithmetic and logical aspects of computational complexity theory in general. Regular participants include members of the logic group, including a number of postdoctoral visitors and Ph.D. students. The seminars are conducted in English unless all participants speak Czech (which seems to never happen).There is also a student logic seminar at Charles University, intended for undergraduate students.
The seminar has been organized continuously since the early 1970s, first by Petr Hájek for more than twenty years, from the early 90s until the summer of 2008 mostly by Jan Krajíček, and since fall 2008 by Neil Thapen.
Kód předmětu (MFF UK): AIL056 (zimní semestr) a AIL080 (letní semestr)
Past programme
Programme archive for summer 2008 - 2010
- 28th February 2011 - Emil Jeřábek, "Real closures of models of arithmetic" - This is a joint work with Leszek Kołodziejczyk. If R is a countable recursively saturated real-closed field, and T any consistent r.e. extension of IOpen, then R has an integer part M which is a model of T by resplendence. In a recent paper, D'Aquino, Knight and Starchenko have shown a kind of converse: if R is a real-closed field with an integer part M which is a model of I\Sigma_4, then R is recursively saturated. We will generalize this result to fragments of bounded arithmetic (IE_2, PV, \Sigma^b_1-IND^{|x|_k}). This suggests that recursive saturation of real closure is a Tennenbaum-like property.
- 7th March - Pavel Pudlák, "Logic of space-time and relativity theory" - I will present "Logic of space-time and relativity theory" by Andreka, Madarasz and Nemeti. They propose first order axiomatizations of special and general theories of relativity. The talk should be understanble without a deeper background in physics.
- 28th March - Pavel Pudlák, "Finitism and physical reality" - This will be another seminar about the philosophy of mathematics. The main question about which it will revolve is: Are the physical natural numbers the same as the mathematical natural numbers?
- 4th April - Jan Krajíček, "On the proof complexity of TC^0 Frege systems" - We make some observations on the relation of AC^0 and TC^0 Frege proof systems.
- 11th April - Petr Glivicky, "Quantifier elimination in Linear Arithmetic and Peano Products" - While Presburger arithmetic (Pr) is a descriptively simple theory (has an elimination set consisting of $\Sigma$-formulas), Peano arithmetic (P) has no elimination at all. I will introduce a theory of Linear arithmetic (LA) which extends Pr by multiplication by one scalar (with full induction) and prove that it has still an elimination set consisting of $\Sigma$-formulas. I will use this result to show some properties of products in models of Peano arithmetic (Peano products) concerning in particular mutual (in)dependence of values of a Peano product in different points.
- 18th April - Jan Krajíček, "Algorithmic dense model theorem, a survey" - The following is from an abstract of Impagliazzo's talk. "Green and Tao used the existence of a dense subset indistinguishable from the primes under certain tests from a certain class to prove the existence of arbitrarily long prime arithmetic progressions. Reingold, Trevisan, Tulsiani and Vadhan, and independently, Gowers, give a quantitatively improved characterization of when such dense models exist. An equivalent formulation was obtained earlier by Barak, Shaltiel and Wigderson." Impagliazzo found a connection with the hard core theorems about pseudorandom generators. The theorem may also be potentially useful in proof complexity.
- 2nd May - Jan Krajíček, "Algorithmic dense model theorem, a survey", Part 2
- 9th May - Marta Bílková, "Moss' coalgebraic modal logic" - Coalgebras provide a uniform framework to deal with various semantic structures for existing modal languages (various types of Kripke frames), as well as various state based transition systems (automata). [ Technically, given a functor T: Set --> Set, a T-coalgebra is a map c: X -->TX, (X is a set of "states", T is the type of "behaviour" or "future", and c is the transition map.) ] Recently various people concentrate both on coalgebraic approach to existing modal logics and finding expressive modal languages for interesting classes of colgebras. In this talk I'll concentrate on one of the possible approaches to the latter, proposed by Larry Moss in 90's. The main idea is that to define a language for T-coalgebras one can deal with a single modality coming from the functor T (its semantics as well as syntax is given by the functor). I'll show how to give a uniform axiomatization and to define cut-free sequent style proof systems for such languages. I'll also try to say how useful can such a language be for ordinary modal language (it provides a disjunctive normal form which e.g. simplifies some interpolation proofs).
- 16th May - Massimo Lauria, "The proof complexity of Paris-Harrington tautologies" - We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. We study the proof complexity of Paris-Harringtons Large Ramsey Theorem for bicolorings of graphs. We prove a non-trivial conditional lower bound in Resolution and a quasi-polynomial upper bound in bounded-depth Frege. The lower bound is conditional on a hardness assumption for a Weak (quasi-polynomial) Pigeonhole Principle in Res(2). The proof technique of the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by applying some highly non-trivial constructions due to Erdos and Mills. (Joint work with Lorenzo Carlucci and Nicola Galesi.)
- 17th October - Pavel Pudlák, "Models explaining pseudorandomness by randomness" - We construct a nonstandard model of arithmetic M_0, an element \Delta \in M_0, a system S of extensions of M_0 and a probability measure on S such that: M_0 is a model of PV; every N \in S is an elementary extension of M_0 w.r.t. polynomial time computable predicates; and for every pseudorandom function f with two values -1 and 1, the probability that f(\Delta)=1 is 1/2 for random N.
- 24th October - Emil Jeřábek, "Root finding in TC^0" - We show that for any constant d, there is a uniform TC^0 algorithm computing approximations of complex zeros of degree d univariate rational polynomials (given by a list of coefficients in binary). The basic idea is to compute the inverse of the polynomial by a power series, using tools from complex analysis, and the result of Hesse, Allender and Barrington that division and iterated products are computable in uniform TC^0. This work is motivated by bounded arithmetic. The complexity class TC^0 contains the basic arithmetical operations (addition, multiplication, ordering), but it is not clear which properties of these operations are provable in the corresponding theory VTC^0 (for binary numbers, i.e., the string sort). It is not even known whether VTC^0 proves integer division to be total. Our result can be equivalently restated as follows: VTC^0 extended with the set of all true \forall\Sigma^B_0 sentences includes IOpen (induction for open formulas in the basic language of arithmetic).
- 31st October - Dai Tri Man Le, "Complexity Classes and Theories for the Comparator Circuit Value Problem" - Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and show how to formalize them in VCC*.
- 14th November - Alexander Smal, "Optimal heuristic algorithms for the image of an injective function" - The existence of optimal algorithms is not known for any decision problem in NP - P. We consider the problem of testing the membership in the image of an injective function. We construct optimal heuristic algorithms for this problem in both randomized and deterministic settings (a heuristic algorithm can err on a small fraction 1/d of the inputs; the parameter d is given to it as an additional input). Thus for this problem we improve an earlier construction of an optimal acceptor (that is optimal on the negative instances only) and also give a deterministic version.
- 21st November - Jakob Nordström, "A general paradigm(?) for proving time-space trade-offs in proof complexity" - I will survey a recent line of work on proving time-space trade-offs for resolution (partly joint with Hastad and Ben-Sasson) and describe how these results can be viewed as a general technique of amplifying weak lower bounds to stronger lower bounds in proof complexity. I will then show that this general paradigm generalizes to the k-DNF resolution proof systems, and discuss whether it might be made to work for Polynomial Calculus and Cutting Planes as well. Time permitting, I might briefly mention some new results that can be interpreted as indicating that this should be the case.
- 28th November- Yuval Filmus, "Scales of prefix codes for N" - We consider monotone prefix codes for the natural numbers. These codes come up naturally in software engineering, and "universal" codes have been suggested by Elias (75). Elias suggested an infinite sequence of codes which get progressively better, and diagonalized his construction to produce an ultimate code. We show that Elias's ultimate code -- or any other single code, or even sequence of codes -- is not optimal by finding a code better than any given sequence of codes. This implies that a scale exists if CH holds, and that in Cohen's model without CH, there is no scale. Given a (uniformly) recursive sequence of codes, the code our construction produces is also recursive. Consequently, we also get a version of the fast-growing hierarchy for codes.
- 5th December - Neil Thapen, "More on approximate counting and search problems" - Jeřábek's theory for approximate counting consists of the bounded arithmetic theory T^1_2 together with the surjective weak pigeonhole principle (sWPHP) for P^NP functions. It is consistent with what is known that every \Sigma^b_1 sentence provable in bounded arithmetic is already provable in this theory, although it is expected that this is not the case. We consider the provable \Sigma^b_1 sentences (also known as total search problems) of natural subtheories of approximate counting. I will talk about some new results in this area: I will give a separation between T^2_2 and PV + sWPHP for P^NP functions in the relativized case; and I will describe a plausible conjecture about narrow resolution refutations that implies a similar separation for T^1_2 + sWPHP for polynomial time functions. Joint work with Sam Buss and Leszek Kołodziejczyk.
- 12th December - Sebastian Müller, "Proof Complexity of Random 3CNF Formulas" - Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Omega(n^{1.5-epsilon}) clauses (Ben-Sasson and Wigderson). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Omega(n^{2/ log n}) clauses, shown by Beame et al. Using a technique by Feige, Kim and Ofek we will see that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we will construct polynomial-size propositional refutations whose lines are TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables and Omega(n^1.4) clauses. Part of the argument is a spectral one and we therefore need to develop an appropriate way to reason about objects such as some Eigenvalues in a weak arithmetic.
- 8th October 2012 - Emil Jeřábek, "Integer factoring by parity arguments" - Papadimitriou introduced several classes of NP search problems based on combinatorial tasks. In particular, the class PPA (polynomial parity argument) consists of problems reducible to the following problem: given a circuit representing an undirected graph of maximum degree 2, and a vertex of degree 1, find another vertex of degree 1. Equivalently, a problem is in PPA if it is reducible to finding a fixpoint of a given involutive function (represented by a circuit) on a domain of odd size. The main result of this talk is that integer factoring has a randomized reduction to a PPA problem. (The reduction can be derandomized assuming a suitable version of the generalized Riemann hypothesis.) This improves a previous result of Buresh-Oppenheim that PPA can factor integers n = 1 (mod 4) having a prime divisor p = 3 (mod 4). The main ingredient of our proof is that the following problem is in PPA: given integers a,n such that the Jacobi symbol (a|n) = 1, find either a square root of a mod n, or a factor of n. We can show this by proving the law of quadratic reciprocity and multiplicativity of the Jacobi symbol in a suitable extension of bounded arithmetic corresponding to PPA, and applying a witnessing theorem. We may also discuss some related results, such as a randomized reduction of factoring to PPP (more precisely, the weak pigeonhole principle), and computing square roots mod n in PPA.
- 16th October - Neil Thapen, "Automatizability and games" - Parity games, mean payoff games and simple stochastic games are families of two-player games played on finite graphs. In each game, deciding which player has a winning strategy is in NP intersect coNP, and it is an open problem to establish whether or not it is in P. A proof system is called weakly automatizable if, roughly speaking, there is a polynomial time algorithm which distinguishes between formulas that are satisfiable and formulas which have a short refutation in the system. Recent papers by Atserias and Maneva and by Huang and Pitassi have shown that the decidability of mean payoff games and simple stochastic games is reducible to the weak automatizability of certain constant-depth proof systems. We simplify and extend their results, in particular showing that if resolution is weakly automatizable, then parity games can be decided in polynomial time. Joint work with Arnold Beckmann and Pavel Pudlak.
- 29th October - Pavel Pudlák, "How difficult is it to prove that a graph is non-Ramsey?" - We will prove a lower bound on resolution proofs of a tautology expressing that a given graph does not have homogeneous sets of size c.log n, where n is the number of vertices.
- 12th November - Wojciech Dzik, "Unification of terms in equational theories and in logic" - Unifiers, i.e. substitutions making two terms equal, modulo a given theory, are quasi-ordered by the relation of "being more general than". Unification type of a theory (or a logic) can be unitary, finitary, infinitary or nullary, depending on the number of maximal (with respect to the quasi-order) unifiers. I will show that in case of (weakly) transitive theories (logics) there is a particular splitting (join-splitting) in the lattice of all theories (logics) which determines particular unification types. I will also give some applications of (projective) unifiers to the problem of admissible rules in logic.
- 26th November - Michal Garlík, "On a Proof of Ajtai's Completeness Theorem for Nonstandard Finite Structures" - Ajtai's generalization of Gödel's completeness theorem describes a definability condition equivalent to the existence of an extension and expansion of a given nonstandard finite structure to a model of a given recursive theory. I will present a proof of the theorem and discuss some applications of the theorem which relate to problems in computational complexity.
- 10th December - Michal Garlík, "On a Proof of Ajtai's Completeness Theorem for Nonstandard Finite Structures", Part 2
- 14th January 2013 - Jan Pich, "Intuitionism and Natural Proofs" - We will discuss the question whether intuitionistic proofs of superpolynomial circuit lower bounds in theories of bounded arithmetic are natural and the problem of efficient witnessing errors of p-time SAT algorithms.
- 18th February - Jindřich Zapletal, "Canonical Ramsey Theory on Polish Spaces" - I will outline the subject of my new book with Vladimir Kanovei and Marcin Sabok. It concerns the classification effort for Borel equivalence relations in descriptive set theory.
- 25th February - Neil Thapen, "The complexity of proving that a graph is Ramsey" - Say that an graph with n vertices is c-Ramsey if it contains no clique or independent set of size c log n. Such a graph witnesses that the Ramsey number r(k) > 2^{k/c}. We define a propositional formula which expresses that a given graph G is c-Ramsey, and show that this formula requires superpolynomial size to prove in resolution, for every graph G. In particular it follows that no polynomial time algorithm for constructing c-Ramsey graphs has a polynomial size resolution proof of its correctness. We rely on a property of c-Ramsey graphs, that every such graph must contain a large subgraph with some of the density properties of the random graph. Other than this, I aim to give a fairly self-contained presentation and will review the necessary background in proof complexity. This is an update of material which Pavel Pudlák presented in the seminar last year.
- 4th March - Neil Thapen, "The complexity of proving that a graph is Ramsey", Part 2
- 11th March - Jan Pich, "Circuit lower bounds in bounded arithmetics" - We will present a natural formalization of polynomial circuit lower bounds in the language of bounded arithmetic, show its properties and some new unprovability results.
- 18th March - Jan Pich, "Circuit lower bounds in bounded arithmetics", Part 2
- 25th March - Albert Atserias, "Quasipolynomial Upper and Lower Bounds for DNF-refutations of a Relativized Weak Pigeonhole Principle" - The relativized weak pigeonhole principle states that if 2n out of n^2 pigeons fly into n holes then some hole must be doubly occupied. By interpreting the usual weak pigeonhole principle in it we note that it has quasipolynomial size n^{polylog(n)} refutations in R(log). We prove a matching lower bound: any R(log), and indeed any DNF-refutation, must have size n^{(log n)^{1/2-\eps}} for every \eps and sufficiently large n. This is joint work with Moritz Müller (Vienna), and Sergi Oliva (Barcelona)
- 8th April - Helmut Schwichtenberg, "Proofs, computations and analysis" - Algorithms are viewed as one aspect of proofs in (constructive) analysis. Data for such algorithms are finite or infinite lists of signed digits -1, 0, 1 (i.e., reals as streams), or possibly non well-founded labelled (by lists of signed digits -1, 0, 1) ternary trees (representing uniformly continuous functions). A theory of computable functionals (TCF) suitable for this setting is described. The main tools are (i) a distiction between computationally relevant and irrelevant logical connectives and (ii) simultaneous inductively/coinductively defined predicates. A realizability interpretation of proofs in TCF can be given, and a soundness theorem holds.
- 15th April - Jan Krajíček, "On the computational complexity of finding hard tautologies" - It is well-known that a polynomial time algorithm finding tautologies hard for a propositional proof system P exists iff P is not optimal. Such an algorithm takes 1^(k) and outputs a tautology A_k of size at least k such that P is not p-bounded on the set of all A_k's. We consider two more general search problems involving finding a hard formula, Cert and Find, motivated by two hypothetical situations: that one can prove that NP and coNP differ and that no optimal proof system exists. In Cert one is asked to find a witness that a given non-deterministic circuit with k inputs does not define TAUT restricted to size k. In Find, given 1^k and a tautology B of size at most k^c, one should output a size k tautology that has no size k^d P-proof from substitution instances of B. We shall prove, assuming the existence of an exponentially hard one-way permutation, that Cert cannot be solved by an algorithm in time exp(k). Using a stronger hypothesis about the proof complexity of Nisan-Wigderson generator we show that both problems Cert and Find are actually undefined for infinitely many k. The results are based on interpreting the Nisan-Wigderson generator as a proof system.
- 22nd April - Petr Glivický, "Descriptive analysis of linear theories and dependency problem in Peano arithmetic" - There is a large gap between the Presburger (Pr) and Peano arithmetics. One way how to explore this space is to consider various extensions of Pr by fragments of product. Linear theories are certain extensions of Pr by multiplication by a set of scalars and with full induction for their language. We show a quantifier elimination result for linear theories, and we perform a detailed analysis of definable sets and functions in their models. In particular, we state that every definable set in a model A of a linear theory is a finite union of linear images of polyhedra in A^k, for some k. As an application of these results, we solve an important instance of the dependency problem in Peano arithmetic. We prove that, for a fixed saturated model B of Pr, the only values of a Peano product on B which are uniquely determined by its values on the line {a} x B (a is from B) are the trivial ones. This enables us to construct a new product on B which satisfies certain amount of induction.
- 6th May - Hong Van Le, "Voevodsky's homotopy type theory and univalent foundations" - Voevodsky's univalent foundation is an application of his homotopy type theory, relating symbolic logic with topology and computer science. In this talk I will discuss basic concepts, examples, and advantages of homotopy type theory, especially Voevodsky's univalent homotopy type theory. The main references are talks by Voevodsky placed on his website, sources from nLab, wiki and the website http://homotopytypetheory.org/ as well as a paper by Awodey "Type theory and Homotopy".
- 13th May - Emil Jeřábek, "Open induction in VTC^0 + IMUL" - Basic arithmetic operations are computable in uniform TC^0, with multiplication being TC^0-complete. We can define addition, multiplication, and ordering on binary integers in the corresponding bounded arithmetic theory VTC^0, and prove that they form a discretely ordered ring. It is a natural question what other first-order properties of elementary arithmetic operations are provable in VTC^0. Since it is not known whether VTC^0 can formalize the Hesse-Allender-Barrington uniform TC^0 algorithms for division and iterated multiplication, we can also consider the same question for the theory VTC^0 + IMUL, including an axiom for iterated multiplication. In previous work, I have proved that there are uniform TC^0 algorithms for approximation of complex roots of constant-degree univariate rational polynomials, which means that VTC^0 extended with all true \forall\Sigma^B_0 sentences proves induction for open formulas in the language of ordered rings (IOpen). In this talk, I will establish that IOpen is in fact provable in VTC^0 + IMUL.
- 20th May - Alexandre Borovik, "Logical and model-theoretic issues of black box group theory" - The talk will describe a peculiar and perhaps unique phenomenon in mathematics: the so-called "black box" probabilistic algorithms of computational finite group theory and discuss its logical and model-theoretic connections. (Joint work with Sukru Yalcinkaya.)
- 27th May - Emil Jeřábek, "Open induction in VTC^0 + IMUL", Part 2 - We will continue the proof that VTC^0 + IMUL includes open induction in the language of ordered rings. In this second part of the talk, I will finish the computations involved with the formalization of the Lagrange inversion formula, and then I will give a model-theoretic argument using some properties of valued fields to establish the main result.
Programme archive for 1995 - summer 2008
Auxiliary Links
Jech's library of preprints/reprints in set theory is available to students in our department
9/5/10 Neil Thapen
