skip to content
 

Proof Automation - Automation in Isabelle's Analysis

Presented by: 
Johannes Hölzl
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.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons