Class 11: Proof Procedures

For the eleventh class, we will read First-Order Proof Tactics in Higher-Order Logic Theorem Provers [PDF] by Joe Hurd.

This is the canonical paper for the Metis automatic theorem prover (ATP) for first-order logic with equality. Metis implements a number of proof procedures for first-order logic with equality (which is in general undecidable, though it has decidable fragments).

The neat thing about Metis is that it has been implemented inside of several proof assistants like Isabelle/HOL and HOL4. Even though those theorem provers are based on higher-order logics, they can call out to Metis to dispatch first-order proofs. In that sense, it's a neat and early example of interaction between ATPs and proof assistants, a mixed-methods workflow we continue to see more and more of to this day. We'll see that a lot more when we get to the ATP weeks of class.

You can find a reading guide and the discussion questions below.

Please note that this is due the morning before class, so that we can discuss it in person. There is no artifact for this reading as I will be away on Thursday---I recommend spending the time you'd normally spend on an artifact this week revisiting an artifact from a previous week in more detail, or playing with the metis tactic in the Isabelle/HOL proof assistant.

The first thing to note about this paper is that it is from 2003. So it is important to remember that context when you read it.

The paper is fairly technical, as it is meant to help the reader implement similar automation in another proof assistant if needed. It is nice to get a sense of how the technical approach works and how the automation is implemented, but it is OK to get lost with all of the details.

Section 6 comes late, but I think it's an especially good read, even though it's short. So I'd be sure to read that, even if you get tired by page 11.

Please write a short paragraph as a comment in the class forum thread about any one of the following discussion questions (you need to respond to just one question of your choice to get credit, though you're free to write more if interested):

1. What are some other fragments of higher-order logics or particular domains for which similar general-purpose automation could be useful?
2. How would you implement this differently in 2022, if at all?
3. How would you implement this for a proof assistant with a dependent type theory, like Coq, Lean, or Agda?
4. Would you trust automation like this without the translated refutations? Why or why not?
5. Given translated refutations into your base higher-order logic, would you feel satisfied with a proof dispatched by interacting with Metis, and find it sufficiently informative? Why or why not? And if not, what would make it more satisfying or informative to you?
6. Write a paragraph responding to someone else's comment in the discussion forum.
7. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.

You may want to look at other people's responses before class in order to shape the discussion. And again remember that you need to answer just one question to get credit, though you are free to answer more if interested.