1 Search Results for "Eker, Steven"

Document
DOI: 10.4230/LIPIcs.RTA.2011.31
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6

Authors: Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{duran_et_al:LIPIcs.RTA.2011.31,
  author =	{Duran, Francisco and Eker, Steven and Escobar, Santiago and Meseguer, Jose and Talcott, Carolyn},
  title =	{{Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{31--40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.31},
  URN =		{urn:nbn:de:0030-drops-31211},
  doi =		{10.4230/LIPIcs.RTA.2011.31},
  annote =	{Keywords: Rewriting logic, narrowing, unification, variants}
}
  • Refine by Author
  • 1 Duran, Francisco
  • 1 Eker, Steven
  • 1 Escobar, Santiago
  • 1 Meseguer, Jose
  • 1 Talcott, Carolyn

  • Refine by Classification

  • Refine by Keyword
  • 1 Rewriting logic
  • 1 narrowing
  • 1 unification
  • 1 variants

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2011

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact