The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Arts와 Giesl은 용어 재작성 시스템(TRS)의 종료를 증명하는 효과적인 방법을 제공하는 종속성 쌍 개념을 도입했습니다. 본 논문에서는 개념을 AC-TRS로 확장하고 AC 종료를 효과적으로 증명하는 새로운 방법을 소개합니다. AC-TRS에 종속성 쌍의 개념을 직접 적용하는 것은 불가능합니다. 이러한 어려움을 피하기 위해 확장 종속성 쌍이라는 개념을 도입합니다. 마지막으로 AC 종속성 쌍과 AC 종속성 체인을 정의합니다. 또한, Ω-reduction과 Ω에 기반한 근사기법을 이용하여 실제 AC-termination을 증명하는데 매우 유용한 근사된 AC-의존성 그래프를 제안한다.V-절감.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
부
Keiichirou KUSAKARI, Yoshihito TOYAMA, "On Proving AC-Termination by AC-Dependency Pairs" in IEICE TRANSACTIONS on Information,
vol. E84-D, no. 5, pp. 604-612, May 2001, doi: .
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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e84-d_5_604/_p
부
@ARTICLE{e84-d_5_604,
author={Keiichirou KUSAKARI, Yoshihito TOYAMA, },
journal={IEICE TRANSACTIONS on Information},
title={On Proving AC-Termination by AC-Dependency Pairs},
year={2001},
volume={E84-D},
number={5},
pages={604-612},
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.},
keywords={},
doi={},
ISSN={},
month={May},}
부
TY - JOUR
TI - On Proving AC-Termination by AC-Dependency Pairs
T2 - IEICE TRANSACTIONS on Information
SP - 604
EP - 612
AU - Keiichirou KUSAKARI
AU - Yoshihito TOYAMA
PY - 2001
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E84-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2001
AB - 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.
ER -