Re: [isabelle] [Sledgehammer]



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
>
>



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