Zulip Chat Archive

Stream: general

Topic: hammers


view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:26):

I want to write a couple of sentences on "hammers" in general, in an article. Am I right in thinking that the original hammer was sledgehammer, which is something to do with Paulson and/or @Jasmin Blanchette ? Is there something explicit I can cite? This is 2010, right? I googled around but keep finding instruction manuals. Is there a publication for "Hammer for Coq"? I can't find anything other than preprints. Are there hammers for other systems? I know about @Gabriel Ebner 's work in Lean (and I am assuming there is also nothing to cite here). By a hammer I think I mean an interface which enables an ITP to talk to an ATP. Would it be right to claim that hammers are currently any kind of "hot topic" or "active area of study"? Or is the basic idea completely understood and the only issue is what parameters and lemmas one should pass to the ATP? Is the latter question a boring one, basically understood, or something which one could envisage AI having a say in?

view this post on Zulip Rob Lewis (Apr 23 2020 at 11:38):

This paper is a nice early summary and cites the earliest hammer papers at the beginning: https://www.cl.cam.ac.uk/~lp15/papers/Automation/paar.pdf

Jasmin is responsible for some big improvements, including https://people.mpi-inf.mpg.de/~jblanche/enc_types_paper.pdf, but he can better point you to his canonical references.

I think the CoqHammer publication is in JAR, https://link.springer.com/article/10.1007/s10817-018-9458-4

view this post on Zulip Rob Lewis (Apr 23 2020 at 11:39):

Would it be right to claim that hammers are currently any kind of "hot topic" or "active area of study"?

Not really, I'd say. Adapting them for more complicated logics (like CoqHammer) is interesting, but IMO it isn't a "hot topic."

view this post on Zulip Rob Lewis (Apr 23 2020 at 11:41):

the only issue is what parameters and lemmas one should pass to the ATP? Is the latter question a boring one, basically understood, or something which one could envisage AI having a say in?

(This is just my impression, I don't have citations to back this up.) I think relevance filtering is well understood, and it's not really the bottleneck in hammer performance. You can make small gains with fancy AI filters. The bigger bottlenecks are the translations, especially for CIC, ATP performance, and reconstruction.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:41):

The reference I use for "hammers" is "Hammering towards QED":
https://people.mpi-inf.mpg.de/~jblanche/h4qed.pdf
Its four authors can be considered the main hammer people (Sledgehammer, MizAR\mathrm{Miz}\mathbb{AR}, HOLyHammer, CoqHammer).

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:41):

(If you go to DBLP (dblp.org), you can look up all the refs I'll give you.)

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:42):

Aah super. I was using math reviews which has some stuff (e.g. it had the Coq ring paper), but not all stuff.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:42):

The PAAR 2010 paper Rob mentioned and the slightly updated IWIL 2010 paper is a good early reference that still gets cited a lot, probably because it has "Sledgehammer" in its title.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:44):

The "Hammering towards QED" will give you references to all the other systems, including MizAR, as of 2014--2015, though.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:44):

What system is HOLyhammer?

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:44):

It's for HOL Light and HOL4.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:44):

By Kaliszyk and Urban.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:44):

Is Sledgehammer for Isabelle, or Isabelle/HOL?

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:44):

/HOL.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:45):

Many thanks Jasmin.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:45):

There were plans to port it to set theory.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:45):

Don't mention it.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:45):

There were over a dozen hammer systems over time, in various systems.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:46):

But Sledgehammer was the first that was actually useful and usable, starting around the end of 2008.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:47):

Sledgehammer's secret was its architecture: relevance filter (most don't have that) + efficient translation (that leaves first-order stuff alone) + reconstruction using an all-purpose ATP built directly into Isabelle (metis).

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:48):

Most other systems I can think of, including recent work such as SMTCoq (AFAIK), don't do relevance filtering. Users have to come up with an exaustive list of potentially relevant lemmas themselves. That in practice makes the tool 100 times less useful.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:48):

It's a bit like using super directly.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:49):

For reconstruction, metis is like super, roughly, but substantially faster. Maybe Lean 4 will fix that finally.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:52):

Concerning "hot topic": I hear left and right about people working on hammers, e.g. based on Dedukti and what not. I think Assia is supervising a student about this. And there are, like, 3 ERC grants at the same time about hammers to some extent (Cezary's, Josef's, and mine -- the goal with Matryoshka is to have HO ATPs we can integrate in proof assistants). But it's still a small fraction of papers at, say, CPP/ITP, so I'd go with "active area of study".

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:53):

I found it hard to google for information about hammers, apparently there is some popular tool with a metal head which the word is also used for. I tried "Isabelle Hammer" but to my surprise just managed to find a big list of people on Linkedin called Isabelle Hammer.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:53):

Finally, for AI in hammers, you have to look at HOLyHammer and what Cezary Kaliszyk and Josef Urban have been doing for, like, 8 years now at least in Cezary's case and 20 for Josef.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:54):

Well start with "Hammering towards QED". We even made the title Briton-friendly. (Don't worry; the rest of the paper is in proper, American English.)

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:55):

There's also a paper called "More SPASS with Isabelle". Given that SPASS means "fun" in German, make sure to Google for it with parental control on.

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 11:56):

Not so surprised. My real estate agent was called Bibi Hammer.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:57):

I think I have more than enough now; thanks.

view this post on Zulip Reid Barton (Apr 23 2020 at 12:01):

Jasmin Blanchette said:

Its four authors can be considered the main hammer people (Sledgehammer, MizAR\mathrm{Miz}\mathbb{AR}, HOLyHammer, CoqHammer).

Sounds like some theorem provers/Avengers crossover

view this post on Zulip Jasmin Blanchette (Apr 23 2020 at 12:12):

The four riders of the acoqalypse.


Last updated: May 17 2021 at 22:15 UTC