How to prove equivalence of term rewriting systems without induction

Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)


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 the 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.

Original languageEnglish
Title of host publication8th International Conference on Automated Deduction - Proceedings
EditorsJorg H. Siekmann
PublisherSpringer Verlag
Number of pages10
ISBN (Print)9783540167808
Publication statusPublished - 1986
Event8th International Conference on Automated Deduction, 1986 - Oxford, United Kingdom
Duration: 1986 Jul 271986 Aug 1

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume230 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other8th International Conference on Automated Deduction, 1986
Country/TerritoryUnited Kingdom

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'How to prove equivalence of term rewriting systems without induction'. Together they form a unique fingerprint.

Cite this