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.