Variants, unification, narrowing, and symbolic reachability in Maude 2.6

Francisco Durán, Steven Eker, Santiago Escobar, José Meseguer, Carolyn Talcott

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication22nd International Conference on Rewriting Techniques and Applications, RTA 2011
Pages31-40
Number of pages10
DOIs
StatePublished - Dec 1 2011
Event22nd International Conference on Rewriting Techniques and Applications, RTA 2011 - Novi Sad, Serbia
Duration: May 30 2011Jun 1 2011

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume10
ISSN (Print)1868-8969

Other

Other22nd International Conference on Rewriting Techniques and Applications, RTA 2011
CountrySerbia
CityNovi Sad
Period5/30/116/1/11

Keywords

  • Narrowing
  • Rewriting logic
  • Unification
  • Variants

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Variants, unification, narrowing, and symbolic reachability in Maude 2.6'. Together they form a unique fingerprint.

  • Cite this

    Durán, F., Eker, S., Escobar, S., Meseguer, J., & Talcott, C. (2011). Variants, unification, narrowing, and symbolic reachability in Maude 2.6. In 22nd International Conference on Rewriting Techniques and Applications, RTA 2011 (pp. 31-40). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 10). https://doi.org/10.4230/LIPIcs.RTA.2011.31