[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6
Duran, Francisco and Eker, Steven and Escobar, Santiago and Meseguer, Jose and Talcott, Carolyn - 2011 - PDF

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