[Club2] talk by Moa Johansson -- Wednesday May 14, 15:00, Turing (00.09.38)

[Andrei Popescu]

Dear All,  

Moa Johansson from Koen Claessen's team in Gothenburg will visit us 
May 12 to May 16 and will give the following talk, based on her accepted CICM 2014 paper.
 
Cheers, 
  Andrei  


Hipster: Integrating Theory Exploration in a Proof Assistant
Moa Johansson
======================================================================
Wed., May 14, 15:00, Room: Turing (00.09.38)

Hipster is a system integrating theory exploration with the proof assistant Isabelle. 
Theory exploration is a technique for automatically discovering new interesting lemmas in a given 
theory development. Hipster can be used in two main modes. The first is exploratory mode, used for 
automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. 
The second is proof mode, used in a particular proof attempt, trying to discover the missing lemmas which would 
allow the current goal to be proved. Hipster’s proof mode complements and boosts existing proof automation techniques 
that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. I will 
present a demo of Hipster showing both modes of use.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140511/dc2a9ae7/attachment.html>