Rewriting Systems
Objectives
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
Code
8417
Credits
6.0
Responsible teacher
Available soon
Hours
Weekly - 4
Total - 16
Teaching language
Português
Prerequisites
Available soon
Bibliography
• 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.