skip to content

Proof Automation - Automation in Isabelle's Analysis

Presented by: 
Johannes Hölzl
Monday 3rd July 2017 - 15:30 to 16:30
INI Seminar Room 2
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