Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]
2013-10-07 22:05 Christoph LANGE:
> 2013-10-07 12:25 Jasmin Blanchette:
>> Auto Sledgehammer and Auto Nitpick run in a much reduced mode -- e.g. Sledgehammer just tries one prover for a few seconds instead of four for half a minute. (The manuals of these tools clarify which options are used.) I've enabled them months ago and don't really notice them any more than I notice Auto Quickcheck or Auto solve_direct. On the other hand, if you invoke "try" regularly, I can see that you don't need those tools.
> OK, thanks, you convinced me. I'll give Auto Sledgehammer a try.
Let me add that I'm finding Auto Sledgehammer very useful. You may
recall from our recent face-to-face conversation that I'm interested in
identifying ATP challenge problems, and that my approach is to look for
lemmas that look easy, can be proved with a few manual steps, but are
relatively hard for ATPs.
Because of the timeout setting, Auto Sledgehammer certainly won't help
me to identify those problems for which Sledgehammer needs a long time
to find an automated proof.
But for surprisingly many theorems, Auto Sledgehammer does find a proof
within the given time. Now, to measure the approximate time the actual
proof would take, it just remains that I make one or two (in case of
"sledgehammer [min]") clicks to see how long metis or smt would need for
Much easier than having to enter "sledgehammer" manually and then wait.
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
This archive was generated by a fusion of
Pipermail (Mailman edition) and