A Church-Rosser Checker Tool for Maude Equational Specifications

This document explains the design and use of a Church-Rosser checker tool, which checks whether an equational specification satisfies the Church-Rosser property. This tool can be used to prove the Church-Rosser property of order-sorted equational specifications in
Maude. The tool has been written entirely in Maude and is in fact an executable specification in rewriting logic of the formal inference system that it implements. The fact that rewriting logic is reflective, and that Maude efficiently supports reflective rewriting logic
computations is systematically exploited in the design of the tool.
 
 

Maude Specifications and Samples

• A Church-Rosser Checker Tool for Maude Equational Specifications (crc.tar)

Instructions: Load full-maude.maude and then crc.maude. Then start the loop (loop init .). The tool is now ready for entering the examples below.

Examples:

Making a natual numbers specification confluent (ex-crc-nats.fm)

Proving an integer numbers specification groung-Church-Rosser (ex-crc-ints.fm)

A second specification of the natural numbers (ex-crc-nats-II.fm)

A second specification of the integer numbers (ex-crc-ints-II.fm)

A specification of the rational numbers (ex-crc-rats.fm)

• A Church-Rosser Checker Tool for Maude Equational Specifications. By Francisco Durán and José Meseguer. Manuscript. Universidad de Málaga and SRI International. July 2000.
• Building Equational Proving Tools by Reflection in Rewriting Logic. By Manuel Clavel, Francisco Durán, Steven Eker, and José     Meseguer. In Cafe: An Industrial-Strength Algebraic Formal Method, Kokichi Futatsugi, Ataru Nakagawa, and Tetsuo Tamai, editors. Elsevier, 2000.
• Building Equational Proving Tools by Reflection in Rewriting Logic. By Manuel Clavel, Francisco Durán, Steven Eker, and José     Meseguer. In Proceedings of the CafeOBJ Symposium '98, Sumazu, Japan. CafeOBJ Project, April, 1998.
• Design and Implementation of the Cafe Prover and Church-Rosser Checker Tools. By Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer. Manuscript, March 1998.