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.
 
> Regards,
> Jasmin
 
Thank you for the answer!
Best,
Marco

PS: Please bear with the horrible quoting, my webmail interface sucks seriously.





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