Navegación

Búsqueda

Búsqueda avanzada

Resultados de búsqueda para associativity

Associative Unification and Symbolic Reasoning Modulo Associativity in Maude

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.

Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Marti-Oliet / Jose Meseguer / Carolyn Talcott / 
Palabras Clave: associativity - narrowing - Rewriting Logic - unification

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada