Associative-commutative reduction orderings (Q1198005)

A rewrite system terminates if the rewrite rules define a relation which is contained in a well-founded ordering, called a reduction ordering. The paper shows how the lexicographic path ordering can be modified so as to make it compatible with associativity and commutativity, i.e. to ensure that if \(v\) is derivable from \(u\) and \(s\), \(t\) are terms obtained from \(v\), respectively \(u\), by computative or associative rules, then \(s\) is derivable from \(t\).