This paper explains the design and use of two equational proving tools, namely an inductive theorem prover-to prove theorems about equational specifications with an initial algebra semantics-and a Church-Rosser checker-to check whether such specifications satisfy the Church-Rosser property. These tools can be used to prove properties of order-sorted equational specifications in Cafe [11] and of membership equational logic specifications in Maude [7, 6]. The tools have been written entirely in Maude and are in fact executable specifications in rewriting logic of the formal inference systems that they implement. Both of these tools treat equational specifications as data that is manipulated. For example, the inductive theorem prover may add an induction hypothesis as a new equational axiom: and the Church-Rosser checker computes critical pairs and membership axioms by inspecting the equations in the original specification. This makes a reflective design - in which theories become data at the metalevel- ideally suited for the task. The fact that rewriting logic is a reflective logic, and Maude efficiently supports reflective rewriting logic computations is systematically exploited in the tools. Rewriting logic reflection allows a modular and declarative treatment of proof tactics. Such tactics can be formally specified by rewrite rules at the metalevel of the theory expressing the tool's inference system, and can be easily changed at will without any modification whatsoever to the inference system itself. The very high level of abstraction at which the tools have been developed has made it relatively easy to build them, makes their implementation easy to understand, and will make their maintenance and future extensions much easier than for conventional implementations, Thanks to the high performance of the Maude engine these important benefits in ease of development, understandability, maintainability, and extensibility, and in flexibility for introducing formally-defined proof tactics, are achieved without sacrificing performance.

• cafe-paper.dvi.gz
• cafe-paper.ps