[Club2] 2 talks by Jasmin Blanchette, Wed. the 14th and Thu. the 15th, at 2PM in Turing room

[Andrei Popescu]

Dear All, 
The coming week we have two talks by Jasmin.  Details follow.
Cheers,    Andrei 

Jasmin Blanchette (joint work with Andrei Paskevich)TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism====================================================Wed. Mar. 14, 14:00, MI 00.09.055 ("Alan Turing")
The TPTP World is a well-established infrastructure for automatic theoremprovers. It defines several concrete syntaxes, notably a typed first-order form(TFF0), that have become de facto standards. This talk introduces the TFF1format, an extension of TFF0 with rank-1 polymorphism. It presents its syntax,typing rules, and semantics, as well as a translation to TFF0. The format isdesigned to be easy to process by existing reasoning tools that support ML-stylepolymorphism. It opens the door to useful middleware, such as monomorphizers andother translation tools. Ultimately, the hope is that TFF1 will be implementedin popular automatic theorem provers.

Jasmin BlanchetteSharing the Burden of (Dis)proof with Nitpick, Quickcheck, and Sledgehammer====================================================Thu. Mar. 15, 14:00, MI 00.09.055 ("Alan Turing")
Isabelle/HOL owes much of its success to its ease of use and powerfulautomation. Much of the automation is performed by external tools: Themetaprover Sledgehammer relies on resolution provers and SMT solvers for itsproof search, the counterexample generator Quickcheck uses the ML compiler as a fast evaluator for ground formulas, and its rival Nitpick is based on the model finder Kodkod, which performs a reduction to SAT. This talk will explain how these tools work under the hood.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20120309/d9482eb8/attachment.html>