How to prove equivalence of term rewriting systems without induction

Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

21 Citations (Scopus)

Abstract

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
Volume90
Issue number2
DOIs
Publication statusPublished - 1991

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this