Re: [isabelle] sledgehammer issue



Sorry, what was that weird output? Do you mean this?

> Try this: by metis (> 1.0 s, timed out).

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.