Kernelization, Proof Complexity and Social Choice

Title: Kernelization, Proof Complexity and Social Choice

Speaker: Gabriel Istrate (West University of Timișoara)


We display an application of the notions of kernelization and data reduction from parameterized complexity to proof complexity: Specifically, we show that the existence of data reduction rules for a parameterized problem having (a) a small-length reduction chain, and (b) small-size (extended) Frege proofs certifying the soundness of reduction steps implies the existence of subexponential size (extended) Frege proofs for propositional formalizations of the given problem. We apply our result to infer the existence of subexponential Frege and extended Frege proofs for a variety of problems. Improving earlier results of Aisenberg et al. (ICALP 2015), we show that propositional formulas expressing (a stronger form of) the Kneser-Lovasz Theorem have polynomial size Frege proofs for each constant value of the parameter k. Previously only quasipolynomial bounds were known (and only for the ordinary Kneser-Lovasz Theorem). Another notable application of our framework is to impossibility results in computational social choice: we show that, for any fixed number of agents, propositional translations of the Arrow and Gibbard-Satterthwaite impossibility theorems have subexponential size Frege proofs.

This is joint work with Cosmin Bonchiș and Adrian Crăciun.

An Introduction to Protocols in Dynamic Epistemic Logic

Title: An Introduction to Protocols in Dynamic Epistemic Logic

Speaker: Alexandru Dragomir (University of Bucharest)


Dynamic epistemic logics are useful in reasoning about knowledge and acts of learning, seen as epistemic actions. However, not all epistemic actions are allowed to be executed in an initial epistemic model, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to two accounts of protocols in DEL: Hoshi’s [1], and Wang’s [2].


[1] T. Hoshi, Epistemic dynamics and protocol information. PhD thesis, Stanford, CA, USA, 2009.
[2] Y. Wang, Epistemic Modelling and Protocol Dynamics. PhD thesis, University of Amsterdam, 2010.

Regular matching problems for infinite trees

Title: Regular matching problems for infinite trees

Speaker: Mircea Marin (West University of Timișoara)


We study the matching problem “∃σ:σ(L)⊆R?” where L and R are regular tree languages over finite ranked alphabets X and Σ respectively, and σ is a substitution such that σ(x) is a set of trees in T(Σ∪H)∖H for all x∈X. Here, H denotes a set of holes which are used to define a concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook Regular algebra and finite machines and showed that if L and R are regular, then the problem “∃σ:∀x∈X:σ(x)≠∅∧σ(L)⊆R?” is decidable. Moreover, there are only finitely many maximal solutions, which are regular and effectively computable. We extend Conway’s results when L and R are regular languages of finite and infinite trees, and language substitution is applied inside-out. We show that if L⊆T(X) and R⊆T(Σ) are regular tree languages then the problem “∃σ∀x∈X:σ(x)≠∅∧σio(L)⊆R?” is decidable. Moreover, there are only finitely many maximal solutions, which are regular and effectively computable. The corresponding question for the outside-in extension σoi remains open, even in the restricted setting of finite trees. Our main result is the decidability of “∃σ:σio(L)⊆R?” if R is regular and L belongs to a class of tree languages closed under intersection with regular sets. Such a special case pops up if L is context-free.
This is joint work with Carlos Camino, Volker Diekert, Besik Dundua and Géraud Sénizergues.


[1] C. Camino, V. Diekert, B. Dundua, M. Marin, G. Sénizergues, Regular matching problems for infinite trees. arXiv:2004.09926 [cs.FL], 2021.

A proof mining case study on the unit interval

Title: A proof mining case study on the unit interval

Speaker: Andrei Sipoș (University of Bucharest & IMAR)


In 1991, Borwein and Borwein proved [1] the following: if L>0, f : [0,1] → [0,1] is L-Lipschitz, (xn), (tn) ⊆ [0,1] are such that for all n, xn+1=(1-tn)xn+tnf(xn) and there is a δ>0 such that for all n, tn≤(2-δ)/(L+1), then the sequence (xn) converges.
The relevant fact here is that the main argument used in their proof is of a kind that hasn’t been analyzed yet from the point of view of proof mining, and thus it may serve as an illustrative new case study. We shall present our work [2] on the proof, showing how to extract a uniform and computable rate of metastability for the above family of sequences.


[1] D. Borwein, J. Borwein, Fixed point iterations for real functions. J. Math. Anal. Appl. 157, no. 1, 112–126, 1991.
[2] A. Sipoș, Rates of metastability for iterations on the unit interval. arXiv:2008.03934 [math.CA], 2020.

Exponential Diophantine equations over ℚ 

Title:  Exponential Diophantine equations over ℚ

Speaker: Mihai Prunescu (University of Bucharest & IMAR)


In a previous exposition [1] we have seen that the solvability over ℚ is undecidable for systems of exponential Diophantine equations. We now show that the solvability of individual exponential Diophantine equations is also undecidable, and that this happens as well for some narrower families of exponential Diophantine equations.


[1] M. Prunescu, The exponential Diophantine problem for ℚ. The Journal of Symbolic Logic, Volume 85, Issue 2, 671–672, 2020.

Unbreakable Romania

We are pleased to support UNbreakable Romania – the national competition organised for students in the country preparing for a career in cybersecurity.

  1. The preparation stage will start on April 1 when the registered participants will have at their disposal theoretical and practical resources that will allow them to become familiar with the format and methodology of the contest.

2. The individual contest will take place between May 14-16.

3. The team competition will take place on June 4-6.

At the end of the season, there will be a national #ROEduCyberSkills ranking that will provide an overview of cybersecurity performance in Romania.

Registration is free and is available on the official website:

Unwinding of proofs

Title: Unwinding of proofs

Speaker: Pedro Pinto (TU Darmstadt)


The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: “What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?”

This research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles.

In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:

  • functional interpretations in an introductory way;
  • the bounded functional interpretation [3,4];
  • a concrete translation example: the metric projection argument.

We finish with a brief discussion of some recent results [5,6].


[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.
[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor, Proceedings of the International Congress of Mathematicians – Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61–82. World Sci. Publ., Hackensack, NJ, 2019.
[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.




Formalizing Gödel’s System T in Lean

Title: Formalizing Gödel’s System T in Lean

Speaker: Horațiu Cheval (University of Bucharest)


In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant.


[1] mathlib Community, The Lean Mathematical Library, 2019.

Hack The Box University 2020 – Qualifier Round

The students of the Faculty of Mathematics and Computer Science Dragoș Albastroiu (3rd-year, CTI) – captain, Robert Dobre (3rd-year, Computer Science), Mihail Feraru (2nd-year, Computer Science) and Andrei Ciobanu (2nd-year master, Security and Applied Logic) represented the University of Bucharest at the Hack The Box University 2020 Qualifier Round, which took place in November, 19th-22nd, online. In the competition participated teams from universities all around the world, and the team of the University of Bucharest ranked among the best, becoming eligible to remain in the competition.