Title: Formalizing Gödel's System T in Lean Speaker: Horațiu Cheval (University of Bucharest) Abstract: 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 …

Title: Unwinding of proofs Speaker: Pedro Pinto (TU Darmstadt) Abstract: 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 …

Title:  Exponential Diophantine equations over ℚ Speaker: Mihai Prunescu (University of Bucharest & IMAR) Abstract: In a previous exposition 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 …

Title: A proof mining case study on the unit interval Speaker: Andrei Sipoș (University of Bucharest & IMAR) Abstract:  In 1991, Borwein and Borwein proved the following: if L>0, f : → is L-Lipschitz, (xn), (tn) ⊆ 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 …

Title: Regular matching problems for infinite trees Speaker: Mircea Marin (West University of Timișoara) Abstract: 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 …

Title: An Introduction to Protocols in Dynamic Epistemic Logic Speaker: Alexandru Dragomir (University of Bucharest) Abstract: 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 …

Title: Kernelization, Proof Complexity and Social Choice Speaker: Gabriel Istrate (West University of Timișoara) Abstract: 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) …