Email Gateway (Aug 22 2022 at 12:22): Email Gateway (Aug 22 2022 at 12:22):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 22 2022 at 12:50):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 12:50):From: Alfio Martini <alfio.martini@acm.org>
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!
Last updated: Apr 20 2024 at 12:26 UTC