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

Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer & Carolyn Talcott
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...