Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 604-612 |
Number of pages | 9 |
Journal | IEICE Transactions on Information and Systems |
Volume | E84-D |
Issue number | 5 |
Publication status | Published - 2001 May |
Keywords
- AC-dependency graph
- AC-dependency pair
- AC-term rewriting system
- AC-termination
ASJC Scopus subject areas
- Software
- Hardware and Architecture
- Computer Vision and Pattern Recognition
- Electrical and Electronic Engineering
- Artificial Intelligence