AbstractA method for proof by structural induction is studied, and problems of automatizing the method is investigated. We specially consider the equational part of such proofs and we observe that the ability to cope with possibly infinite searches for non-existent equational proofs is crucial. Completion as a means to find an equational proof of equivalence of two given terms is studied. By heuristics we weaken the requirements of completeness on the resulting set, and thereby present modifications of both standard completion and ordered completion which guarantee termination.
Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs
Additional Key Words and Phrases: Automated Verification, Initial Algebra, Structural Induction
Selected references
- Stephen J. Garland and John V. Guttag. Inductive methods for reasoning about abstract data types. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 219-228, San Diego, California, January 1988.
- John V. Guttag and James J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10:27-52, 1978.
- Gérard Huet. A complete proof of correctness of the Knuth-Bendix completeness algorithm. Journal of Computer and System Sciences, 23(1):11-21, August 1981.
- Gérard Huet and Jean-Marie Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2):239-266, October 1982.
- Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1-33, July 1989.
- David R. Musser. On proving inductive properties of abstract data types. In Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pages 154-162, Las Vegas, Nevada, January 1980.