Email Gateway (Aug 22 2022 at 13:23): Email Gateway (Aug 22 2022 at 13:23):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Dear list,
when I'm trying to use sledgehammer it give me smt method for proof my
lemmas and this repeated many times. Because using smt is not allowed by
Submission Guidelines, also I don't prefer using it, so there is such a way
to avoid smt suggestion by sledgehammer?
Regards
Omar
Email Gateway (Aug 22 2022 at 13:23):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Omar,
Which version of Isabelle are you using? With a recent version, whenever Sledgehammer produces an "smt" proof, it also tries to generate a more detailed proof. Unfortunately, this will not work for CVC4, and you need a bit of manual work if you want to transform a proof found by CVC4 in something acceptable. For example, if you get
by (smt foo bar)
from Sledgehammer, you can try again with
sledgehammer [prover = z3] (foo bar)
and hopefully you will get an alternative proof.
If you never ever want to see the "smt" proofs, you can also set the option "smt_proofs = false". E.g.
sledgehammer_params [smt_proofs = false]
See the documentation ("isabelle doc sledgehammer") for details.
Cheers,
Jasmin
Last updated: Apr 19 2024 at 20:15 UTC