This class, we are going to look at Sledgehammer in the wild! The paper we read on Tuesday was about Sledgehammer in practice. One of the coolest things about Sledgehammer is its extremely wide adoption in the Isabelle/HOL community. So we are going to look at some other people's proof developments, and how they use Sledgehammer or any of the automatic solvers it calls.
This exercise is going to be a bit more open-ended than what we've seen so far. Isabelle/HOL has an archive of proof developments; we will go through this archive to find developments that we like, and see how they use this automation. We'll also play around with modifying and understanding the development. We'll discuss in groups, then post on the board as usual. More below.
- Install the Isabelle/HOL proof assistant following these instructions.
- Download the Isabelle/HOL Archive of Formal Proofs here.
- Browse the Archive of Formal Proofs here, and identify a project that looks interesting to you. (If you would prefer to search for particular proofs using natural language, and use that to identify a project, you can use the SErAPIS search engine.)
- Open the interesting project in Isabelle/HOL, and make sure the proofs go through.
If you have any trouble, please post your questions in this class forum thread. Please also drop any installation tips you have in that thread.
If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked.
You can find the exercise we will do together in class below.