Email Gateway (Aug 19 2022 at 12:18): Email Gateway (Aug 19 2022 at 12:18):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-04 10:42 Makarius:
With the implicit "auto sledgehammer" and explicit "slegdehammer panel"
you normally don't put query commands in the buffer anymore,
Could you once more explain what "auto sledgehammer" is? I know
entering "sledgehammer" (or "try", which I use in practice most of the
time) into the buffer, and I know the new sledgehammer panel, and I
didn't see anything else in the NEWS file.
Cheers, and thanks in advance,
Christoph
Email Gateway (Aug 19 2022 at 12:18):From: Makarius <makarius@sketis.net>
The NEWS file has this very terse entry:
* Support for automatic tools in HOL, which try to prove or disprove
toplevel theorem statements.
The sledgehammer manual then has this:
For Isabelle/jEdit users, Sledgehammer provides an automatic mode that
can be enabled via the “Auto Sledgehammer” option under “Plugins > Plugin
Options > Isabelle > General.” In this mode, Sledgehammer is run on
every newly entered theorem.
The Plugin Options have more "automatically tried tools" in store, most of
them off by default.
"Auto methods" is the same mechanism as 'try0', but it tends to suck up a
lot of CPU resources, since the classic Isabelle proof tools easily get
into non-terminating situations without instrumentation by facts that are
properly classified as simp/intro/elim/dest/iff.
I should probably say a few more general things about the "auto" tools in
the still empty slots of the jedit manual, pointing to the other manuals,
too.
We also need more practical experience with such options.
Makarius
Email Gateway (Aug 19 2022 at 12:18):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-04 15:13 Makarius:
Thanks for pointing out! Very interesting to know, but (now take this
as feedback from a naive end-user) I probably won't enable all these
automations seems. Auto quickcheck and solve_direct are very nice, but
I wouldn't want time-consuming tools (such as Sledgehammer) to run
automatically even while I am still editing a statement. I made it into
a habit to invoke "try" whenever I've finished writing down a statement.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:20):From: Christoph LANGE <math.semantic.web@gmail.com>
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. And
otherwise fall back to "try" if I don't like it.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:20):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-07 22:05 Christoph LANGE:
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
Last updated: Nov 21 2024 at 12:39 UTC