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



Dear Users,

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


However, the Snapshot version of 23-12 always finds  (very quickly) a proof
with Z3 (with and without try methods).

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