Re: [isabelle] smt method avoidance
> 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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and