Re: [isabelle] RC5: Short experience report



These are great developments! But already, for some years now, sledgehammer has been good enough to help people prove things they didn’t really understand. That’s how I managed to port tens of thousands of lines of incomprehensible HOL Light proofs. It’s also good at discovering contradictions when people have been using “sorry” a little too freely.

It’s not fanciful to foresee a “self-healing” capability for proof developments: where you update a definition and the system would identify and automatically repair proofs that broke as a result. Also in the not-too-distant future might be source to source translations of structured proofs from one proof assistant to another, with high-level proofs in the target system being generated automatically using the source proofs as hints (as opposed to the current practice of emulating one formalism within another).

Larry

> On 15 Feb 2021, at 09:16, Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk> 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.





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