Proof-theoretic techniques for term rewriting theory.

Nachum Dershowitz, Mitsuhiro Okada

研究成果: Conference contribution

33 被引用数 (Scopus)

抄録

A bridge is presented between term-rewriting theory in computer science and proof theory in logic. It is shown that proof-theoretic tools are very useful for analyzing two basic attributes of term rewriting systems, the termination property and the Church-Rosser property. A counterexample is given to show that Knuth's critical pair lemma does not hold for conditional rewrite systems. Two restrictions on conditional systems under which the critical pair lemma holds are presented. One is considered a generalization of Bergstra-Klop's former result; the other is concerned with a generalization of Kaplan's and Jouannaud-Waldmann's systems.

本文言語English
ホスト出版物のタイトルProc Third Annu Symp on Logic in Comput Sci
出版社Publ by IEEE
ページ104-111
ページ数8
ISBN(印刷版)0818608536
出版ステータスPublished - 1988 12月 1
外部発表はい

出版物シリーズ

名前Proc Third Annu Symp on Logic in Comput Sci

ASJC Scopus subject areas

  • 工学(全般)

フィンガープリント

「Proof-theoretic techniques for term rewriting theory.」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル