BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//SECURITY & APPLIED LOGIC - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://sal.cs.unibuc.ro
X-WR-CALDESC:Events for SECURITY & APPLIED LOGIC
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Bucharest
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20200329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20201025T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20210328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20211031T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20220327T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20221030T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20210304T100000
DTEND;TZID=Europe/Bucharest:20210304T120000
DTSTAMP:20260423T063159
CREATED:20210303T165215Z
LAST-MODIFIED:20210317T165240Z
UID:691-1614852000-1614859200@sal.cs.unibuc.ro
SUMMARY:Unwinding of proofs
DESCRIPTION:Title: Unwinding of proofs \nSpeaker: Pedro Pinto (TU Darmstadt)  \n\nAbstract: \nThe 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?”\n \n \nThis 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.\n\nIn this talk\, we set out to give a brief introduction to the proof mining program\, focusing on the following points: \n\n\n\nfunctional interpretations in an introductory way;\nthe bounded functional interpretation [3\,4];\na concrete translation example: the metric projection argument.\n\nWe finish with a brief discussion of some recent results [5\,6]. \nReferences: \n\n[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg\, 2008.\n[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.\n[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic\, 135:73-112\, 2005.\n[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic\, 157:122-129\, 2009.\n[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA]\, 2021.\n[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA]\, 2021.\n  \n\n  \nReferences:
URL:https://sal.cs.unibuc.ro/event/unwinding-of-proofs/
CATEGORIES:Logic Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20210311T100000
DTEND;TZID=Europe/Bucharest:20210311T120000
DTSTAMP:20260423T063159
CREATED:20210310T154158Z
LAST-MODIFIED:20210317T154308Z
UID:683-1615456800-1615464000@sal.cs.unibuc.ro
SUMMARY:Exponential Diophantine equations over ℚ 
DESCRIPTION:Title:  Exponential Diophantine equations over ℚ \nSpeaker: Mihai Prunescu (University of Bucharest & IMAR) \n\nAbstract: \n\nIn 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. \nReferences: \n\n[1] M. Prunescu\, The exponential Diophantine problem for ℚ. The Journal of Symbolic Logic\, Volume 85\, Issue 2\, 671–672\, 2020.
URL:https://sal.cs.unibuc.ro/event/exponential-diophantine-equations-over-%e2%84%9a/
CATEGORIES:Logic Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20210318T100000
DTEND;TZID=Europe/Bucharest:20210318T120000
DTSTAMP:20260423T063159
CREATED:20210317T151527Z
LAST-MODIFIED:20210317T204833Z
UID:681-1616061600-1616068800@sal.cs.unibuc.ro
SUMMARY:A proof mining case study on the unit interval
DESCRIPTION:Title: A proof mining case study on the unit interval \nSpeaker: Andrei Sipoș (University of Bucharest & IMAR) \n\nAbstract:  \n\nIn 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.\nThe 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.\nReferences: \n\n\n[1] D. Borwein\, J. Borwein\, Fixed point iterations for real functions. J. Math. Anal. Appl. 157\, no. 1\, 112–126\, 1991.\n[2] A. Sipoș\, Rates of metastability for iterations on the unit interval. arXiv:2008.03934 [math.CA]\, 2020.
URL:https://sal.cs.unibuc.ro/event/a-proof-mining-case-study-on-the-unit-interval/
CATEGORIES:Logic Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20210325T100000
DTEND;TZID=Europe/Bucharest:20210325T120000
DTSTAMP:20260423T063159
CREATED:20210322T160836Z
LAST-MODIFIED:20210323T090618Z
UID:697-1616666400-1616673600@sal.cs.unibuc.ro
SUMMARY:Regular matching problems for infinite trees
DESCRIPTION:Title: Regular matching problems for infinite trees \nSpeaker: Mircea Marin (West University of Timișoara) \n\nAbstract:  \nWe 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.\nThis is joint work with Carlos Camino\, Volker Diekert\, Besik Dundua and Géraud Sénizergues. \n\nReferences: \n[1] C. Camino\, V. Diekert\, B. Dundua\, M. Marin\, G. Sénizergues\, Regular matching problems for infinite trees. arXiv:2004.09926 [cs.FL]\, 2021.
URL:https://sal.cs.unibuc.ro/event/regular-matching-problems-for-infinite-trees/
CATEGORIES:Logic Seminar
END:VEVENT
END:VCALENDAR