Rewriting in Computer Science and Logic

This lecture is intended to give an introduction to term rewriting systems and their application in computer science and logic. In particular we will discuss general reduction relations, properties of reduction systems such as confluence and termination, and completion procedures.

Term rewriting systems developed out of mathematical logic and are an important part of theoretical computer science. They have applications in many areas, from functional programming to automatic theorem proving and computer algebra. The theory of rewriting is fundamental to concepts in constructive algebra, such as Gröbner bases, and also to concepts in logic, such as decision of equational theories (e.g. the theory of groups).

Organization

Summer Semester 2019.

Number:	326.065
Title:	Rewriting in Computer Science and Logic
Lecturer:	Temur Kutsia
Time:	Friday, 12:00–13:30
Room:	T 406
Language:	English
First meeting:	March 8
Registration:	Via the KUSSS system. Please register also for the exercises.
Grading:	Exercises, written exam at the end of the semester.

Exercises

Exercises will be held on Fridays, after the lecture, between 13:45–14:30 in the same room, T 406. Instructor: Cleopatra Pau.

Course Materials

Slides

Literature

J. Avenhaus, Reduktionssysteme, Springer-Verlag, 1995.
F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge Univ. Press, 1998.
R. V. Book, F. Otto, String-Rewriting Systems, Springer-Verlag, 1993.
N. Dershowitz, D. A. Plaisted, Rewriting. In A. Robinson, A. Voronkov (eds.), Handbook of Automated Reasoning, pp. 535-610, Elsevier Science Publ., 2001.
Terese. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55, Cambridge University Press, 2003.
Materials from the International School on Rewriting. 2009, 2010, 2012, 2014, 2015, 2017.
Tools on Rewriting.