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

Design and Implementation od the Cafe Prover and Church-Rosser Checker Tools
 by Dr. Steven Eker, Manuel Clavel, Francisco Duran & José Meseguer.

Abstract
The present document gives detailed explanations of our reflective design for the in­ductive 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.
Files
 













 

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