Rewrite systems are sets of equations used to substitute equals for equals from left-to-right only. They have important applications to programming languages, since they represent a simple and intuitive functional language, and in automated deduction, where they play an important role in improving the efficiency of reasoning about equations. Termination of a system means that the equations cannot be used infinitely often, without reaching a term that does not contain an instance of a left-handed side. Proving termination can be difficult. (It is, of course, undecidable in general.) Under past support, a number of methods for proving termination were devised which have proved useful. New aspects of this subject are now being investigated with an emphasis on semantic methods for structured (hierarchical) systems and extensions of rewriting to handle conditional equalities, associative- commutative functions, higher-order rewriting, and a logic programming style. Since establishing termination is an essential component of many automated deduction and program verification systems, this project will also invest effort in implementations.
