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.

• A Church-Rosser Checker Tool for Maude Equational Specifications
• Termination Checker and Knuth-Bendix Completion Tools for Maude Equational Specifications
• Coherence Checker and Completion Tools for Maude Specifications
• The Interoperation of Church-Rosser Checker, Termination Checker, and Coherence Checker
• An Inductive Theorem Prover (ITP Tool)