Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (Tutorial)

Resumen:

This paper introduces some novel features of Maude 2.7. We have added support for: (i) built-in order-sorted unification modulo associativity, commutativity, and identity, (ii) built-in variant generation, (iii) built-in order-sorted unification modulo a finite variant theory, and (iv) symbolic reachability modulo a finite variant theory.

Palabras Clave:

associativity commutativity and identity - Maude - narrowing - Order-sorted - unification

Autor(es):

• Francisco Durán {duran@lcc.uma.es}
  Universidad de Málaga
  
• Steven Eker {eker@csl.sri.com}
  SRI International
  
• Santiago Escobar {sescobar@dsic.upv.es}
  Universitat Politècnica de València
  
• Narciso Martí-Oliet {narciso@ucm.es}
  Universidad Complutense de Madrid
  
• José Meseguer {meseguer@cs.uiuc.edu}
  University of Illinois at Urbana-Champaign
  
• Carolyn Talcott {clt@cs.stanford.edu}
  SRI International
  

Handle:

Descargas:

Este artículo tiene una licencia de uso CreativeCommons Reconocimiento (by)

Descarga el artículo haciendo click aquí.