The present document gives detailed explanations of our reflective design for the inductive theorem prover and the Knuth-Bendix checker that we are building as part of the Cafe project. The Maude code for each of the tools is also given and discussed in its entirety. 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 in a separate section. In the rest of this introduction we give high-level informal explanations of the key concepts on reflection and strategies at the heart of our design and implementation for the tools, and of the tools themselves.

• cafe97.ps