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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Bachmair. Proof by consistency. In Symp. on Logic in Computer Science, IEEE, 1988.
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).
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Symp. on Logic in Computer Science, pages 346–357, IEEE, 1986.
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.
N. Dershowitz. Applications of the Knuth-Bendix completion procedure. In Proc. of the Seminaire d'Informatique Theorique, Paris, pages 95–111, December 1982.
N. Dershowitz. Completion and its applications. In Resolution of Equations in Algebraic Structures, Academic Press, New York, 1988.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.
N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, August 1979.
M. Fay. First-order unification in an equational theory. In Fourth Workshop on Automated Deduction, pages 161–167, Austin, Texas, 1979.
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).
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.
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.
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).
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).
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.
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.
J-M. Hullot. Canonical forms and unification. In Conf. on Automated Deduction, pages 318–334, 1980.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. on Computing, Nov 1986.
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.
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.
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.
D. Kapur, P. Narendran, and H. Zhang. Proof by induction using test sets. In Conf. on Automated Deduction, Oxford, U.K., 1986.
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.
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.
D. S. Lankford. A Simple Explanation of Inductionless Induction. Memo MTP-14, Dep. of Mathmatics, Louisiana Tech. Univ., Aug 1981.
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.
U. S. Reddy. Narrowing as the operational semantics of functional languages. In Symp. on Logic Program., pages 138–151, IEEE, Boston, 1985.
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).
U. S. Reddy. Transformational derivation of programs using the Focus system. In Symp. Practical Software Development Environments, pages 163–172, ACM, December 1988.
D. Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522–587, Sept. 1976.
J. R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM, 21(4):622–642, 1974.
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).
Author information
Authors and Affiliations
Editor information
Rights 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