The present document gives detailed explanations of our reflective design for the inductive theorem prover and the Church-Rosser checker that we have built as part of the Cafe project. The Maude code for each of the tools is also given and discussed in its entirety. Furthermore, examples illustrating the use of the tools and methodological suggestions drawn from the examples are also given.
Since the reflective nature of rewriting logic and Maude, and the closely related concept of internal strategies, are key features of our design, we dedicate two sections to explain in detail how these concepts are supported by the Maude implementation. Each tool, including the formal system that it implements and its corresponding Maude implementation, is then explained and illustrated with examples in a separate section.
(BibTeX entry) (gzip'ed Postscript)