[Club2] Reminder: Talk by Cezary Kaliszyk at 14:00

[Jasmin Christian Blanchette]

Anfang der weitergeleiteten Nachricht:

> Von: Andrei Popescu <uuomul at yahoo.com>
> Betreff: [Club2] Talk by Cezary Kaliszyk: Wed. Febr. 27, Turing
> Datum: 19. Februar 2013 16:38:44 MEZ
> An: club2 <club2 at mailbroy.informatik.tu-muenchen.de>
> Kopie: Cezary kaliszyc <kaliszyc at in.tum.de>
> 
> Dear All,  
> 
> Next week we have a talk by Cezary on HOL Light automation via external ATPs.  
> 
> Best regards, 
>   Andrei 
> 
> Cezary Kaliszyk
> Learning-Assisted Automated Reasoning with Flyspeck
> ====================================================
> Wed. Febr. 27, 14:00, Room 00.09.055 ("Alan Turing") 
> 
> This talk reports our experiments with using external ATP and
> premise selection methods on HOL Light. We will present the
> architecture of the system focusing on the design decisions
> that made it different from existing `hammer' tools. The premise
> selection mechanisms are evaluated on the Flyspeck development
> in various scenarios, including a bootstrapping scenario
> emulating the development of Flyspeck from axioms to the last
> theorem, each time using only the previous theorems and proofs.
> It is shown that 39\% of the 14185 %\Flyspeck theorems could be
> proved in a push-button mode (without any high-level advice
> and user interaction) in 30 seconds of real time. This is
> achieved by fourteen different combinations of ATP systems and
> premise selection methods based on machine learning from previous
> proofs in the corpora.
> _______________________________________________
> Club2 mailing list
> List page: https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/club2
> Webpage with calendar: http://www21.in.tum.de/club2

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130227/e7a4646a/attachment.html>