## Reading

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.