Name
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/s10817-006-9053-y | Journal of Automated Reasoning |
Keywords | DocType | Volume |
commutative rewriting systems,. ac-termination,dependency pair,ac-dependency pair method,distribution elimination,general dummy elimination,ac-dependency pair,elimination transformations,improved general dummy elimination,corresponding restricted argument,argument ltering,elimination trans- formation,dummy elimination,essential property,elimination transformation,various elimination transformation | Journal | 37 |
Issue | ISSN | Citations |
3 | 0168-7433 | 4 |
PageRank | References | Authors |
0.45 | 26 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Keiichirou Kusakari | 1 | 135 | 9.56 |
| M. Nakamura | 2 | 149 | 30.71 |
| Yoshihito Toyama | 3 | 533 | 49.60 |