    

Building Equational Proving Tools by Reflection in Rewriting Logic
by Dr. Steven Eker, Manuel Clavel, Francisco Duran & José Meseguer.
Abstract
This paper explains the design and use of two equational proving tools,
namely an inductive theorem proverto prove theorems about equational specifications with an initial algebra semanticsand a ChurchRosser checkerto check whether such specifications satisfy the ChurchRosser property. These tools can be used to prove properties of ordersorted 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 ChurchRosser 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 formallydefined proof tactics, are achieved without sacrificing performance.
Files


