[Club2] talk by Steffen Smolka: this Friday, July 19, 14:00, Room Turing (00.09.38)

[Andrei Popescu]

Dear All, 

This talk is 95% identical to the rehearsal Steffen did two months ago, so if you have seen the previous talk, you will probably want to skip this one.


Cheers, 
   Andrei

Steffen Smolka
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
=========================================================
Friday July 19, 14:00, Room Turing (00.09.38)

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