How to prove equivalence of term rewriting systems without induction

Yoshihito Toyama

研究成果: Article査読

23 被引用数 (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.

本文言語English
ページ(範囲)369-390
ページ数22
ジャーナルTheoretical Computer Science
90
2
DOI
出版ステータスPublished - 1991

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「How to prove equivalence of term rewriting systems without induction」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル