Our previous work with Joseph Goguen and the other members of the OBJ team has influenced the design of Maude in important ways; in fact, OBJ3 is essentially a functional sublanguage of Maude. We thank Timothy Winkler for his valuable contributions to the development of the Maude ideas. We also thank Carolyn Talcott for many discussions on Maude and for her valuable suggestions on strategy aspects. We are grateful to Jean-Pierre Jouannaud and Adel Bouhoula for their collaboration on the proof theory and theorem proving techniques of membership equational logic, and to Peter Mosses for his very detailed and helpful comments on this paper and his kind help and advice with its LaTeX and HTML versions. Ralph Wachter deserves special thanks for encouraging us in the development of the Maude ideas from the initial stages to the present. We are grateful for very helpful discussions and exchanges with Christiano Braga, Roberto Bruni, Grit Denker, Kokichi Futatsugi, Claude and Hélène Kirchner, Alexander Knapp, Ulrike Lechner, Christian Lengauer, Ugo Montanari, Pierre-Etienne Moreau, Uri Nodelman, Peter Ölveczky, Isabel Pita, Mark-Oliver Stehr, Valentin Turchin, Martin Wirsing, and many other colleagues.