Goguen, J. A. How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation. (English) Zbl 0438.68043 Automated deduction, 5th Conf., Les Arcs/France 1980, Lect. Notes Comput. Sci. 87, 356-373 (1980). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 1 ReviewCited in 37 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68P05 Data structures 68Q65 Abstract data types; algebraic specification 08A99 Algebraic structures 03B35 Mechanization of proofs and logical operations Keywords:correctness of data type implementation; deciding the equivalence of expressions; rewrite rules; inductive equational hypotheses; initial algebra; structural induction; Knuth-Bendix algorithm Citations:Zbl 0428.00026 PDFBibTeX XML