[Club2] Wed. the 21st, talk by Daniel Wand (the usual place and time)

[Andrei Popescu]

Hello, 
Daniel Wand will be visiting us next next week, and will give a talk on the integration of SPASS with Isabelle.  
Cheers,   Andrei 

More SPASS with IsabelleDaniel Wand(joint work with Jasmin Blanchette, Andrei Popescu, and Christoph Weidenbach)====================================================Wed. Mar. 21, 14:00, MI 00.09.055 ("Alan Turing")
Sledgehammer integrates automatic theorem provers to discharge interactive proofobligations. This talk presents a tighter integration of the superpositionprover SPASS, to increase Sledgehammer's success rate. The main enhancements are native support for rigid sorts (simple types) in SPASS, simplification thathonors the orientation of Isabelle "simp" rules, and a pair of clause-selectionstrategies targeted at large lemma libraries. The usefulness of this integrationis confirmed by an evaluation on a vast benchmark suite and by a case study

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