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
Este artigo explora como estender a técnica de pares de dependências para provar o encerramento de sistemas de reescrita de ordem superior. Mostramos que a propriedade de terminação de sistemas de reescrita de ordem superior pode ser verificada pela inexistência de um infinito R-cadeia, que é uma extensão do resultado de Arts e Giesl para o caso de primeira ordem. Esclarece-se que a propriedade subtermo da quase-ordenação, utilizada para comprovação automática da extinção, é indispensável.
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.
Copiar
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
Copiar
@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},}
Copiar
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 -