Re: [isabelle] sledgehammer, smt and metis
Ven 21/11/14, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> ha scritto:
> Hi Marco,
> By default, "smt" calls are only proposed if all else failed. More precisely,
> whenever Sledgehammer gives a "by (smt ...)",
it's because the variations of "metis" failed
or timed out. So if you successfully replaced "by
smt" by something like "by (metis (no_types,
lifting) ...)", it's either because it timed out or
> because the specific combination of "metis" options wasn't tried.
The specific combinations usually take less then a second once I manually enter them, hence I think it's the second case.
Given that, I find that it would be nice if sledgehammer would try those combinations, too.
Of course I have no clue about whether this is technically possible.
> (Those that are tried can be seen by passing "[verbose]" or "[debug]".)
I think this is a useful suggestion; however, at the moment I cannot try it.
> Well setting "smt_proofs=false" surely must have changed
> something, namely that you never get any "smt(2)"
> proofs, right?
Exactly, no bugs. I just hoped that using that setting would have helped emerging alternative metis combinations.
> Already in
> Isabelle2014, Sledgehammer should attempt to generate Isar
proofs (cf. "isar_proofs" option in the manual)
for Z3 when offering "by (smt2 ...)". This support
has been improved further in the repository version and
should help you produce "smt(2)"-free proofs, fit
> for the AFP.
Yes, indeed a couple of Isar proofs generated by SH were readable, and I happily used them.
It was a very nice sensation, by the way :)
I mean, reading a proof that nobody wrote.
Thank you for the answer!
PS: Please bear with the horrible quoting, my webmail interface sucks seriously.
This archive was generated by a fusion of
Pipermail (Mailman edition) and