Proofs by induction in equational theories with constructors

摘要

We show how to prove (and disprove) theorems in the initial algebra of an equational variety by a simple extension of the Knuth-Bendix completion algorithm. This allows us to prove by purely equational reasoning theorems whose proof usually requires induction. We show applications of this method to proofs of programs computing over data structures, and to proofs of algebraic-summation identities. This work extends and simplifies recent results of Musser, “Proc., 7th Annual ACM Symposium on Principles of Programming Languages,” Las Vegas, January 1980, pp. 154–162, and Goguen, “Proc., 5th Conf. on Automated Deduction,” Les Arcs, July 1980, pp. 356–373.