Elimination transformations for associative-commutative rewriting systems

Kusakari Keiichirou, Nakamura Masaki, Toyama Yoshihito

研究成果: Article査読

4 被引用数 (Scopus)

抄録

To simplify the task of proving termination and AC-termination of term rewriting systems, elimination transformations have been vigorously studied since the 1990s. Dummy elimination, distribution elimination, general dummy elimination, and improved general dummy elimination are examples of elimination transformations. In this paper we clarify the essence of elimination transformations based on the notion of dependency pairs. We first present a theorem that gives a general and essential property for elimination transformations, making them sound with AC-termination. Based on the theorem, we design an elimination transformation called the argument filtering transformation. Next, we clarify the relation among various elimination transformations by comparing them with a corresponding restricted argument filtering transformation. Finally, we compare the AC-dependency pair method with the argument filtering transformation.

本文言語English
ページ(範囲)205-229
ページ数25
ジャーナルJournal of Automated Reasoning
37
3
DOI
出版ステータスPublished - 2006 10月
外部発表はい

ASJC Scopus subject areas

  • ソフトウェア
  • 計算理論と計算数学
  • 人工知能

フィンガープリント

「Elimination transformations for associative-commutative rewriting systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル