TY - GEN
T1 - Variants, unification, narrowing, and symbolic reachability in Maude 2.6
AU - Durán, Francisco
AU - Eker, Steven
AU - Escobar, Santiago
AU - Meseguer, José
AU - Talcott, Carolyn
PY - 2011
Y1 - 2011
N2 - 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 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.
AB - 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 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.
KW - Narrowing
KW - Rewriting logic
KW - Unification
KW - Variants
UR - http://www.scopus.com/inward/record.url?scp=84866398042&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84866398042&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.RTA.2011.31
DO - 10.4230/LIPIcs.RTA.2011.31
M3 - Conference contribution
AN - SCOPUS:84866398042
SN - 9783939897309
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 31
EP - 40
BT - 22nd International Conference on Rewriting Techniques and Applications, RTA 2011
T2 - 22nd International Conference on Rewriting Techniques and Applications, RTA 2011
Y2 - 30 May 2011 through 1 June 2011
ER -