[Club2] Talk by Cezary Kaliszyk: Wed. Febr. 27, Turing

[Andrei Popescu]

Dear All,  
Next week we have a talk by Cezary on HOL Light automation via external ATPs.  
Best regards,   Andrei 
Cezary KaliszykLearning-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 andpremise selection methods on HOL Light. We will present thearchitecture of the system focusing on the design decisionsthat made it different from existing `hammer' tools. The premiseselection mechanisms are evaluated on the Flyspeck developmentin various scenarios, including a bootstrapping scenarioemulating the development of Flyspeck from axioms to the lasttheorem, each time using only the previous theorems and proofs.It is shown that 39\% of the 14185 %\Flyspeck theorems could beproved in a push-button mode (without any high-level adviceand user interaction) in 30 seconds of real time. This isachieved by fourteen different combinations of ATP systems andpremise selection methods based on machine learning from previousproofs in the corpora.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130219/b3d897b0/attachment.html>