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.
Keywords for this software
References in zbMATH (referenced in 55 articles )
Showing results 1 to 20 of 55.
Sorted by year (- Kapur, Deepak: Conditional congruence closure over uninterpreted and interpreted symbols (2019)
- Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (2017)
- Kirchner, Claude; Kirchner, Hélène; Nahon, Fabrice: Narrowing based inductive proof search (2013)
- Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
- Galdino, André L.; Ayala-Rincón, Mauricio: A formalization of the Knuth-Bendix(-Huet) critical pair theorem (2010)
- L. Galdino, André; Ayala-Rincón, Mauricio: A PVS theory for term rewriting systems (2009)
- Nahon, Fabrice; Kirchner, Claude; Kirchner, Hélène; Brauner, Paul: Inductive proof search modulo (2009)
- Aoto, Takahito: Sound lemma generation for proving inductive validity of equations (2008)
- Giesl, Jürgen; Kühnemann, Armin; Voigtländer, Janis: Deaccumulation techniques for improving provability (2007)
- Beeson, Michael: Mathematical induction in Otter-lambda (2006)
- Kapur, Deepak: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs (2006)
- Gamboa, Ruben A.: The correctness of the fast Fourier transform: A structured proof in ACL2 (2002)
- Kapur, Deepak: Rewriting, induction and decision procedures: A case study of Presburger arithmetic (2001)
- Stratulat, Sorin: A general framework to build contextual cover set induction provers (2001)
- Comon, Hubert; Nieuwenhuis, Robert: Induction = I-axiomatization + first-order consistency. (2000)
- Kapur, Deepak; Subramaniam, Mahadevan: Extending decision procedures with induction schemes (2000)
- Kapur, Deepak; Subramaniam, Mahadevan: Using an induction prover for verifying arithmetic circuits (2000)
- Walther, C.; Kolbe, T.: Proving theorems by reuse (2000)
- Hermiller, Susan M.; Meier, John: Artin groups, rewriting systems and three-manifolds (1999)
- Bonacina, Maria Paola; Hsiang, Jieh: On the modelling of search in theorem proving -- towards a theory of strategy analysis (1998)