Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sledgehammer: One-line proof reconstruction fa...

Email Gateway (Aug 22 2022 at 10:33):

From: Lars Hupel <hupel@in.tum.de>
Dear Jasmin,

I'll happily comply to your appeal :-)

I have attached a theory* which makes the Sledgehammer panel print

"cvc4": One-line proof reconstruction failed: by smt.
"spass": One-line proof reconstruction failed: by metis.

... and more of the same. However, the goal can be solved by both
'metis' and 'smt'.

Isabelle2014 correctly suggested 'metis'.

If I call 'sledgehammer [strict]' explicitly, the output for
'remote_vampire' changes to

"remote_vampire": Try this: by meson (6 ms).

... but 'meson' doesn't appear to solve it.

Cheers
Lars

• nevermind the error at the end of the proof, it is unrelated
  Scratch.thy

Email Gateway (Aug 22 2022 at 12:21):

From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,

I've found another instance of this problem in RC2. All of these work:

"cvc4": One-line proof reconstruction failed: by (smt subsetI).
"z3": Timed out.
"spass": One-line proof reconstruction failed: by (metis subset_code(1)).
"e": One-line proof reconstruction failed: by (metis subsetI).
"remote_vampire": One-line proof reconstruction failed: by (metis subsetI).

It's in a bigger theory context this time. I can send you my files if
you want.

Cheers
Lars

Last updated: Nov 21 2024 at 12:39 UTC