An extension of the dependency pair method for proving termination of higher-order rewrite systems

Authors
Sakai, M Watanabe, Y Sakabe, T
Citation
M. Sakai et al., An extension of the dependency pair method for proving termination of higher-order rewrite systems, IEICE T INF, E84D(8), 2001, pp. 1025-1032
Citations number
11
Categorie Soggetti
Information Tecnology & Communication Systems
Journal title
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS
ISSN journal
09168532 → ACNP
Volume
E84D
Issue
8
Year of publication
2001
Pages
1025 - 1032
Database
ISI
SICI code
0916-8532(200108)E84D:8<1025:AEOTDP>2.0.ZU;2-Z
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-existenc e 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 indispensab le.