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 4th November, 1:30pm - Nicola Galesi, "Space Lower Bounds for Random Formulae in Algebraic Proof Systems"

The study of space measure in Proof Complexity has gained in the last years more and more importance: first it is clearly of theoretical importance in the study of complexity of proofs; second it is connected with SAT solving, since it might provide theoretical explanations of efficiency or inefficiency of specific Theorem Provers or SAT-solvers; finally it is connected with important characterizations studied in Finite Model Theory, thus providing a solid link between the two research fields.

In the talk we will present recent work where we devise a new general combinatorial framework for proving space lower bounds in algebraic proof systems like Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR). Our method can be viewed as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution. This can be seen as a first step towards a precise characterization of the space for algebraic systems in terms of combinatorial games, like Ehrenfeucht-Fraisse, which are used in Finite Model Theory.

A simple application of our method allows us to obtain all the currently known space lower bounds for PCR, like the Pigeonhole Principle. But more importantly, using our approach in its full potentiality, we answer the open problem of proving space lower bounds in Polynomial Calculus and Polynomials Calculus with Resolution for the polynomial encoding of randomly chosen $k$-CNF formulas. Our method also applies to the well studied Graph Pigeonhole Principle which is a Pigeonhole principle over a constant (left) degree bipartite expander graph.

In the talk we will discuss a number of open problems which arise from our works which might be solved generalizing our approach

Joint Work with Ilario Bonacina.


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 never seems to 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

Programme archive for 1995 - summer 2008


Auxiliary Links

Fall schools

Colloquia lectures

Web connections

Proof complexity mailing list

Jech's library of preprints/reprints in set theory is available to students in our department

Baby logic seminar



9/5/10 Neil Thapen