BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Semi-Automatic Asymptotics in Isabelle/HOL - Manuel Eberl (Technis
 che Universität München)
DTSTART:20170705T123000Z
DTEND:20170705T133000Z
UID:TALK73451@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Computer Algebra Systems can easily compute limits and<br>asym
 ptotic expansions of complicated real functions\; interactive theorem<br>p
 rovers\, on the other hand\, provide very little support for such problems
  and<br>proving asymptotic properties of a function often involves long an
 d tedious<br>manual proofs.<br><br>&nbsp\;<br><br>In this talk\, I will pr
 esent my work about bringing<br>automation for real-valued asymptotics to 
 Isabelle/HOL using multiseries<br>expansions.<br><br>This yields a procedu
 re to automatically prove limits and<br>&lsquo\;Big-O&#39\;<br><br>estimat
 es of real-valued functions similarly to computer<br>algebra systems like 
 Mathematica and Maple &ndash\; but while proving every step of<br>the proc
 ess correct.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR