This is an old revision of the document!

---

Lecture 19

Push-down automata

First-order theorem provers: completeness of resolution