Email Gateway (Aug 22 2022 at 10:16): Email Gateway (Aug 22 2022 at 10:16):From: Bohua Zhan <bzhan@mit.edu>
When I tried sledgehammer on the following theorem:
theorem Max_ge': "finite A ⟹ x > Max A ⟹ ¬(x ∈ A)"
The cvc4 output is:
Try this: using leD by auto (6 ms).
However, the command does not work. It probably should be
using Max_ge leD by auto
Best,
Bohua
Email Gateway (Aug 22 2022 at 10:16):From: Alfio Martini <alfio.martini@acm.org>
Hi Bohua,
Using 2015/Windows with try methods I get with cvc4:
using Max_ge not_le by blast
Without try methods: by (metis Max_ge leD)
Best!
Best!
Email Gateway (Aug 22 2022 at 10:17):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Bohua,
Thank you for this report. This issue is already fixed in the repository version (since 28 May 2015, right after the release). As a workaround, you can pass the option “dont_minimize” to Sledgehammer, e.g.
sledgehammer [dont_minimize]
when this arises.
Regards,
Jasmin
Email Gateway (Aug 22 2022 at 10:17):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Bohua,
Thank you for this report. This issue is already fixed in the repository version (since 28 May 2015, right after the release). As a workaround, you can pass the option “dont_minimize” to Sledgehammer, e.g.
sledgehammer [dont_minimize]
when this arises.
Regards,
Jasmin
Last updated: Apr 25 2024 at 16:19 UTC