RRL

An overview of Rewrite Rule Laboratory (RRL). 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.


References in zbMATH (referenced in 55 articles )

Showing results 21 to 40 of 55.
Sorted by year (citations)
  1. Bonacina, Maria Paola; Hsiang, Jieh: On the modelling of search in theorem proving -- towards a theory of strategy analysis (1998)
  2. Bonacina, Maria Paola; Hsiang, Jieh: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. (1998) ioport
  3. Jouannaud, Jean-Pierre; Rubio, Albert: Rewrite orderings for higher-order terms in (\eta)-long (\beta)-normal form and the recursive path ordering (1998)
  4. Rao, M. R. K. Krishna; Kapur, Deepak; Shyamasundar, R. K.: Transformational methodology for proving termination of logic programs (1998)
  5. Krishna Rao, M. R. K.; Kapur, D.; Shyamasundar, R. K.: Proving termination of GHC programs. (1997) ioport
  6. Krishna Rao, M. R. K.; Kapur, D.; Shyamasundar, R. K.: Proving termination of GHC programs. (1997) ioport
  7. Kapur, Deepak; Subramaniam, M.: Lemma discovery in automating induction (1996)
  8. Kapur, Deepak; Subramaniam, M.: New uses of linear arithmetic in automated theorem proving by induction (1996)
  9. Kapur, Deepak; Sivakumar, G.; Zhang, Hantao: A path ordering for proving termination of AC rewrite systems (1995)
  10. Kapur, D.; Zhang, H.: An overview of rewrite rule laboratory (RRL) (1995) ioport
  11. Bonacina, Maria Paola; Hsiang, Jieh: Parallelization of deduction strategies: An analytical study (1994) ioport
  12. Bonacina, Maria Paola; Hsiang, Jieh: On subsumption in distributed derivations (1994)
  13. Hermiller, Susan M.: Rewriting systems of Coxeter groups (1994)
  14. Kapur, D.; Nie, X.; Musser, D. R.: An overview of the Tecton proof system (1994)
  15. Kapur, D.; Nie, X.; Musser, D. R.: An overview of the tecton proof system. (1994) ioport
  16. Stavridou, Victoria: Gordon’s computer: A hardware verification case study in OBJ3 (1994)
  17. Zhang, Hantao: Automated proofs of equality problems in Overbeek’s competition (1993)
  18. Zhang, Hantao; Hua, Gary Xin: Proving Ramsey’s theory by the cover set induction: A case and comparision study. (1993)
  19. Martin, Ursula; Lai, Michael: Some experiments with a completion theorem prover (1992)
  20. Wos, Larry; McCune, William: The application of automated reasoning to questions in mathematics and logic (1992)