On Proving AC-Termination by AC-Dependency Pairs

概要

論文の詳細を見る
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 Ω-reduction.
社団法人電子情報通信学会の論文
2001-05-01