On proving AC-termination by AC-dependency pairs

K. Kusakari, Y. Toyama

研究成果: Article査読

12 被引用数 (Scopus)

抄録

Arts and Giesl introduced the notion of dependency pairs, which gives effective methods for proving termination of term rewriting systems (TRSs). In this paper, we extend the notion to AC-TRSs, and introduce new methods for effectively proving AC-termination. It is impossible to directly apply the notion of dependency pairs to AC-TRSs. To avoid this difficulty, we introduce the notion of extended dependency pairs. Finally we define the AC-dependency pair and the AC-dependency chain. Furthermore, we propose approximated AC-dependency graphs, which is very useful for proving AC-termination in practice, using the approximation technique based on Ω-reduction and ΩV-reduction.

本文言語English
ページ(範囲)604-612
ページ数9
ジャーナルIEICE Transactions on Information and Systems
E84-D
5
出版ステータスPublished - 2001 5

ASJC Scopus subject areas

  • ソフトウェア
  • ハードウェアとアーキテクチャ
  • コンピュータ ビジョンおよびパターン認識
  • 電子工学および電気工学
  • 人工知能

引用スタイル