Maude system

The Maude system is an implementation of rewriting logic.

It is similar in its general approach to Joseph Goguen’s OBJ3 implementation of equational logic, but based on rewriting logic rather than order-sorted equational logic, and with a heavy emphasis on powerful metaprogramming based on reflection.

Maude is free software, and tutorials are available online.

It was originally developed at SRI International, but is now developed by a diverse collaboration of researchers.