Master's program at the Faculty of Mathematics and Computer Science, University of Bucharest
Speaker: Marian Calborean (University of Bucharest) Abstract: The Sorites paradox is usually studied as a propositional paradox. However, the general form of the Sorites is second-order, with three main features. It doesn’t contain any arbitrary parameters. It can be used to generate the propositional Sorites by appropriate replacement of the second-order premise with arbitrary clauses. …
Speaker: Ulrich Kohlenbach (Technische Universität Darmstadt) Title: A quantitative analysis of the “Lion-Man” game Abstract: We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an ε-capture criterion. We prove that in uniformly convex bounded domains the lion always …
POSTPONED UNTIL FURTHER NOTICE. Speaker: Alexandru Dragomir (University of Bucharest) Title: Protocols in Dynamic Epistemic Logic Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (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: 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) …