Re: [isabelle] sledgehammer issue



On Do, 2016-09-01 at 13:03 +0100, Lawrence Paulson wrote:
> A bug in E then. 

If I understand it correctly, the bug could also be in the translation
from HOL to E, which is done by sledgehammer.

--
 Peter


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