LIPIcs.RTA.2011.31.pdf
- Filesize: 248 kB
- 10 pages
Document
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6
Authors
-
Part of:
Volume:
22nd International Conference on Rewriting Techniques and Applications (RTA'11) (RTA 2011)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2011-04-26
Cite As Get BibTex
Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott. Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 31-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.RTA.2011.31
Abstract
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.
Subject Classification
Keywords
- Rewriting logic
- narrowing
- unification
- variants
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads