Toyama, Yoshihito How to prove equivalence of term rewriting systems without induction. (English) Zbl 0642.68033 Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 118-127 (1986). Summary: [For the entire collection see Zbl 0598.00015.] A simple method is proposed for testing equivalence in a restricted domain of two given term rewriting systems. By using the Church-Rosser property and the reachability of term rewriting systems, the method allows us to prove equivalence of these systems without explicit use of induction; this proof usually requires some kind of induction. The method proposed is a general extension of inductionless induction methods developed by Musser, Goguen, Huet, and Hullot, and allows us to extend inductionless induction concepts to not only term rewriting systems with the termination property, but also various reduction systems: term rewriting systems without the termination property, string rewriting systems, graph rewriting systems, combinatory reduction systems, and resolution systems. This method is applied to test equivalence of term rewriting systems, to prove the inductive theorems, and to derive a new term rewriting system from a given system by using equivalence transformation rules. Cited in 2 Documents MSC: 68Q65 Abstract data types; algebraic specification 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 08B05 Equational logic, Mal’tsev conditions Keywords:Church-Rosser property; inductionless induction; equivalence of term rewriting systems; inductive theorems; equivalence transformation Citations:Zbl 0598.00015 PDFBibTeX XML