Email Gateway (Aug 22 2022 at 21:15): Email Gateway (Aug 22 2022 at 21:15):From: Giles Reger <giles.reger@manchester.ac.uk>
Hello,
I am looking for academic or industrial users of Sledgehammer who are using Vampire via Sledgehammer or are interested in using Vampire via Sledgehammer.
For context, I am asking for two reasons:
I often say “lots of people use Vampire via Sledgehammer” but I don’t really know if this is true and have very little evidence to support the statement — my only datapoint is the number of requests Geoff occasionally reports as sent to SystemOnTPTP from Sledgehammer (remote_vampire). But now that Isabelle comes with a (non-commercial) version of Vampire it might be that we have more users. It would be great to gain some awareness of some (if any) projects benefitting from Vampire via Sledgehammer.
I would like to make Vampire “better" at handling problems produced by Sledgehammer in the (nearish) future. Knowing some people who use Sledgehammer would be potentially useful in motivating and evaluating this work.
Cheers, Giles
Email Gateway (Aug 22 2022 at 21:15):From: Lawrence Paulson <lp15@cam.ac.uk>
This is undoubtedly true. Many (probably most) Isabelle users click their Sledgehammer button all the time, invoking Vampire as well as other provers. There are no statistics on how frequently Vampire is successful or how often it beats other systems. Vampire has been available to install for quite a long time already (a number of years, though often persistence was needed to grab a copy).
Larry Paulson
Email Gateway (Aug 22 2022 at 21:15):From: Peter Lammich <lammich@in.tum.de>
Hi Giles.
I use sledgehammer on a regular basis. However, neither which prover
found the proof, nor how often I actually used sledgehammer during
proof exploration work, is somehow visible from the final theory.
Nevertheless, it would be safe to say that, without sledgehammer, we
would not have won interactive verification competitions (VerifyThis,
ProofGround), and our daily proving work would be much more cumbersome.
Email Gateway (Aug 23 2022 at 08:11):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Same here. I (and I suspect our entire team of about 10 fairly active Isabelle user) use it often, but have no statistics.
From memory, it does sometimes come up with the only proof, which then sometimes is too large to replay. (cvc4 and z3 also sometimes come up with proofs the other tools do not find, i.e. it’s not always the case that vampire is the only one who finds a proof).
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:11):From: Tobias Nipkow <nipkow@in.tum.de>
Same here. That is, sledgehammer is a major advance. Experts (incl myself) and
novices (incl my students) alike love it.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:11):From: "John F. Hughes" <jfh@cs.brown.edu>
I'd say it accounts for about 80% of my (limited) success with Isabelle.
And it's clear I need to learn about this "vampire" thing as well. :)
Email Gateway (Aug 23 2022 at 08:12):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear John,
also here in Innsbruck, sledgehammer is heavily used.
I personally turned on "SLEDGEHAMMER_SPY=yes” in etc/settings some time
ago, which generates statistics about sledgehammer usage in a separate file.
I will send this file in a separate email to you (not the mailing list);
perhaps it is useful for your evaluation.
Cheers,
René
Email Gateway (Aug 23 2022 at 08:12):From: Manuel Eberl <eberlm@in.tum.de>
As a bit of a counterpoint: I personally don't use sledgehammer very
much. Perhaps it is just a personal preference – I am a bit impatient
and don't like interrupting my work flow and wait for 20 or 30 seconds.
I do use sledgehammer when I am frustrated by something that seems
intuitively obvious but I'm not quite sure what the easiest way to prove
it is. Most of the time, sledgehammer is then just as stumped as I am,
but occasionally it comes up with a proof.
However, sledgehammer proofs are often fairly clunky. I don't really
like proofs that say "by (metis …)", where "…" is a list of 20 technical
lemmas, one of which is "semiring_normalization_rules(37)". That's
another reason why I don't use sledgehammer as often as everyone else.
In any case, it's a great tool, and it seems that it has continuously
gotten better since I started using Isabelle some 8 years ago.
I've also heard that people sometimes use it as a sort of semantic
"find_theorems" command.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:12):From: Lawrence Paulson <lp15@cam.ac.uk>
On 20 Jan 2020, 10:05 +0000, Manuel Eberl <eberlm@in.tum.de>, wrote:
As a bit of a counterpoint: I personally don't use sledgehammer very
much. Perhaps it is just a personal preference – I am a bit impatient
and don't like interrupting my work flow and wait for 20 or 30 seconds.
A key design goal, realised already by 2007, was background operation: you can do other things while waiting for Sledgehammer to finish. So in particular, you can continue editing your document provided you confine your changes to below the cursor.
I do use sledgehammer when I am frustrated by something that seems intuitively obvious
Here we differ, because I often use Sledgehammer when I'm really not sure whether something is true or not.
However, sledgehammer proofs are often fairly clunky. I don't really
like proofs that say "by (metis …)", where "…" is a list of 20 technical
lemmas, one of which is "semiring_normalization_rules(37)".
This certainly is annoying and requires a second pass through completed proofs. Once you know that you've actually got a theorem, it's worth the effort to make it look good.
Larry
Last updated: Nov 21 2024 at 12:39 UTC