Associative Unification and Symbolic Reasoning Modulo Associativity in Maude





Publicado en

Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019)

Licencia Creative Commons


We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unifica- tion problems u =? v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in prac- tice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incom- plete. This paper describes this associative unification algorithm imple- mented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrow- ing based symbolic reachability analysis have been extended to deal with associativity.


Acerca de Durán, Francisco

Palabras clave

Associativity, Narrowing, Rewriting Logic, Unification
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX