Presentation 1998/11/20
On Proving Termination by General Dummy Elimination
Masaki Nakamura, Yoshihito Toyama,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) The general dummy elimination defined by Ferreira is a transformation on TRSs that eliminates a function symbol in rules of TRSs to prove termimation easier thsn the original one. Recently, Arts and Giesl introduced the notion of dependency pairs, which gives an effective method for analyzing an infinite reduction sequence. The purpose of this paper is to extend the general dummy elimination and to prove that the extended transformation is sound with respect to termination by the notion of dependency pairs.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) TRS / Termination / Transformation / General Dummy Elimination / Dependency Pair
Paper # COMP98-58
Date of Issue

Conference Information
Committee COMP
Conference Date 1998/11/20(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Theoretical Foundations of Computing (COMP)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) On Proving Termination by General Dummy Elimination
Sub Title (in English)
Keyword(1) TRS
Keyword(2) Termination
Keyword(3) Transformation
Keyword(4) General Dummy Elimination
Keyword(5) Dependency Pair
1st Author's Name Masaki Nakamura
1st Author's Affiliation School of Information Science, JAIST()
2nd Author's Name Yoshihito Toyama
2nd Author's Affiliation School of Information Science, JAIST
Date 1998/11/20
Paper # COMP98-58
Volume (vol) vol.98
Number (no) 432
Page pp.pp.-
#Pages 8
Date of Issue