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.
Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Martí-Oliet / José Meseguer / Carolyn Talcott /
Palabras Clave: associativity commutativity and identity - Maude - narrowing - Order-sorted - unification
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