Faculty of Science

Objectives

provide an introductory grasp of term rewriting, possible extensions and demonstration of practical application areas.

Contents

Abstract reduction systems; Notions of: well-foundedness, well-formedness; Ordered sets; reduction, lexicographic, multiset orders. Other requisite mathematical foundations. Universal algebra: terms, substitutions, and identities; algebras, homomorphisms; congruences; term and Σ algebras; equational and inductive theories. Term rewriting systems; equational problems (matching, word problem, etc.); syntactic unification; notions in semantic (equational) unification. Termination: decidability; reduction/polynomial orders, simplification/recursive path orders, etc. Confluence: Church-Rosser property and normal forms; critical pairs, orthogonality. Mention combination problems. Completion: completion procedures and proof orders; Knuth-Bendix completion algorithm, etc. Mention/overview extensions: ordered, conditional, class, class conditional TRS and some of their termination/confluence constraints; higher-order rewriting systems; graph rewriting systems; narrowing; reduction strategies. Illustrative applications: programming languages, proof systems; symbolic and algebraic computations; proof checking; functional and logic programming.

Prerequisite: