Re: [isabelle] Isabelle-RCX/Windows 64 bits (Sledgehammer)



Hi,

This problem seems to be solved in  Isabelle-RC4/Windows.
The lemma is solved quickly by Z3 (with and without try methods) in both
versions (32/64 bits).

I have no idea if the new status could be related to this:

> - more robust Sledgehammer preplay phase

Best!

On Sat, Feb 6, 2016 at 9:30 AM, Makarius <makarius at sketis.net> wrote:

> On Fri, 29 Jan 2016, Alfio Martini wrote:
>
> In Isabelle-RC2 and -RC1, Sledgehammer often fails to find a proof for the
>> notorious lemma about indexed sums (with
>> or without try methods):
>>
>> lemma aux: "m <= n+1 ==> setsum f {m..n + 1} =
>>    setsum f {m..n} + f (n + 1 :: int)"
>>
>> OS: Windows 10 with a Intel i5-5200U CPU @ 2.20GHz
>>
>
> I've briefly tried this with with Isabelle2015 and Isabelle2016-RC3 on
> Linux, and it fails consistently for all provers.
>
> It is unclear to me if one could expect this to work.  It depends a lot on
> HOL library contents, and these change frequently.
>
>
>         Makarius
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



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