Re: [isabelle] Sledgehammer 2015 oddity



Hi Thomas,

> Short summary: in Isabelle 2015 all sledgehammer provers recommend "by
> auto" to solve a goal that can be solved trivially but not by auto.

Thanks for the example. I am very much dependent on user-provided examples for debugging this feature.

Here, the problem is that Sledgehammer noticed that âusing foo bar by autoâ solved the problem, then its minimized kicked in and noticed that âfooâ and âbarâ were in the simpset and simply took them away. In most cases, this is a useful, time- and CPU-saving strategy, but in your example taking out âfoo" turned out to be deadly. See change 7d278b0617d3 â unfortunately too late for Isabelle2015. The change joins 2c468c062589 and 533f6cfc04c0, done earlier this year.

Appeal to the list: Please let me know if you run into other examples where either Sledgehammer finds a proof that doesnât work and it claims it does or vice versa. The issues are normally easy to track down and address if you can provide me with an example that reproduces the problem.

Jasmin





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