Elimination transformations for associative-commutative rewriting systems

Kusakari Keiichirou, Nakamura Masaki, Yoshihito Toyama

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)205-229
Number of pages25
JournalJournal of Automated Reasoning
Volume37
Issue number3
DOIs
Publication statusPublished - 2006 Oct 1

Keywords

  • (AC-)dependency pair
  • (AC-)termination
  • Argument filtering
  • Elimination transformation

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Elimination transformations for associative-commutative rewriting systems'. Together they form a unique fingerprint.

Cite this