This class, we will read Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers [PDF] [DOI] by Lawrence C. Paulson and Jasmin Christian Blanchette.
Sledgehammer works by flattening goals in Isabelle/HOL's logic (a classical higher-order logic called HOL) into first-order logic, then invoking first-order procedures to dispatch those goals. Sledgehammer also reconstructs lower-level proofs in the end, so that the resulting proof does not always rely on calls to Sledgehammer. (I am not sure to what degree proof reconstruction is used in practice, relative to keeping calls to Sledgehammer in the code.)
Probably the coolest thing about Sledgehammer is that people actually use it. That's impressive, because often one of the hardest problems of building powerful tools and automation is getting people to use it---that is, adoption. This paper focuses on the design decisions that contributed to adoption, at least in the authors' views.
Sledgehammer has seen a number of implementations in proof assistants other than Isabelle/HOL, including in Coq. But Sledgehammer remains immensely popular, while some of these other tools have not really taken off. The reasons for this are hard to pin down---and worthy of discussion.
You can find a reading guide and the discussion questions below. The public version of the slides for this class are here.
Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.