This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Σ, Ax ∪ E ), the E , Ax-variants of a term t are understood as the set of all pairs consisting of a substitution σ and the E , Ax-canonical form of t σ. The equational theory Ax ∪ E has the finite variant property iff, for each term, there is a finite and complete 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.
Keywords: Rewriting logic, narrowing, unification, variants