An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E84-D No.8 pp.1025-1032
- Publication Date
- 2001/08/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Theory/Models of Computation
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
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.
Cite this
Copy
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
Copy
@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},}
Copy
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 -
English
