*To*: "Blanchette, J.C." <j.c.blanchette at vu.nl>*Subject*: Re: [isabelle] [Sledgehammer]*From*: Paulo Emílio de Vilhena <pevilhena2 at gmail.com>*Date*: Wed, 2 May 2018 11:37:33 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <43AB2085-F43D-46D0-9098-E85FBBC96F2C@vu.nl>*References*: <CACNZHBwVnPOgRRE1SaP+aA-Fvdf8-v-J30CJdeRtTMAurZLP2Q@mail.gmail.com> <43AB2085-F43D-46D0-9098-E85FBBC96F2C@vu.nl>

Dear Jasmin, Thank you for your reply. Indeed, Sledgehammer is of great help and even not succeeding it helps finding relevant facts as you mentioned. It just feels awkward that, for me, most of the time when this behavior appears is in very simple situations where the argument of performance wouldn't work at an intuitive level (I don't know the inner functioning of Sledgehammer, I'm simply based on the size of the one-line proof output as an user naively does). For example, there was a situation where all the provers outputed "by blast" and Isabelle wasn't able to finish the proof with this command. Another example, to make things concrete, was the situation of yesterday: if I write "using less" to give Sledgehammer a hint, all the provers but one proposed "empty by auto" as solution, which failed, and the last proposed "cycle_decomp.simps by auto" and also failed. What is bizarre is that if I don't write "using less" Sledgehammer manages to find solutions that work. I just repeated the experience today and the same behavior appeared. I also noticed that it was really fast to propose these faulty solutions so I don't think it is a performance problem (again, based on naive observations). To finish, I would like to suggest a modification to avoid this kind of situation, which is really annoying: I think it would be nice if Sledgehammer asks Isabelle to verify if the solution works instead of the user doing it by hand. If the solution doesn't work, it could just write an assertion as in the case of "Timed out". I think it would be less frustrating. Cheers, Paulo. On Wed, May 2, 2018 at 10:51 AM, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote: > Dear Paulo, > > > I found a problem with the usage of sledgehammer's proposed solutions: > > sometimes, even if it states "Proof found" and it manages to output an > > one-line proof without the "timed-out" assertion, the proposed solution > > does not work. This problem arrives to me with a certain frequency. > Today, > > for example, It happened two times in the same proof. > > > > I am available to help solving this problem. > > I'm afraid this is not a problem per se but the intended behavior. > Sledgehammer works in two steps: it looks for a solution using external > automatic theorem provers; then it attempts to reconstruct it using > Isabelle tactics. Sometimes, step 2 is too slow (or fails for other > reasons). Through the years, we've been looking at various ways to increase > the reconstruction success rate (see e.g. some of Sascha Böhme's or my > publicatons) but there's always more that could be done. Hopefully, by > inspecting the Sledgehammer output, you will come up with ideas on how to > carry out the proof. > > Cheers, > > Jasmin > >

**References**:**[isabelle] [Sledgehammer]***From:*Paulo Emílio de Vilhena

- Previous by Date: Re: [isabelle] Reversing simp rules
- Next by Date: Re: [isabelle] [Sledgehammer]
- Previous by Thread: [isabelle] [Sledgehammer]
- Next by Thread: Re: [isabelle] [Sledgehammer]
- Cl-isabelle-users May 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list