@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: RRL
Keywords: rewrite rule laboratory
Description:
Semantics: first-order logic
Deductive machinery: completion procedure, rewriting,
associative-commutative theories, linear arithmetic,
Groebner basis over boolean ring, induction.
Dynamics: ???
Persistence: ???
Automatic proof of theorems in first-order predicate calculus with equality
generating decision procedures foin first-order theories
inductionless induction and explicit induction
checking consistency and completeness of equational specifications
solving equations modulo and equational theory
Input is first-order theory given by set of axioms: equations conditional
equations and arbitrary first-order formulae. All axioms are transformed
to equations and theory viewed as congruence relation.
Contact persons:
Deepak Kapur
Department of Computer Science
State University of New York
Albany NY, USA
kapur@cs.albany.edu
Hantao Zhang
Department of Computer Science
University of Iowa
Iowa City, Iowa
hzhang@cs.uiowa.edu
User group: RPI, SUNY, Albany, U. of Iowa, and other universities.
Pragmatics: ??
Documentation:
Papers which appeared in RTA-85, RTA-89, CADE-8, CADE-9, Acta Informatica,
J. of Symbolic Computation.
D. Kapur and H. Zhang, ``An Overview of RRL (Rewrite Rule Laboratory),''
Proc. of {\it Third International Conf. of Rewriting Techniques
and Applications,} Chapel Hill, North Carolina, April 1989.
D. Kapur, and H. Zhang, {\it RRL: A Rewrite Rule Laboratory -
User's Manual.} Unpublished Manuscript, General Electric Corporate
Research and Development, Schenectady, NY, April 1987. Revised, May 1989.
Applications:
Mechanization of proofs of theorems about algebraic structures
(particularly problems about groups and ring commutativity
problems).
Canonical systems for equational axiomatizations.
Proofs of properties of algorithms and string matching
algorithms written in an equational language.
Debug VHDL description of Sobel Image Processing Chip.
Over 1000 gates, gate level verification using RRL.
Narendran, P and Stillman, J
Formal Verification of the Sobel Image Processing Chip
ta Proc IEEE Design Automation Conf 1988
Extensions/enhancements:
Proof management, proof command language, user interface. These
issues are being addressed in the development of Tecton proof
management system at SUNY, Albany, and RPI. RRL serves as the
inference engine for Tecton.
Resource requirements:
Implemented in Franz Lisp; ported to Austin Kyoto Common Lisp (AKCL)
Runs on SUN, sparcs, Symbolics.
Where-to-get-it: email to kapur or zhang
[info source/date] CADE 9 and d kapur 4/92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%