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