by Francisco Durán and José Meseguer
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.
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
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.
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,
Design and Implementation
of the Cafe Prover and Church-Rosser Checker Tools. By Manuel Clavel,
Francisco Durán, Steven Eker, and José Meseguer. Manuscript,