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
본 논문에서는 고차 재작성 시스템의 종료를 증명하기 위해 종속성 쌍 기술을 확장하는 방법을 탐구합니다. 우리는 고차 재작성 시스템의 종료 속성이 무한의 존재로 확인될 수 있음을 보여줍니다. R-chain은 1차 사례에 대한 Arts'와 Giesl의 결과를 확장한 것입니다. 종료를 자동으로 증명하는 데 사용되는 준주문의 하위 항목 속성이 필수라는 것이 분명해졌습니다.
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.
부
Masahiko SAKAI, Yoshitsugu WATANABE, Toshiki SAKABE, "An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems" in IEICE TRANSACTIONS on Information,
vol. E84-D, no. 8, pp. 1025-1032, August 2001, doi: .
Abstract: This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. We show that the termination property of higher-order rewrite systems can be checked by the non-existence of an infinite R-chain, which is an extension of Arts' and Giesl's result for the first-order case. It is clarified that the subterm property of the quasi-ordering, used for proving termination automatically, is indispensable.
URL: https://global.ieice.org/en_transactions/information/10.1587/e84-d_8_1025/_p
부
@ARTICLE{e84-d_8_1025,
author={Masahiko SAKAI, Yoshitsugu WATANABE, Toshiki SAKABE, },
journal={IEICE TRANSACTIONS on Information},
title={An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems},
year={2001},
volume={E84-D},
number={8},
pages={1025-1032},
abstract={This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. We show that the termination property of higher-order rewrite systems can be checked by the non-existence of an infinite R-chain, which is an extension of Arts' and Giesl's result for the first-order case. It is clarified that the subterm property of the quasi-ordering, used for proving termination automatically, is indispensable.},
keywords={},
doi={},
ISSN={},
month={August},}
부
TY - JOUR
TI - An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
T2 - IEICE TRANSACTIONS on Information
SP - 1025
EP - 1032
AU - Masahiko SAKAI
AU - Yoshitsugu WATANABE
AU - Toshiki SAKABE
PY - 2001
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E84-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2001
AB - This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. We show that the termination property of higher-order rewrite systems can be checked by the non-existence of an infinite R-chain, which is an extension of Arts' and Giesl's result for the first-order case. It is clarified that the subterm property of the quasi-ordering, used for proving termination automatically, is indispensable.
ER -