Equational reasoning is an important component in symbolic algebra, automated deduction, high-level programming languages, program verification, and artificial intelligence. Reasoning with equations involves deriving consequences of given equations and finding values for variables that satisfy a given equation. Rewriting is a very powerful method for dealing with equations. Directed equations, called rewrite rules, are used to replace equals by equals, but only in the indicated direction. The theory of rewriting centers around the concept of normal form, an expression that cannot be rewritten any further. Computation consists of rewriting to a normal form; when the normal form is unique, it is taken as the value of the initial expression. When rewriting equal terms always leads to the same normal form, the set of rules is said to be convergent and rewriting can be used to check for equality. The International Conference on Rewriting Techniques and Applications (RTA) is the major conference in the domain of rewriting. Its creation has been decided after the Workshop on the Rewrite Rule Laboratory, held in Schenectady (NY) in September 1983. From 1985 to 1993, RTA has been a bi-annual conference. In 1995, RTA has been merged with the Workshop on Conditional (and Typed) Term Rewriting Systems (CTRS) and has become an annual conference.
