How to prove equivalence of term rewriting systems without induction

Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

23 Citations (Scopus)


A simple method, based on the Church-Rosser property and reachability, is proposed for proving the equivalence in a restricted domain of two given term rewriting systems without the explicit use of induction; this proof usually requires some kind of induction. The method is applied to prove the inductive theorems and to derive a new term rewriting system from a given system by using the equivalence transformation rules. The result is a general extension of the inductionless induction methods developed by Musser, Goguen, Huet and Hullot.

Original languageEnglish
Pages (from-to)369-390
Number of pages22
JournalTheoretical Computer Science
Issue number2
Publication statusPublished - 1991

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