Computer Laboratory > Teaching > Course material 2009–10 > Basic Rewriting Theory

 

Basic Rewriting Theory
2009–10

Principal lecturer: Dr Marcelo Fiore
Taken by: MPhil ACS
Syllabus

►  Reading material from Term Rewriting and All That:

  • Motivating Examples (Chapter 1)
  • Equivalence and reduction:
    • Basic definitions (Section 2.1, pages 7 and 8)
  • Terms, substitutions, and identities (Section 3.1)
  • Equivalence and reduction:
    • Basic results (Section 2.1, pages 9 to 13)
  • Deciding equational theories (Section 4.1)
  • Unification:
    • Syntactic unification (Section 4.5)
    • Unification by transformation (Section 4.6)
  • Well-founded induction (Section 2.2, pages 13 and 14)
  • Proving Confluence (Section 2.7, pages 28 to 30)
  • Term Rewriting Systems (Section 4.2)
  • Confluence:
    • Undecidability (Section 6.1, page 134)
    • The Critical Pair Theorem (Section 6.2, pages 135 to 141)
  • Termination in Abstract Reduction Systems:
    • Proving termination (Section 2.3)
    • Lexicographic orders (Section 2.4)
    • Multiset orders (Section 2.5)
  • Termination in Term Rewriting Systems:
    • The decision problem (Section 5.1)
    • Reduction orders (Section 5.2)
  • Completion:
    • The basic completion procedure (Section 7.1)

►  Exercises from Term Rewriting and All That.