2026-07-21T14:13:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3121 2024-03-06T10:33:49Z ddc:004 open_access

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 Duran, Francisco Eker, Steven Escobar, Santiago Meseguer, Jose Talcott, Carolyn Rewriting logic narrowing unification variants 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Francisco Duran and Steven Eker and Santiago Escobar and Jose Meseguer and Carolyn Talcott 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.31 urn:nbn:de:0030-drops-31211 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.31 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode