On proving AC-termination by AC-dependency pairs

K. Kusakari, Y. Toyama

Research output: Contribution to journalArticle

12 Citations (Scopus)

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 languageEnglish
Pages (from-to)604-612
Number of pages9
JournalIEICE Transactions on Information and Systems
VolumeE84-D
Issue number5
Publication statusPublished - 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

Cite this