Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6

This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence