REWRITE SYSTEMS
Autumn 2004
Nachum Dershowitz


  1. Introduction (PDF)
  2. Termination (PDF)
  3. Orderings (PDF)
  4. Dependencies (PDF)
  5. Confluence (PDF)
  6. Critical Pairs
    1. Part a (PDF only)
    2. Part b (PDF)
  7. Completion (PDF only)
  8. Theorem Proving (PDF)
  9. Well-quasi ordered labelled trees (PDF only)
  10. Superposition (PDF only)
  11. Orthogonality (PDF)
  12. Strategies (PDF)
  13. Semantic Unification (PDF)
  14. Induction & Conclusion (PDF)