This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Dershowitz, N. (1987). Termination of rewriting. J. of Symbolic Computation.
Guttag, J.V., Kapur, D., Musser, D.R. (eds.) (1984). Proceedings of an NSF Workshop on the Rewrite Rule Laboratory Sept. 6–9 Sept. 1983, General Electric Research and Development Center Report 84GEN008.
Hsiang, J. (1985). Refutational theorem proving using term-rewriting systems. Artificial Intelligence Journal, 25, 255–300.
Hsiang, J., and Rusinowitch, M. (1986). “A new method for establishing refutational completeness in theorem proving,” Proc. 8th Conf. on Automated Deduction, LNCS No. 230, Springer Verlag, 141–152.
Jouannaud, J., and Kounalis, E. (1986). Automatic proofs by induction in equational theories without constructors. Proc. of Symposium on Logic in Computer Science, 358–366.
Kapur, D., and Musser, D.R. (1984). Proof by consistency. In Reference
Kapur, D., Musser, D.R., and Narendran, P. (1984). Only prime superpositions need be considered for the Knuth-Bendix completion procedure. GE Corporate Research and Development Report, Schenectady. Also in Journal of Symbolic Computation Vol. 4, August 1988.
Kapur, D., and Narendran, P. (1985). An equational approach to theorem proving in first-order predicate calculus. Proc. of 8th IJCAI, Los Angeles, Calif.
Kapur, D., and Narendran, P. (1987). Matching, Unification and Complexity. SIGSAM Bulletin.
Kapur, D., Narendran, P., and Zhang, H (1985). On sufficient completeness and related properties of term rewriting systems. GE Corporate Research and Development Report, Schenectady, NY. Acta Informatica, Vol. 24, Fasc. 4, August 1987, 395–416.
Kapur, D., Narendran, P., and Zhang, H. (1986). Proof by induction using test sets. Eighth International Conference on Automated Deduction (CADE-8), Oxford, England, July 1986, Lecture Notes in Computer Science, 230, Springer Verlag, New York, 99–117.
Kapur, D. and Sivakumar, G. (1984) Architecture of and experiments with RRL, a Rewrite Rule Laboratory. In: Reference [2], 33–56.
Kapur, D., and Zhang, H. (1987). RRL: A Rewrite Rule Laboratory — User's Manual. GE Corporate Research and Development Report, Schenectady, NY, April 1987.
Kapur, D., and Zhang, H. (1988). RRL: A Rewrite Rule Laboratory. Proc. of Ninth International Conference on Automated Deduction (CADE-9), Argonne, IL, May 1988.
Kapur, D., and Zhang, H. (1988). Proving equivalence of different axiomatizations of free groups. J. of Automated Reasoning 4, 3, 331–352.
Knuth, D.E. and Bendix, P.B. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebras. (ed. J. Leech), Pergamon Press, 263–297.
Lankford, D.S., and Ballantyne, A.M. (1977). Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions. Dept. of Math. and Computer Science, University of Texas, Austin, Texas, Report ATP-39.
Musser, D.R. (1980). On proving inductive properties of abstract data types. Proc. 7th Principles of Programming Languages (POPL).
Narendran, P., and Stillman, J. (1988). Hardware verification in the Interactive VHDL Workstation. In: VLSI Specification, Verification and Synthesis (eds. G. Birtwistle and P.A. Subrahmanyam), Kluwer Academic Publishers, 217–235.
Narendran, P., and Stillman, J. (1988). Formal verification of the Sobel image processing chip. GE Corporate Research and Development Report, Schenectady, NY, November 1987. Proc. Design Automation Conference.
Peterson, G.L., and Stickel, M.E. (1981). Complete sets of reductions for some equational theories. J. ACM, 28/2, 233–264.
Stickel, M.E. (1984). “A case study of theorem proving by the Knuth-Bendix method: discovering that x 3=x implies ring commutativity”, Proc. of 7th Conf. on Automated Deduction, Springer-Verlag LNCS 170, pp. 248–258.
Zhang, H., and Kapur, D. (1987). First-order theorem proving using conditional rewriting. Proc. of Ninth International Conference on Automated Deduction (CADE-9), Argonne, IL, May 1988.
Zhang, H., and Kapur, D. (1989). Consider only general superpositions in completion procedures. This Proceedings.
Zhang, H., Kapur, D., and Krishnamoorthy, M.S. (1988). A mechanizable induction principle for equational specifications. Proc. of Ninth International Conference on Automated Deduction (CADE-9), Argonne, IL, May 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Zhang, H. (1989). An overview of Rewrite Rule Laboratory (RRL). In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_138
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_138
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive