A Church-Rosser Checker Tool for Maude Equational Specifications

Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer

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 CafeOBJ and of membership equational logic specifications in Maude. 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. The fact that rewriting logic is a reflective logic, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the design of the tools.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International