hammers

Stream: general

[Kevin Buzzard]

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?

[Rob Lewis]

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

[Rob Lewis]

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."

[Rob Lewis]

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.

[Jasmin Blanchette]

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, $\mathrm{Miz}\mathbb{AR}$, HOLyHammer, CoqHammer).

[Jasmin Blanchette]

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

[Kevin Buzzard]

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

[Jasmin Blanchette]

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.

[Jasmin Blanchette]

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

[Kevin Buzzard]

What system is HOLyhammer?

[Jasmin Blanchette]

It's for HOL Light and HOL4.

[Jasmin Blanchette]

By Kaliszyk and Urban.

[Kevin Buzzard]

Is Sledgehammer for Isabelle, or Isabelle/HOL?

[Jasmin Blanchette]

/HOL.

[Kevin Buzzard]

Many thanks Jasmin.

[Jasmin Blanchette]

There were plans to port it to set theory.

[Jasmin Blanchette]

Don't mention it.

[Jasmin Blanchette]

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

[Jasmin Blanchette]

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

[Jasmin Blanchette]

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).

[Jasmin Blanchette]

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.

[Jasmin Blanchette]

It's a bit like using super directly.

[Jasmin Blanchette]

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

[Jasmin Blanchette]

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".

[Kevin Buzzard]

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.

[Jasmin Blanchette]

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.

[Jasmin Blanchette]

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.)

[Jasmin Blanchette]

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.

[Jasmin Blanchette]

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

[Kevin Buzzard]

I think I have more than enough now; thanks.

[Reid Barton]

Jasmin Blanchette said:

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

Sounds like some theorem provers/Avengers crossover

[Jasmin Blanchette]

The four riders of the acoqalypse.