Re: [isabelle] sledgehammer issue



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

--
 Peter


> It looks normal to me. Sometimes proofs time out.
> 
> You can also get a warning if sledgehammer proves the goal without
> referring to the goal itself (specifically, its negation). This
> indicates that your assumptions are themselves inconsistent. Possibly
> too much use of"sorry". We all do it.
> 
> Larry
> 
> > 
> > On 31 Aug 2016, at 16:08, Peter Lammich <lammich at in.tum.de> wrote:
> > 
> > Hi Jasmin,
> > 
> > In Isabelle2016, I get the following weird sledgehammer output.
> > 
> > Sometimes, (I could not reproduce with small example), I also get
> > the
> > message that e derived false from these facts, and that I should
> > report
> > this as a "bug" in sledgehammer.
> > 
> > 
> > theory Scratch
> > imports MainÂ
> > Â "$AFP/Refine_Monadic/Refine_Monadic"
> > begin
> > 
> > 
> > Â lemma "A=B"
> > ÂÂÂÂusing ASSERT_simps(1) inres_simps(3) pw_ASSERT(2)
> > ÂÂÂÂsledgehammer [provers = e]
> > (* Sledgehammering...Â
> > "e": Try this: by metis (> 1.0 s, timed out).
> > *)
> > Â oopsÂÂÂÂ
> > 
> > 
> > --
> > Â Peter
> > 
> 




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