skip to content
 

Semi-Automatic Asymptotics in Isabelle/HOL

Presented by: 
Manuel Eberl
Date: 
Wednesday 5th July 2017 - 13:30 to 14:30
Venue: 
INI Seminar Room 2
Abstract: 
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 video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons