This document explains the design and use of a coherence checker tool and of a coherence completion tool. The coherence checker tool checks whether a rewrite logic specification is coherent, and the coherence completion tool tries to complete a rewrite logic specification in order to make it coherent. These tools can be used to prove the coherence property or to coherence complete order-sorted rewrite specifications in Maude. The tools have been written entirely in Maude and are in fact executable specifications in rewriting logic of the formal inference system that they implement. The fact that rewriting logic is reflective, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the design of the tools.
(BibTeX entry) (gzip'ed Postscript)