Skip to main content
SpringerLink
Log in

Term rewriting induction

  • Conference paper
  • First Online:
10th International Conference on Automated Deduction (CADE 1990)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 449))

Included in the following conference series:

Abstract

An induction method called term rewriting induction is proposed for proving properties of term rewriting systems. It is shown that the Knuth-Bendix completion-based inductive proof procedures construct term rewriting induction proofs. It has been widely held heretofore that these procedures construct proofs by consistency, and cannot be justified as induction methods. Our formulation shows otherwise. Technically, our result goes beyond the earlier ones in that it is independent of the confluence or ground confluence of the rewrite systems involved. This addresses one of the major criticisms of the method raised in recent times.

This work was supported in part by a NSF grant: NSF-CCR-87-00988.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair. Proof by consistency. In Symp. on Logic in Computer Science, IEEE, 1988.

    Google Scholar 

  2. L. Bachmair and N. Dershowitz. Completion for rewriting module a congruence. In P. Lescanne, editor, Rewriting Techniques and Applications, pages 192–203, Springer-Verlag, 1987. (Lecture Notes in Comp. Science, Vol 256).

    Google Scholar 

  3. L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Symp. on Logic in Computer Science, pages 346–357, IEEE, 1986.

    Google Scholar 

  4. R. Bündgen and W. Küchlin. Computing ground reducibility and inductively complete positions. In N. Dershowitz, editor, Rewriting Techniques and Appl., pages 59–75, Springer-Verlag, Berlin, 1989.

    Google Scholar 

  5. N. Dershowitz. Applications of the Knuth-Bendix completion procedure. In Proc. of the Seminaire d'Informatique Theorique, Paris, pages 95–111, December 1982.

    Google Scholar 

  6. N. Dershowitz. Completion and its applications. In Resolution of Equations in Algebraic Structures, Academic Press, New York, 1988.

    Google Scholar 

  7. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.

    Google Scholar 

  8. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, August 1979.

    Google Scholar 

  9. M. Fay. First-order unification in an equational theory. In Fourth Workshop on Automated Deduction, pages 161–167, Austin, Texas, 1979.

    Google Scholar 

  10. L. Fribourg. A strong restriction of the inductive completion procedure. In Intern. Conf. Aut., Lang. and Program., pages 105–115, Reenes, France, July 1986. (Springer Lecture Notes in Computer Science, Vol. 226).

    Google Scholar 

  11. S. J. Garland and J. V Guttag. Inductive methods for reasoning about abstract data types. In ACM Symp. on Princ. of Program. Languages, pages 219–228, ACM, 1988.

    Google Scholar 

  12. J. A. Goguen. How to prove inductive hypotheses without induction. In Conf. on Automated Deduction, pages 356–372, Springer Verlag Lecture Notes in Computer Science, Vol 87, Jul 1980.

    Google Scholar 

  13. C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engeler, editor, Symp. Semantics of Algorithmic Languages, pages 102–116, Springer-Verlag, 1971. (Lect. Notes in Math. Vo. 188).

    Google Scholar 

  14. G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, October 1980. (Previous version in Proc. Symp. Foundations of Computer Science, Oct 1977).

    Google Scholar 

  15. G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. In Symp. on Foundations of computer Science, pages 96–107, IEEE, Lake Placid, NY, October 1980.

    Google Scholar 

  16. G. Huet and D. C. Oppen. Equations and rewrite rules: A survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405, Academic Press, New York, 1980.

    Google Scholar 

  17. J-M. Hullot. Canonical forms and unification. In Conf. on Automated Deduction, pages 318–334, 1980.

    Google Scholar 

  18. J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. on Computing, Nov 1986.

    Google Scholar 

  19. J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in equational theories without constructors. In Symp. on Logic in Computer Science, pages 358–366, IEEE, Cambridge, MA., June 1986.

    Google Scholar 

  20. D. Kapur and D. R. Musser. Proof by consistency. In Proc. of NSF Workshop on the Rewrite Rule Laboratory, Sep 4–6, 1983, G.E. R&D Center Report GEN 84008, Schenectady, April 1984.

    Google Scholar 

  21. D. Kapur, P. Narendran, and F. Otto. On Ground-Confluence of Term Rewriting Systems. Technical Report 87-6, General Electric R & D Center, Schenectady, New York, 1987.

    Google Scholar 

  22. D. Kapur, P. Narendran, and H. Zhang. Proof by induction using test sets. In Conf. on Automated Deduction, Oxford, U.K., 1986.

    Google Scholar 

  23. D. Knuth and P. Bendix. Simple word problems in Universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297, Pergamon Press, 1970.

    Google Scholar 

  24. W. Küchlin. Inductive completion by ground proof transformation. In Proc. 1987 MCC Colloquium on Resolution of Equations in Algebraic Structures, MCC, Austin, Texas, 1988.

    Google Scholar 

  25. D. S. Lankford. A Simple Explanation of Inductionless Induction. Memo MTP-14, Dep. of Mathmatics, Louisiana Tech. Univ., Aug 1981.

    Google Scholar 

  26. D. R. Musser. On proving inductive properties of abstract data types. In ACM Symp. on Princ. of Program. Languages, pages 154–162, ACM, Las Vegas, 1980.

    Google Scholar 

  27. U. S. Reddy. Narrowing as the operational semantics of functional languages. In Symp. on Logic Program., pages 138–151, IEEE, Boston, 1985.

    Google Scholar 

  28. U. S. Reddy. Rewriting techniques for program synthesis. In N. Dershowitz, editor, Rewriting Techniques and Appl., pages 388–403, Springer-Verlag, 1989. (LNCS Vol. 355).

    Google Scholar 

  29. U. S. Reddy. Transformational derivation of programs using the Focus system. In Symp. Practical Software Development Environments, pages 163–172, ACM, December 1988.

    Google Scholar 

  30. D. Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522–587, Sept. 1976.

    Google Scholar 

  31. J. R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM, 21(4):622–642, 1974.

    Google Scholar 

  32. H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In E Lusk and R. Overbeek, editors, Conf. on Automated Deduction, pages 162–181, Springer-Verlag, Berlin, 1988. (LNCS Vol 310).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, 61801, Urbana, IL

    Uday S. Reddy

Authors
  1. Uday S. Reddy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reddy, U.S. (1990). Term rewriting induction. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_86

Download citation

  • DOI: https://doi.org/10.1007/3-540-52885-7_86

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52885-2

  • Online ISBN: 978-3-540-47171-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation