Re: [isabelle] sledgehammer, smt and metis



Hi Marco,

> I am currently removing smt from a lot of Isabelle proofs, and I noticed, strictly empirically, what follows.
> 
> A number of such proofs kept working by merely (and manually) replacing "by smt" (or "by smt2") with something like "by (metis(no_types,lifting))", (or metis with other combinations of options (e.g., hide_lams, mono_tags, etc...)).
> 
> I think that it would be nice, given the licensing issues, that sledgehammer would suggest these alternatives, rather than (or at least in addition to) "by smt".

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. (Those that are tried can be seen by passing "[verbose]" or "[debug]".)

> However, I couldn't find a way of influencing s/h behaviour in such a way, by reading s/h manual. 
> I tried with smt_proofs=false, to no avail.

Well setting "smt_proofs=false" surely must have changed something, namely that you never get any "smt(2)" proofs, right? If not, that's really a bug, and I would like you to send me an example that reproduces the problem.

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.

Regards,

Jasmin





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