Re: [isabelle] RC5: Short experience report



Dear Peter,

You wrote:

> Porting of lemmas using the word library was, as expected, more
> difficult. With the help of sledgehammer, which feels really powerful,
> I could force most lemmas through, even without a complete
> understanding or overview of the changes to Word.

If Sledgehammer feels more powerful, it's because it is. Makarius has repackaged many of the provers, using the latest versions; this was long overdue. On the Sledgehammer side, Martin has been doing the necessary integration, testing, and evaluation work. I'm very grateful to both! The integration of veriT as a reconstruction method, by Hans-Jörg, Mathias, and Martin, also helps reduce reconstruction failures by half, they claim in their draft [*]. Two more highlights:

1. We now communicate with E in a lambda-free HOL logic with support for currying and Booleans. That helps the success rate a lot. (E should get lambdas and HO unification this year.)

2. Sledgehammer now includes the Zipperposition higher-order prover that's developed largely by my team. It won last year CASC's higher-order division by a record margin. It's not enabled by default because we ran out of time to test it thoroughly, but you can add it to the Sledgehammer panel or "sledgehammer_params". It's good on HO things like p {x. q x | r x} ==> p {x. r x | q x} (which should be trivial but are "lost in translation" to FOL). Reconstruction remains a challenge, though.

Jasmin

[*] https://matryoshka-project.github.io/pubs/verit_isa_paper.pdf





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.