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 41 to 55 of 55.
Sorted by year (citations)
  1. Kapur, Deepak; Musser, David; Narendran, Paliath; Stillman, Jonathan: Semi-unification (1991)
  2. Kapur, Deepak; Narendran, Paliath; Zhang, Hantao: Automating inductionless induction using test sets (1991)
  3. Lescanne, Pierre: On the recursive decomposition ordering with lexicographical status and other related orderings (1990)
  4. Zhang, Hantao; Kapur, Deepak: Unnecessary inferences in associative-commutative completion procedures (1990)
  5. Lincoln, Patrick; Christian, Jim: Adventures in associative-commutative unification (1989)
  6. Barry, Michele; Cyrluk, David; Kapur, Deepak; Mundy, Joseph; Nguyen, Van- Duc: A multi-level geometric reasoning system for vision (1988)
  7. Kapur, Deepak; Musser, David R.; Narendran, Paliath: Only prime superpositions need be considered in the Knuth-Bendix completion procedure (1988)
  8. Kapur, Deepak; Zhang, Hantao: Problem corner: Proving equivalence of different axiomatizations of free groups (1988)
  9. Zhang, Hantao; Kapur, Deepak: First-order theorem proving using conditional rewrite rules (1988)
  10. Benanav, Dan; Kapur, Deepak; Narendran, Paliath: Complexity of matching problems (1987)
  11. Buchberger, Bruno: History and basic features of the critical-pair/completion procedure (1987)
  12. Dershowitz, Nachum: Termination of rewriting (1987)
  13. Kapur, Deepak; Narendran, Paliath; Zhang, Hantao: Proof by induction using test sets (1986)
  14. Bachmair, Leo; Plaisted, David A.: Termination orderings for associative-commutative rewriting systems (1985)
  15. Krishnamoorthy, M. S.; Narendran, P.: On recursive path ordering (1985)