Ponente: Manuel Eberl (Technische Universität München)
Lugar: Seminario Mirian Andrés (Edificio CCT)
Hora: jueves 16 de noviembre, 11:00
Resumen: Computer Algebra Systems can easily compute limits and asymptotic expansions of complicated real functions; interactive theorem provers, on the other hand, provide very little support for such problems and proving asymptotic properties of a function often involves long and tedious manual proofs. In this talk, I will present my work about bringing automation for real-valued asymptotics to Isabelle/HOL using multiseries expansions. This yields a procedure to automatically prove limits and ‘Big-O’ estimates of real-valued functions similarly to computer algebra systems like Mathematica and Maple – but while proving every step of the process correct.
The slides of the talk are available in the following link.