Unification and narrowing in maude 2.4

Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications, and has a relatively large worldwide user and open-source developer base. This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel functions for order-sorted unification modulo some frequently occurring equational axioms. Narrowing is currently supported in its Full Maude extension. We also give a brief summary of the most important features of Maude 2.4 that were not part of Maude 2.0 and earlier releases. These features include communication with external objects, a new implementation of its module algebra, and new predefined libraries. We also review some new Maude applications.

Original languageEnglish (US)
Title of host publicationRewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings
Number of pages11
StatePublished - 2009
Event20th International Conference on Rewriting Techniques and Applications, RTA 2009 - Brasilia, Brazil
Duration: Jun 29 2009Jul 1 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5595 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other20th International Conference on Rewriting Techniques and Applications, RTA 2009

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Unification and narrowing in maude 2.4'. Together they form a unique fingerprint.

Cite this