Re: [isabelle] sledgehammer issue



A bug in E then. If you are ambitious, you could try to isolate the input and see if it yields a spurious proof when running E standalone. By coincidence, a new version was released yesterday, warning of a bug:

> E 1.9.1 "Sungma" is the latest version of the successful automated
> theorem prover.
> 
> Major user-visible improvements of E 1.9.1 are improved automatic
> modes, automatic detection of input format, major fixes to the
> watchlist mechanism (especially with respect to using it to provide
> hints for proof search) and a bug-fix for a rarely triggered, but
> nasty bug in clausification. We recommend all users of older versions
> to upgrade to E 1.9.1.
> 
> You can find the source distribution and additional information at
> the E website at
>               http://www.eprover.org

Larry

> On 1 Sep 2016, at 12:50, Peter Lammich <lammich at in.tum.de> wrote:
> 
> On Do, 2016-09-01 at 12:36 +0100, Lawrence Paulson wrote:
>> Sorry, what was that weird output? Do you mean this?
>> 
>>> 
>>> Try this: by metis (> 1.0 s, timed out).
> 
> This, in combination with the lemma "A=B", which is clearly not
> provable (A,B are just variables). 
> 
> This indicates e found a proof for something unprovable. Btw, there
> should be no "sorry"s in Main or "$AFP/Refine_Monadic/Refine_Monadic".





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