A Set of Proving Tools for Maude Specifications
In these pages there are links to a set of tools for Maude specifications.
Each of the pages offers information about the design and use of the different
tools, which have been written entirely in Maude and are in fact executable
specifications in rewriting logic of the formal inference systems that
they implement. The fact that rewriting logic is reflective, and that Maude
efficiently supports reflective rewriting logic computations is systematically
exploited in the design of the tools.