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

[Andrei Popescu]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130511/78b691e7/attachment.html>