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.
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.