skip to content
 

Proof Automation - Automation in Isabelle's Analysis

Presented by: 
Johannes Hölzl Carnegie Mellon University
Date: 
Monday 3rd July 2017 - 15:30 to 16:30
Venue: 
INI Seminar Room 2
Abstract: 
It is essential in Isabelle's analysis library has special support to handle continuity, measurability, and differentiability, etc. This is quite different to *big* automation like SMT or what Sledgehammer does.



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