Re: [isabelle] sledgehammer issue



Hi Larry,

I very much hope that the AFP editors have ensured that âsorry" is not used in AFP entries (which is the only imported thing in Peterâs example next to Main).

Dmitriy

> On 01 Sep 2016, at 13:36, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> 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.