eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2011-04-26
31
40
10.4230/LIPIcs.RTA.2011.31
article
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6
Duran, Francisco
Eker, Steven
Escobar, Santiago
Meseguer, Jose
Talcott, Carolyn
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol010-rta2011/LIPIcs.RTA.2011.31/LIPIcs.RTA.2011.31.pdf
Rewriting logic
narrowing
unification
variants