https://studiegids.vu.nl/en/courses/2024-2025/XM_400121The students will learn to: (a) reason about properties of abstract reduction systems, (Applying knowledge and understanding) (Making judgements) (b) understand term rewriting and be able to design term rewriting systems, (Knowledge and understanding) (Applying knowledge and understanding) (c) understand and apply combinatory logic, (Knowledge and understanding) (Applying knowledge and understanding) (d) reason about and prove termination of TRSs (using recursive path orders, monotone algebras,...), (Applying knowledge and understanding) (Making judgements) (e) reason about confluence of TRSs (using critical pairs and orthogonality), (Applying knowledge and understanding) (Making judgements) (f) apply Knuth-Bendix completion, (Applying knowledge and understanding) (g) understand and apply different reduction strategies, (Knowledge and understanding) (Applying knowledge and understanding) (h) reason about properties of TRSs using modularity, (Applying knowledge and understanding) (Making judgements) (g) understand (un)decidability of important properties, (Knowledge and understanding) (h) understand the basic concepts of infinitary rewriting. (Knowledge and understanding)Term rewriting systems (TRSs) provide a natural formalism for specifying rules of computation and investigating their properties. TRSs are also of basic importance for functional programming and for the implementation of abstract data types. Applications can also be found in theorem proving, proof checking, and logic programming. During this course, students will learn the fundamental notions of term rewriting and getting acquainted with some more advanced topics in the field.Lectures and exercise classes.At the end of the course, there is a written final exam. The final grade is the grade of the final exam.Course notes will be provided on Canvas.MSc Computer Science