SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Current Design and Implementation of the Cafe Prover and Knuth-Bendix Checker Tools
 by Dr. Steven Eker, Manuel Clavel & Josť Meseguer.

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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2022 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy