Re: [isabelle] smt method avoidance



Dear Omar,

> 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.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.