[Club2] talks by Steffen Smolka and Jasmin Blanchette-- Wed. May 15, 14:00, Turing

[Andrei Popescu]

Correction: The room for both talks is Turing (as indicated in the email subject), not Tarski (as was wrongly written in the body of the message).
Andrei 
--- On Sun, 5/12/13, Andrei Popescu <uuomul at yahoo.com> wrote:

From: Andrei Popescu <uuomul at yahoo.com>
Subject: [Club2] talks by Steffen Smolka and Jasmin Blanchette-- Wed. May 15, 14:00, Turing
To: "club2" <club2 at mailbroy.informatik.tu-muenchen.de>
Date: Sunday, May 12, 2013, 1:44 AM

Dear All,  
Next week, Steffen and Jasmin will talk about recent work on proof reconstruction with Sledgehammer.  
Best regards,   Andrei 
First talk: 
Steffen Smolka (joint work with Jasmin Blanchette)Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs=========================================================Wed. May 15, 14:00, Room 01.09.011 ("Alfred Tarski") 
Sledgehammer integrates external automatic theorem provers (ATPs) in the Isabelle/HOL proof assistant. To guard against bugs, ATP proofs must be reconstructed in Isabelle. Reconstructing complex proofs involves translating them to detailed Isabelle proof texts, using suitable proof methods to justify the inferences. This has been attempted before with little success, but we have addressed the main issues: Sledgehammer now transforms the proofs by contradiction into direct proofs; it reconstructs skolemization inferences; it provides the right amount of type annotations to ensure formulas are
 parsed correctly without overwhelming them with types; and it iteratively tests and compresses the output, resulting in simpler and faster proofs.
Second talk:
Jasmin BlanchetteRedirecting Proofs by Contradiction=========================================================Wed. May 15, 14:30, Room 01.09.011 ("Alfred Tarski") 
This paper presents an algorithm that redirects proofs by contradiction. The input is a refutation graph, as produced by an automatic theorem prover (e.g., E, SPASS, Vampire, Z3); the output is a direct proof expressed in natural deduction extended
 with case analyses and nested subproofs. The algorithm is implemented in Isabelle's Sledgehammer, where it enhances the legibility of machine-generated proofs.
-----Inline Attachment Follows-----

_______________________________________________
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/20130511/d9a8831a/attachment.html>