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

Much easier than having to enter "sledgehammer" manually and then wait.

Cheers,

Christoph

-- 
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.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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