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.
(BibTeX entry) (gzip'ed Postscript)