[Club2] Correction: Daniel's talk this Wednesday (the 21st) is at 15:00, not 14:00

[Andrei Popescu]

Regards,    Andrei
More SPASS with IsabelleDaniel Wand(joint work with Jasmin Blanchette, Andrei Popescu, and Christoph Weidenbach)====================================================Wed. Mar. 21, 15:00, MI 00.09.055 ("Alan Turing")
Sledgehammer integrates automatic theorem provers to discharge interactive proof obligations. 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 that honors the orientation of Isabelle "simp" rules, and a pair of clause-selection strategies targeted at large lemma libraries. The usefulness of this integration is confirmed by an evaluation on a vast benchmark suite and by a case study. 
--- On Fri, 3/16/12, Andrei Popescu <uuomul at yahoo.com> wrote:

From: Andrei Popescu <uuomul at yahoo.com>
Subject: 2 club2 talks next week on Wednesday the 21st
To: club2 at mailbroy.informatik.tu-muenchen.de
Date: Friday, March 16, 2012, 7:06 PM

Dear All,  
This week, we have a talk by Johannes on a formalization of pCTL model checking and one by our visitor Daniel Wand the integration of SPASS with Isabelle.  
Best regards,   Andrei 

Johannes Hölzl (joint work with Tobias Nipkow)Verifying pCTL Model Checking====================================================Wed. Mar. 21, 10:00, MI 00.09.055 ("Alan Turing")
Probabilistic model checkers like PRISM check the satisfiability ofprobabilistic CTL (pCTL) formulas against discrete-time Markov chains. Weprove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.

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 proof obligations. 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 that honors the orientation of Isabelle "simp" rules, and a pair of clause-selection strategies targeted at large lemma libraries. The usefulness of this integration is 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/20120319/c4ffafc1/attachment.html>