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.

[Maude Home Page]