[Club2] PxTP/PSATTT talk rehearsal Wed 13 Jul @ 14:00 (Turing)

[Jasmin Blanchette]

Hallo zusammen,

I'll momentarily replace Mr. Popescu (who appears to be busy) and announce the next Club2 talk. I fully realize I am trying your patience with my repetitive talks, and will not hold it against you if you do not show up. The talk is today (Wednesday) from 14:00 to 15:00 in Turing.

Jasmin


Proof Search and Proof Reconstruction in Sledgehammer
PxTP/PSATT 2011 at CADE-23

The main difficulty with Sledgehammer's proof search is to encode type information efficiently, including polymorphism. For SMT solvers, we monomorphize the problem and map the resulting ground types to SMT-LIB sorts. For resolution provers, we experimented with a menagerie of type encodings and selected the most appropriate encoding for each prover, sacrificing soundness for efficiency in some cases.

For proof reconstruction, several schemes are supported: (1) SMT solvers can be trusted and used as oracles; (2) Z3 proofs are replayed step by step and can be stored as certificates to speed up replay; (3) from resolution proofs, Sledgehammer extracts the used lemmas and attempts to re-find the proofs in Isabelle; (4) experimentally, we also implemented structured Isabelle proof construction from resolution proofs. This last scheme is the most promising, and we are currently working on improving the readability of the proofs and add support for SMT proofs.