Rewriting Systems


Expertise of the fundamental concepts of rewriting systems, such as termination and confluence.

To know the proof the basic results of the theory of rewriting systems, including the theorem of critical pairs.

Know how to apply the fundamental results on the theory of semigroup presentations and Grobner bases.

Recognize the application of these concepts in some computer systems, such as the computer algebra systems, in automatic theorem proving, in the specification and verification of programs and programming languages ​​of higher orders.

General characterization





Responsible teacher

João Jorge Ribeiro Soares Gonçalves de Araújo


Weekly - Available soon

Total - 16

Teaching language



Available soon


• Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press,1998.

• Benjamin Benninghofen, Susanne Kemmerich and Michael M. Richter. Systems ofReductions. Lecture Notes in Computer Science, vol. 277. Springer-Verlag, 1987.

• Ronald V. Book and Friedrich Otto. String-Rewriting Systems. Springer-Verlag, 1993.

• TERESE, Term Rewriting Systems, Cambridge University Press, 2003.

• Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.

Teaching method

Available soon

Evaluation method

Available soon

Subject matter

1. Abstract Reduction Systems: equivalence and reduction; well-founded induction; order relations.

2. Term Rewriting Systems: terms, substitutions, and identities; free algebras; term álgebras; equational classes; equational problems.

3. String-Rewriting Systems: Church-Rosser Congruences; the word problem; semigroups and presentations.

4. Termination: the decision problem; reduction orders; simplification orders.

5. Confluence: confluence and locally confluence; the decision problem; critical pairs.

6. Completion: the Knuth-Bendix completion procedure.

7. Gröbner Bases: polynomial reduction; Gröbner bases; Buchberger''''''''''''''''s algorithm.


Programs where the course is taught: