An Overview of Rewrite Rule Laboratory (RRL)
J. of Computer and
Mathematics with Applications,
29, 2, 1995, 91-114.
Deepak Kapur and Hantao Zhang
RRL ( Rewrite Rule Laboratory) was originally developed as an environment for experimenting with automated reasoning algorithms for equational logic based on rewrite techniques. It has now matured into a full-fledged theorem prover which has been used to solve hard and challenging mathematical problems in automated reasoning literature as well as a research tool for investigating the use of formal methods in hardware and software design. We provide a brief historical account of development of RRL and its descendants, give an overview of the main capabilities of RRL and conclude with a discussion of applications of RRL.